MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research
Not on the map. Why?
Abstract (arXiv)
Existing LLM-based theorem provers have achieved impressive results on formal mathematics benchmarks, yet they remain confined to acting as autonomous agents that prove a stated proposition. In this paper, we propose MathCoPilot, a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research, in which the mathematician steers the high-level mathematical direction while AI agents carry out the detailed formalization and proof work under continuous human guidance. MathCoPilot unifies three core capabilities: (1) an interactive workbench where the mathematician and AI agents collaborate through a living proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; (2) automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and (3) topic-driven paper retrieval and automated formalization into a verified Lean knowledge base. Using MathCoPilot, we systematically compare four state-of-the-art LLMs, including Gemini~3.1~Pro, GPT-5.4, and Claude~Opus~4.7, on a FormalMATH subset and on two real PDE theorems requiring deep domain expertise, evaluating their ability to produce verified Lean~4 proofs and to identify errors in deliberately incorrect proofs. Our results show that while current models can handle undergraduate-level problems with high success rates under favorable autoformalization conditions, substantial challenges remain for domain-specific theorems requiring genuine mathematical understanding.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Builds on 22 of its 37 references that are in the map. First posted on arXiv 16 Jul 2026.
Builds on
22 of 37 references.
References · 22
- 2022ReAct: Synergizing Reasoning and Acting in Language Modelscited by 8,695
- 2023Improving Factuality and Reasoning in Language Models through Multiagent Debatecited by 1,784
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
- 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
- 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
- 2022Autoformalization with Large Language Modelscited by 263
- 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
- 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
- 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
- 2022Formal Mathematics Statement Curriculum Learningcited by 142
- 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 101
- 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 82
10 more
- 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 81
- 2023MathChat: Converse to Tackle Challenging Math Problems with LLM Agentscited by 68
- 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
- 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 59
- 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 58
- 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematicscited by 50
- 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
- 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 31
- 2026Automated Conjecture Resolution with Formal Verificationcited by 28
- 2026Process-Verified Reinforcement Learning for Theorem Proving via Leancited by 7
Built on by
Citing papers per year: 2026: 1.
1 paper.