1 Introduction↩︎

Mathematical research is undergoing a paradigm shift [1]–[3]. For most of its history, the machine has been at most a tool, a calculator, a search engine, or a proof checker, while the mathematician alone poses the questions, devises the arguments, and judges their correctness. The rise of capable AI agents is now challenging this division of labor and pointing toward a new paradigm in which AI and mathematician work as collaborators, the human steering the high-level direction and creation while the machine carries out ever larger parts of the reasoning. The dream of such assistance dates back to the origins of automated theorem proving [4], and the emergence of large language models (LLMs) has accelerated it, with systems such as AlphaProof [5], DeepSeek-Prover [6], and various Lean-based agents [7]–[10] achieving impressive results. However, these systems are inherently task-centered, concentrating on how an agent (or multi agents) can best carry out one concrete step such as proving a given theorem, while overlooking the mathematician’s role in research and failing to support their broader workflow.

The workflow of a working mathematician is far more complex than “prove a given theorem.” It involves several interconnected activities: Reading and digesting existing work. Mathematicians spend a substantial fraction of their time understanding papers, proofs, and constructions produced by others. Long-term knowledge accumulation. Each researcher maintains a personal repository of lemmas, notation conventions, and proof techniques built over years of study. Interactive human-machine collaboration. Researchers need to ask questions, discuss approaches, request explanations, and have their informal sketches formalized by an assistant that adapts to their style. Diverse proof strategies. Mathematicians think in heterogeneous ways: some begin with natural language sketches, while others prefer to formalize first and then reason, so a useful assistant must support multiple strategies rather than committing to a single approach.

Current LLM-based formal mathematics systems primarily operate under a question-and-answer (Q&A) paradigm [9], [11]–[13]. While they are capable of generating complete proof processes, this black-box approach falls short of genuinely assisting mathematicians in active research. First, because these systems directly output complete, end-to-end proofs in a single pass, the generated content is often overwhelming. Mathematicians are forced to parse a massive volume of unsegmented steps, making it difficult to read through the proof, comprehend the underlying logic, or verify its correctness. Second, these systems lack interactivity across levels of granularity. Whether a mathematician wants to propose a high-level proof sketch or intervene at a specific logical step, the Q&A format prevents them from injecting insights or steering the model’s direction mid-generation. Due to these rigidities, practical research tasks remain fundamentally unsupported. A mathematician who wants to formalize a proof from a newly published paper, explore whether a lemma from an earlier result applies, or discuss a proof strategy with an AI collaborator currently has no unified tool to turn to. Moreover, the rapid proliferation of LLM-based provers has made it difficult to understand the relative strengths of different models and strategies. Existing evaluations typically report a single pass-rate number per system, obscuring important questions: how does performance vary across proving strategies? How sensitive are results to the choice of autoformalization pipeline? Can current models detect subtle logical errors in proofs?

To address these gaps, we present MathCoPilot, a human-in-the-loop system that embodies a new human–AI symbiotic paradigm for mathematical research. Rather than treating proving as an autonomous task, MathCoPilot casts it as a collaboration in which the mathematician steers the high-level mathematical direction while AI agents carry out the detailed implementation. Given a research topic, the system supports paper retrieval and automatically transforms the retrieved content into verified Lean code stored in a local knowledge base. When proving theorems, it orchestrates multiple proving skills, dynamically switching between them based on intermediate progress, and automatically verifies each candidate proof in Lean. Crucially, instead of having AI agents converse among themselves, MathCoPilot keeps the mathematician in control through a living proof blueprint, a flowchart of proof steps in which the human provides direction by pointing at any step, while the AI handles the detailed work of brainstorming strategies, decomposing the proof, discharging steps, and formalizing them in Lean.

To understand how different design choices affect proving performance, we conduct a systematic evaluation of the key components within MathCoPilot across different proving skills and autoformalization routes. We carry out two complementary studies. The first is an evaluation on a FormalMATH subset comparing the NL-first and formalization-first skills, in which we evaluate Gemini 3.1 Pro, GPT-5.4, and Claude Opus 4.7. The second is a focused study on two real PDE theorems, the L\(^2\) error estimate for the semi-discrete upwind DG method and the Gauss–Radau projection reference-cell estimate, evaluated across three autoformalization routes, in which we test Gemini 3.1 Pro, GPT-5.4, Claude Opus 4.7, and Claude Sonnet 4 on their ability to produce fully verified Lean 4 proofs and to identify errors in deliberately incorrect proofs.

Our experiments reveal that current models can solve undergraduate-level problems at moderate success rates, and that writing a natural-language proof before formalization roughly doubles the strict pass rate. On the real PDE tasks, performance is highly sensitive to how the statement is formalized: given a well-formed Lean formalization, Claude Opus 4.7 produces verified Lean 4 certificates on every attempt and GPT-5.4 follows closely, whereas the same models fail on version-incompatible formalizations. Performance also varies sharply across proving skills and error-detection capabilities. These findings suggest that while LLMs have made substantial progress on formal mathematics, bridging the gap to research-level mathematical reasoning remains an open challenge.

2 Related Work↩︎

2.1 LLM-Based Theorem Proving↩︎

The integration of AI-driven methods into formal proof has fostered a rich and rapidly evolving line of work. Early approaches primarily used language models for premise selection [4], [14], while subsequent work explored direct proof generation via sequence-to-sequence models [8]. More recently, large language models (LLMs) have demonstrated unprecedented capabilities in mathematical reasoning. However, because verifying pure natural language proofs is inherently difficult, the mainstream paradigm has shifted toward integrating LLMs with formal languages, such as Lean [15] and Isabelle [16]. Despite this shift, directly generating formal code remains a severe bottleneck for current LLMs due to the scarcity of formal training data. Consequently, recent advancements in this domain broadly bifurcate into two distinct categories.

The first category leverages natural language (informal mathematics) as an intermediate bridge. These approaches first generate a natural language proof and subsequently translate it into a formal language for verification. For instance, Draft-Sketch-Prove [7] demonstrated that drafting an informal mathematical sketch to outline the high-level logical structure before attempting formalization significantly improves the model’s success rate. Hilbert [17] further introduced a recursive refinement strategy that first attempts a direct formal proof and, upon verification failure, reverts to natural language to decompose the complex target into smaller, manageable sub-goals before recursively repeating this formalization-decomposition cycle.

The second category confronts the generation challenge head-on by utilizing finetuning [5], [18], [19], data synthesis [12], and advanced inference strategy [20]–[22] to directly enhance the model’s capacity to produce formal tactics. For example, DeepSeek-Prover-V2 [21] utilizes Monte Carlo Tree Search (MCTS) guided by Lean’s state feedback to explore complex proof trees. AlphaProof [5] combined Gemini-based models with RL to solve competition-level geometry and algebra problems. Goedel-Prover-V2 [12] further trains a prover capable of generation, correction, and expansion, rather than relying on pure single-pass generation.

2.2 AI-Assisted Mathematical Research Systems↩︎

Multi-agent reasoning systems [23]–[25] have demonstrated that collaborative debate among agents can improve reasoning quality, and interactive frameworks like ReAct [26] enable iterative reasoning with tool use. Existing mathematical tool bases such as Mathlib [27] provide extensive community-maintained libraries, which are supported by rigorous verification environments like Lean. Building upon these environments, interactive proof systems such as LeanDojo [28] provides an open-source playground that enables fine-grained premise extraction, hard negative mining, and retrieval-augmented theorem proving, while Lean Copilot [29] assists humans by integrating LLM inference into Lean to suggest proof steps, complete sub-goals, and select premises.

Two systems are particularly relevant to our work. Numina-Lean-Agent [9] leverages the capabilities of Claude Code to autonomously orchestrate natural language proving and Lean verification. Rethlas & Archon [10] is a dual-agent system: Rethlas handles literature retrieval, proof planning, and heuristic refinement via natural language, while Archon compiles these informal plans into Lean and fills in the formal gaps. This framework successfully resolved an open Anderson conjecture in commutative algebra.

These systems share a common focus: given a statement, they aim to autonomously generate a complete formal proof. While the vision of fully automated, end-to-end theorem proving is ambitious and has driven significant progress, we argue that the ideal human-AI interaction paradigm should not seek to entirely replace human researchers. Instead, human experts are best suited for high-level directional design, leaving the tedious, low-level formalization tasks to AI. Consequently, our system, MathCoPilot, heavily emphasizes active mathematician involvement. Within our system, humans supervise and continuously refine the overarching proof sketches, while delegating the fine-grained, step-level detail completion to AI. This division of labor ensures that the overall proving workflow remains highly controllable, mathematically intuitive, and ultimately more efficient.

3 MathCoPilot↩︎

MathCoPilot is designed around a simple principle: the system should serve the mathematician, not the benchmark. This means supporting the full breadth of research activities within a single platform, with the mathematician retaining control over the process at every stage. We organize the system around three core capabilities: an interactive human–AI workbench that turns proof construction into a human-in-the-loop process centered on an editable proof blueprint; automated proving skill orchestration; and automated knowledge base construction and maintenance. Figure 1 illustrates the overall architecture.

3.1 Interactive Human–AI Proof Co-Construction↩︎

The core capability of MathCoPilot is an interactive workbench where a mathematician and AI agents co-construct a proof. Rather than delivering a single end-to-end proof, the system organizes the work as a human-in-the-loop pipeline of specialized agents centered on a shared, editable proof blueprint. This keeps the mathematician in control of the high-level direction while the detailed sub-tasks are delegated to the agents. The workflow begins when the mathematician states a target proposition and proceeds through five agents.

Brainstorm Agent. Given the target, the Brainstorm Agent proposes several candidate proof strategies, each a high-level natural-language sketch of a possible route to the result. The mathematician can edit these suggestions directly, merge or discard them, and ultimately selects one strategy to develop. This keeps the choice of overall approach, the step that most depends on mathematical taste, in human hands.

Blueprint Agent. From the selected strategy, the Blueprint Agent generates a proof blueprint by decomposing the sketch into a graph of nodes, where each node is a self-contained sub-step, such as a lemma, a case, or an intermediate claim, and the edges encode logical dependencies. The blueprint is rendered as a flowchart annotated with each node’s natural-language intent and current status (open, in progress, or verified), so that the mathematician can see at a glance which parts of the argument are settled and which remain open. Crucially, interaction is node-local and pointing-based: instead of locating a step through back-and-forth dialogue, the mathematician clicks directly into a node to inspect, edit, or act on that specific step. This makes large proofs navigable and gives the human and the agents a concrete shared workspace.

Prover Agent. The Prover Agent is the discussion-time interface to the automated skill orchestration that will be introduced in Section 3.2. For any node, the mathematician can designate the claim and ask the Prover Agent to discharge it fully automatically. When a step is too hard to close directly, the mathematician can instead recurse: the entire workflow is re-applied to that single node, asking the Brainstorm Agent for sub-strategies, generating a sub-blueprint, and proving the resulting finer sub-steps. This recursion can be repeated to arbitrary depth, letting a difficult proof be broken down until each leaf is automatically provable.

Formalizer Agent. The Formalizer Agent maintains the correspondence between the informal blueprint and Lean 4. When the blueprint is first created, it emits a Lean sketch that mirrors the node structure, namely a skeleton of have statements whose unproven steps are filled with sorry. As each node is completed, it automatically translates that node’s natural-language argument into Lean and validates it against the Lean 4 verifier, so that formal progress accumulates in lockstep with the informal proof.

Aggregation Agent. Once the blueprint is fully discharged, the Aggregation Agent collects the per-node results and synthesizes them into a single coherent natural-language proof of the original target, suitable for inclusion in a paper. It linearizes the dependency graph, stitches the node-level arguments into connected prose, and pairs the exposition with the assembled Lean proof.

Throughout this pipeline, the system provides on-demand explanation: given any node or Lean fragment, it generates natural-language explanations at multiple granularities, from high-level strategy overviews to individual tactic justifications. A mathematician can, for example, ask “why did you apply induction here?” and receive both a formal account of the tactic’s effect and an informal description of the underlying mathematical intuition.

3.2 Proving Skill Orchestration↩︎

A central feature of MathCoPilot is that proving is not a fixed sequential pipeline but rather an automated orchestration of skills that adapt based on the current proof state, Lean feedback, and knowledge base content. The system maintains a pool of proving skills, such as NL-first (generate an informal sketch, then incrementally formalize), formalization-first (fully formalize the statement, then search for tactics via Lean’s own proof state), and knowledge-grounded proving (retrieve analogous theorems and reusable lemmas from the user’s knowledge base before and during proof construction).

Rather than executing these skills in a predetermined order, an orchestrator dynamically selects and composes skills at each step. The proving process typically proceeds as follows: the system begins by analyzing the formal statement and searching the knowledge base for relevant prior results. Based on this analysis, it selects an initial proving skill and generates a proof attempt. This attempt is then submitted to the Lean 4 environment, which returns either a success signal or detailed error information (e.g., type mismatches, missing hypotheses, incomplete tactics, unsolved goals). The orchestrator parses this feedback, diagnoses the failure mode, and decides on the next action, which may include retrying with a different skill, refining the current approach based on the specific error, searching for additional lemmas in the knowledge base, or requesting human intervention.

The key insight is that this is not a fixed workflow but a flexible, feedback-driven orchestration. In some cases, the NL-first skill may produce a clean proof on the first attempt. In others, the system may switch between multiple skills, incorporate knowledge base results mid-proof, and iteratively refine based on Lean feedback several times before arriving at a correct proof. The orchestrator learns from historical proof attempts which skills tend to succeed for which types of problems, improving its selection over time.

3.3 Automated Knowledge Base Construction and Maintenance↩︎

Given a research topic specified by the user, MathCoPilot can retrieve relevant papers from multiple sources including Semantic Scholar, arXiv, and the Lean Mathlib, ranking them by relevance score, citation count, and formalization potential. For each retrieved paper, an extraction agent identifies formal definitions and their dependencies, theorem statements including all hypotheses and conclusions, proof sketches and lemma chains, and the notation conventions used by the authors. The extracted content is then translated into Lean 4 code using LLM prompting with access to the Mathlib library as context, following a dependency-aware ordering where definitions are formalized first, then auxiliary lemmas, then main theorems. Each formalized Lean file is compiled and verified against the Lean 4 type checker, and only content that passes compilation enters the knowledge base.

Crucially, each knowledge base entry stores both the verified Lean 4 code and the natural language proof process that led to it, including the informal reasoning chain, key insights at each step, and the correspondence between natural language arguments and formal tactics. This dual representation serves two purposes: it enables the system to provide natural language explanations when a mathematician retrieves a lemma, and it allows the agents in Section 3.1 to reason about proofs in both informal and formal terms.

Verified entries are indexed by topic tags, theorem names, dependency graphs, and natural language summaries to support flexible retrieval. The knowledge base is personal: it grows organically as the mathematician processes papers and proves theorems, accumulating a reusable repository tailored to their research interests. The system also supports incremental maintenance: when the underlying Lean environment (e.g., Mathlib) is updated, existing entries are automatically re-verified, and any incompatibilities are flagged for the user.

4 FormalMATH Benchmark Experiments↩︎

We first evaluate MathCoPilot in a controlled benchmark setting using a sampled subset of FormalMATH. This section isolates the effect of proving skill choice on undergraduate-level formal mathematics, and then studies whether the full interactive proof-blueprint workflow can recover hard cases unsolved by GPT-5.4 through recursive refinement of unresolved local proof obligations.

4.1 FormalMATH Experimental Setup↩︎

Models and routes. The FormalMATH study evaluates Gemini 3.1 Pro, GPT-5.4, and Claude Opus 4.7. Each model is tested under two proving skills from Section 3.2: formalization-first (FF), where the model works from the formal statement directly, and NL-first (NL), where it first produces a natural-language proof sketch and then translates the argument into Lean.

FormalMATH subset. We sample 21 problems from FormalMATH to compare the proving skills, with exactly three problems from each of seven domains: Algebra, Differentiation, Integral, Multivariable Calculus, Other, Precalculus, and Sequences and Series. Each problem contains a natural-language statement, a formalized Lean statement, and a reference solution. The sampled problems are listed in Appendix 8.1. This gives \(21 \times 3 \times 2 = 126\) proof attempts.

GPT-unsolved subset. To evaluate the full our interactive system beyond a single baseline prompting route, we select 12 cases that GPT-5.4 failed to solve: u-math_862, u-math_645, u-math_166, u-math_839, u-math_93, u-math_237, hardmath_162, DEMIMathAnalysis_86, DEMIMathAnalysis_26, DEMIMathAnalysis_37, DEMIMathAnalysis_19, and DEMIMathAnalysis_75. In this setting the system is allowed to use the interactive proof-blueprint workflow: when a first formalization fails, the unresolved proof obligations are exposed as local nodes, searched against standard mathematical facts, and recursively formalized until either Lean verifies the node or the node remains open.

Verification protocol. We verify FormalMATH proofs with Lean 4.30.0-rc2 and Mathlib v4.30.0-rc2 under a 1200-second timeout. We report a strict pass rate: a proof passes only if lake env lean accepts the file, the final proof is nonempty, and the file contains no sorry/placeholder proof. This strict rule matters: Claude Opus 4.7 has 6/21 raw verifier passes under Formalization-First, but three are empty formal-proof outputs and are therefore counted as failures.

4.2 FormalMATH Results↩︎

Table 1 shows the strict pass rates. The main pattern is simple: generating a natural-language proof before Lean translation substantially improves reliability. The NL skill reaches 20/63 overall, exactly double FF’s 10/63. The improvement is consistent across all three models, with gains of +14.29% for Gemini and GPT and +19.05% for Opus after the empty-proof correction.

The domain-level heatmap in Table 2 gives a more informative view. The NL skill is not uniformly better because the benchmark mixes very different formalization burdens. It gives large gains in Differentiation, where FF solves none of the nine attempts but NL solves six, and in Precalculus, where the per-skill score increases from 5/9 to 7/9. In contrast, Integral, Other, and Sequences and Series remain at 0/18 across both skills and all models. These zero rows are important: they show that failures are not merely model-choice noise, but often reflect missing formal infrastructure, brittle theorem statements, or proof obligations that current single-turn prompting does not bridge.

5pt

Failure analysis further supports this interpretation. The most common blocking category is residual sorry: 19 times under FF and 23 times under NL. Thus, the models often understand enough to state a plausible proof plan but cannot discharge the Lean proof obligations. The NL skill reduces this problem for tractable domains by giving the Lean stage a structured proof skeleton, but it does not solve domains whose formal statements require substantial libraries or nontrivial analytic machinery. Appendix 8.2 gives a concrete NL-skill example from the Integral domain: all three models identify the correct endpoint Laplace-method argument for hardmath_734, yet each final Lean file still contains sorry. This case illustrates why strict verification can disagree with a superficially convincing natural-language derivation.

4.3 Recovering Failures with MathCoPilot↩︎

Table 3 reports the recovery experiment on the 12 difficult FormalMATH cases unsolved by GPT-5.4. In the first system pass, nine of the twelve cases are fully formalized and accepted by Lean under the same strict rule used above. Three cases remain open: u-math_839, u-math_237, and hardmath_162. The failure mode of hardmath_162 is qualitatively different from the other two: the system produces a complete natural-language proof of the endpoint Laplace asymptotic, but the Lean attempt stalls at local analytic and numerical sublemmas. When those sublemmas are recursively exposed as proof-blueprint nodes, the system eventually formalizes the endpoint Laplace statement completely, yielding a verified Lean certificate in tex/lean/Main.lean. Counting this lemma-refinement stage, MathCoPilot verifies 10/12 of the targeted GPT-unsolved cases.

3pt

Table 4 gives a closer view of the most informative recovery case, hardmath_162. In the baseline FormalMATH experiment, all six Gemini/GPT/Opus solutions on this problem, across both FF and NL settings, end with the same failure category: the generated Lean file contains a top-level sorry.The natural-language behavior is more nuanced. Some attempts identify the endpoint-Laplace route, while others correctly notice that the autoformalized target is semantically brittle: the Lean statement uses an outer parameter \(x\), then shadows it inside the function whose limit is being taken, and asks for convergence to a rounded expression depending on the outer \(x\). In either case, the baseline attempts do not convert the Laplace argument into checkable local proof obligations.

3pt

The hardmath_162 refinement is particularly informative. The unsolved obligation is not a high-level proof strategy failure but the formalization of an endpoint Laplace lemma: \[I(x)=\int_{-0.7}^{0.5}(-0.9t^2)e^{x\phi(t)}\,dt, \qquad \phi(t)=1.7t^4-0.3t-0.6\cos t-2\arctan t+2.6,\] with the target asymptotic \[I(x)\sim \frac{(-0.9)(-0.7)^2 e^{x\phi(-0.7)}}{x(-\phi'(-0.7))} \qquad (x\to+\infty),\] together with the numerical bounds \[|\phi(-0.7)-3.98|\le0.001,\qquad \left|\frac{(-0.9)(-0.7)^2}{-\phi'(-0.7)}+0.10\right|\le0.002.\] These are standard consequences of the endpoint form of Laplace’s method plus concrete interval estimates. The system decomposes them into derivative identities, endpoint separation, integration-by-parts, remainder bounds, and numerical inequalities, after which Lean verifies the final theorem. Appendix 8.3 gives the detailed evidence.

The refined statement is also mathematically sharper than the displayed benchmark approximation. The proof does not assert the strict asymptotic equivalence \[I(x)\sim -\frac{0.10 e^{3.98x}}{x},\] which would be sensitive to the rounded exponent. Instead, it proves the exact endpoint formula \[I(x)\sim \frac{-0.9(-0.7)^2}{-\phi'(-0.7)} \frac{e^{x\phi(-0.7)}}{x},\] and separately proves that \(\phi(-0.7)\) is within \(0.001\) of \(3.98\) and that the leading coefficient is within \(0.002\) of \(-0.10\). This separation between exact asymptotics and rounded numerical presentation is precisely the kind of distinction that the proof-blueprint workflow makes explicit.

5 PDE Theorem Proving Experiments↩︎

We next evaluate MathCoPilot on two real theorems from numerical PDE analysis. This setting is deliberately more demanding than the FormalMATH benchmark: the statements come from actual domain-specific analysis, the proofs rely on numerical-method concepts that are not fully developed in Mathlib, and success depends on choosing a suitable formalization boundary rather than merely finding a short tactic proof. We therefore treat the PDE study as a separate real-data evaluation of whether current models can help with research-level mathematical formalization.

5.1 PDE Experimental Setup↩︎

Theorems. We use two real theorems from numerical PDE analysis. They are drawn from the standard discontinuous Galerkin (DG) analysis pipeline for transport-dominated PDEs. Linear advection is the canonical scalar model for wave propagation and conservation-law transport; upwind DG schemes trace back to finite-element discretizations of neutron-transport equations and later became a central family of high-order methods for hyperbolic conservation laws [30]–[32]. The first is the semi-discrete upwind DG error estimate for linear advection, \[\label{eq:dg-advection-error} \|u(\cdot,T)-u_h(\cdot,T)\|_{L^2(0,1)} \le C h^{K+1},\tag{1}\] proved by splitting \(u-u_h=(u-\Pi_hu)+(\Pi_hu-u_h)\), using Galerkin orthogonality, an energy estimate, and Gronwall’s inequality, following the classical error-analysis template for scalar hyperbolic DG methods [33], [34]. The second is the Gauss–Radau reference-cell projection estimate, \[\begin{align} \tag{2} \|\hat{\Pi} \hat{w}-\hat{w}\|_{L^2(\hat{I})} &\le C |\hat{w}|_{H^{k+1}(\hat{I})}, \\ \tag{3} \|P w-w\|_{L^2(I_i)} &\le C h_i^{k+1}|w|_{H^{k+1}(I_i)}. \end{align}\] which represents the local approximation ingredient used in those DG analyses: endpoint matching is aligned with the one-sided upwind flux, while the \(L^2\) bounds are consequences of polynomial approximation, Bramble–Hilbert type estimates, and affine scaling from a reference cell to a physical mesh cell [34]–[36]. Appendix 8.4 states the two PDE cases in more detail.

Routes and models. For these two theorems, we adopt three routes. In the GPT-Formalized and Opus-Formalized routes, GPT-5.4 and Claude Opus 4.7 respectively formalize the statement into a Lean stub, which is then handed to each model to prove. In the Direct route, each model formalizes the statement and writes both the natural-language and Lean proofs on its own. We evaluate Gemini 3.1 Pro, GPT-5.4, and Claude Opus 4.7 on all three routes, and Claude Sonnet 4 on the GPT-Formalized route. This yields 20 Lean proof attempts.

Verification protocol and scope. We use Lean 4.30.0 and Mathlib v4.30.0 under a 600-second timeout. Current Mathlib does not contain a full formal development of DG methods, Sobolev estimates, or Gauss–Radau projection theory. Therefore, successful PDE files often encode the deep analytic ingredients as opaque declarations or axioms and then verify the formal assembly step in Lean. We count these as successful Lean certificates, not as end-to-end formalizations of PDE analysis from first principles. Consequently, the PDE pass rates in Table 5 are not directly comparable to the end-to-end strict pass rates in Table 1.

Wrong-proof diagnostic. Because proof review is an important part of real mathematical work, we also test wrong-proof detection by giving Gemini 3.1 Pro and GPT-5.4 deliberately flawed proofs of the two PDE theorems. Appendices 8.5 and 8.6 summarize the proof-output patterns and wrong-proof diagnostics.

5.2 Proof Synthesis Results↩︎

Table 5 summarizes the PDE proof synthesis results. The GPT-Formalized route performs poorly not because the theorems are mathematically impossible, but because the GPT-produced formalizations are associated with Lean-version and declaration-boundary incompatibilities, including generated declarations that should instead be represented as explicit opaque or axiom assumptions in the tested Lean 4.29 setting. This formalization/version issue causes Gemini, GPT-5.4, and Sonnet to fail both theorems. Claude Opus 4.7 is the only model that adapts the formalization and produces assembly certificates for both. The Opus-Formalized route yields assembly certificates for all six tested attempts. The Direct route is intermediate: GPT-5.4 and Claude Opus 4.7 produce assembly certificates for both theorems under their own declared assumptions, while Gemini 3.1 Pro produces Lean files with logical/tactic-level failures.

These results reveal a different failure mode from the FormalMATH experiment. In the PDE setting, the strongest closed models can produce mathematically coherent natural-language proofs: they mention the correct DG error decomposition, the admissibility of the discrete error \(\xi=\Pi_hu-u_h\) as a test function, energy stability, Gronwall’s inequality, and the Bramble–Hilbert/scaling argument for Gauss–Radau projection. The main bottleneck is turning that understanding into a version-correct and appropriately abstract Lean. Successful proofs typically separate the work into two layers: analytic PDE facts are declared as explicit assumptions, while Lean verifies the algebraic combination, norm inequality, or scaling step. Appendix 8.5 summarizes representative PDE proof-output patterns and identifies which analytic ingredients are treated as opaque declarations or axioms.

We also include an out-of-distribution diagnostic with two open-source theorem-proving models, DeepSeek-Prover-V2 [37] and Goedel-Prover-V2 [12], on the DG theorem. Both fail to produce valid Lean 4 code (0/2). Their outputs remain in natural-language meta-analysis and then repeat until truncation. This suggests that specialization on competition-style formal mathematics does not automatically transfer to PDE/numerical-analysis reasoning.

5.3 Wrong-Proof Detection↩︎

We additionally evaluate whether models can act as mathematical proof reviewers rather than proof constructors. For each PDE theorem, we provide a polished but deliberately flawed proof and ask Gemini 3.1 Pro and GPT-5.4 to decide whether the argument is correct and to locate the failure.

Both models correctly reject all four model-theorem pairs. The diagnostic cases in Appendix 8.6 show that critique can be easier than construction: even when Lean proof generation depends on abstracting away PDE theory with opaque declarations or axioms, the models can still recognize invalid mathematical moves in natural-language proofs. This supports using MathCoPilot’s Formalizer Agent as a complementary mode to proof synthesis, especially for domain-specific arguments whose full formal library support is still incomplete.

6 Discussion↩︎

Our results highlight four key takeaways. Current models show meaningful capability on undergraduate-level formal mathematics, but this capability is highly sensitive to the autoformalization pipeline and to the domain’s available formal infrastructure. The NL-first skill consistently outperforms formalization-first on the FormalMATH subset, validating the intuition that informal reasoning provides a valuable scaffold for formalization. The recovery study further shows that an interactive proof-blueprint loop can recover many hard cases missed by a strong baseline: among twelve GPT-5.4-missed cases, the system produces strict Lean certificates for 9/12 immediately and 10/12 after local lemma refinement. Finally, the gap between benchmark proofs and PDE certificates, together with the wrong-proof diagnostic, underscores that proof construction, formal certification, and mathematical critique remain distinct skills.

These findings carry practical implications: investing in better autoformalization pipelines may yield larger returns than scaling up model size, and evaluation of formal mathematics systems should include domain-specific problems alongside curated benchmarks.

7 Conclusion and Future Work↩︎

We presented MathCoPilot, a human-in-the-loop system embodying a human–AI symbiotic paradigm for mathematical research, which unifies knowledge construction, automated proving skill orchestration, and interactive human–AI collaboration. Our experiments across four state-of-the-art LLMs reveal that these models demonstrate strong capability on undergraduate-level formal mathematics, that the NL-first proving skill achieves higher accuracy than formalization-first, and that autoformalization quality has a decisive impact on proving success. At the same time, performance on real PDE theorems and error detection tasks shows that substantial challenges remain for domain-specific mathematical reasoning.

Several directions for future work are promising. Integrating with community resources such as Mathlib to bootstrap larger knowledge bases would enable cross-community knowledge sharing and reduce the cold-start problem for new users. Training the skill orchestrator to learn from historical proof attempts could develop domain-specific skill preferences that improve with use. Supporting collaborative knowledge bases across research groups, with access control, versioning, and merge capabilities, would extend the system from individual to team-level use. Extending beyond Lean 4 to support Coq, Isabelle, and other proof assistants would enable cross-system knowledge transfer. Finally, conducting rigorous user studies with larger participant pools and controlled experiments would quantify the impact on research productivity.

8 Appendix↩︎

This appendix provides compact case-level details supporting the aggregate results. We first present seven representative FormalMATH problems, one from each sampled domain, to make the benchmark composition concrete. We then analyze the hardmath_734 Integral case as a representative NL-skill failure and the hardmath_162 refinement as a representative MathCoPilot recovery case, before turning to the two PDE diagnostics used for proof synthesis and wrong-proof detection.

8.1 Seven Representative FormalMATH Problems↩︎

To make the benchmark composition transparent, we present one representative problem from each sampled FormalMATH domain. These examples expose the heterogeneous nature of the subset, which ranges from algebraic simplification and elementary differentiation to asymptotic integration, multivariable integration, functional-equation nonexistence, and sequence-space convergence.

8.2 Case C: hardmath_734 NL-First Outputs↩︎

Gemini 3.1 Pro NL-First Natural-Language Proof

Given: The integral \[I(x)=\int_{-0.8}^{-0.1} \bigl(2.7t^5+1.5\sin(t)-1.1\cos(t)+0.5\bigr) e^{x\left(-0.5t^5+4.1\cos(t)+1.9\operatorname{atan}(t)\right)}\,dt.\] We are tasked with developing an analytical formula for \(I(x)\) that is accurate as \(x\to\infty\) and proving that \[I(x)\approx -\frac{0.32e^{3.89x}}{x}.\]

Derivation: Let us define the amplitude function \(f(t)\) and the phase function \(g(t)\) from the integrand such that \[I(x)=\int_{-0.8}^{-0.1}f(t)e^{xg(t)}\,dt:\] \[f(t)=2.7t^5+1.5\sin(t)-1.1\cos(t)+0.5, \qquad g(t)=-0.5t^5+4.1\cos(t)+1.9\operatorname{atan}(t).\] To find the asymptotic behavior of \(I(x)\) as \(x\to\infty\), we apply Laplace’s method. We first analyze the exponent function \(g(t)\) to locate its maximum on the interval \([-0.8,-0.1]\). The first derivative of \(g(t)\) with respect to \(t\) is \[g'(t)=-2.5t^4-4.1\sin(t)+\frac{1.9}{1+t^2}.\] We must determine the sign of \(g'(t)\) for \(t\in[-0.8,-0.1]\). Because \(t<0\) on this interval, \(\sin(t)<0\), which implies that the term \(-4.1\sin(t)\) is strictly positive. We can establish a strict lower bound for \(g'(t)\) by minimizing each of its terms independently on the interval \([-0.8,-0.1]\):

1. The rational term \(\frac{1.9}{1+t^2}\) is positive and monotonically decreasing in magnitude as \(|t|\) increases. Its minimum on the interval occurs at \(t=-0.8\), yielding \[\frac{1.9}{1+(-0.8)^2}=\frac{1.9}{1.64}\approx 1.1585.\]

2. The trigonometric term \(-4.1\sin(t)\) is positive and its minimum occurs at \(t=-0.1\), yielding \[-4.1\sin(-0.1)\approx -4.1(-0.0998)\approx 0.4093.\]

3. The polynomial term \(-2.5t^4\) is negative and its minimum occurs at \(t=-0.8\), yielding \[-2.5(-0.8)^4=-2.5(0.4096)=-1.0240.\]

Summing these minimum contributions provides a lower bound for the derivative: \[g'(t)\ge -1.0240+0.4093+1.1585=0.5438.\] Because \(g'(t)\ge 0.5438>0\) for all \(t\in[-0.8,-0.1]\), the function \(g(t)\) is strictly increasing on the entire interval. Consequently, \(g(t)\) attains its unique absolute maximum at the right endpoint, \(b=-0.1\).

We now invoke the standard theorem for Laplace’s method: If \(f(t)\) and \(g(t)\) are smooth functions, and \(g(t)\) attains its strict global maximum on \([a,b]\) at the right endpoint \(b\) with \(g'(b)>0\), then as \(x\to\infty\), the integral is asymptotically equivalent to \[I(x)\sim \frac{f(b)}{xg'(b)}e^{xg(b)}.\] The functions \(f(t)\) and \(g(t)\) are composed of polynomials, trigonometric, and inverse trigonometric functions, which are smooth everywhere on \([-0.8,-0.1]\). We have already established that the maximum is at \(b=-0.1\) and \(g'(-0.1)>0\). Thus, the hypotheses are fully satisfied.

Next, we evaluate \(f(b)\), \(g(b)\), and \(g'(b)\) at \(b=-0.1\): \[f(-0.1)=2.7(-0.1)^5+1.5\sin(-0.1)-1.1\cos(-0.1)+0.5,\] \[f(-0.1)\approx 2.7(-0.00001)+1.5(-0.099833)-1.1(0.995004)+0.5\approx -0.744282.\] \[g(-0.1)=-0.5(-0.1)^5+4.1\cos(-0.1)+1.9\operatorname{atan}(-0.1),\] \[g(-0.1)\approx -0.5(-0.00001)+4.1(0.995004)+1.9(-0.099669)\approx 3.890152.\] \[g'(-0.1)=-2.5(-0.1)^4-4.1\sin(-0.1)+\frac{1.9}{1+(-0.1)^2},\] \[g'(-0.1)\approx -2.5(0.0001)-4.1(-0.099833)+\frac{1.9}{1.01}\approx 2.290255.\] Substituting these numerical values into the asymptotic formula gives \[I(x)\sim \frac{-0.744282}{2.290255x}e^{3.890152x} \approx -\frac{0.324978}{x}e^{3.890152x}.\] Rounding the coefficient and the exponent to two decimal places, we obtain the final analytical formula: \[I(x)\approx -\frac{0.32e^{3.89x}}{x}.\]

import Mathlib

open Real Filter Function
open scoped BigOperators Topology

theorem hardmath_734 (I : ℝ → ℝ)
  (hI : I = λ x => ∫ t in (-0.8)..(-0.1), (2.7*t^5 + 1.5*sin t - 1.1*cos t + 0.5) *
    exp (x * (-0.5*t^5 + 4.1*cos t + 1.9*arctan t))) :
  ∀ ε > 0, ∃ x_0, ∀ x > x_0, |I x + 0.32 * exp (3.89 * x) / x| < ε := by
  sorry

5:
6: theorem hardmath_734 (I : ℝ → ℝ)
7:   (hI : I = λ x => ∫ t in (-0.8)..(-0.1), (2.7*t^5 + 1.5*sin t - 1.1*cos t + 0.5) *

GPT-5.4 NL-First Natural-Language Proof

We are given, for real \(x\), \[I(x)=\int_{-0.8}^{-0.1}A(t)e^{x\Phi(t)}\,dt,\] where \[A(t)=2.7t^5+1.5\sin t-1.1\cos t+0.5\] and \[\Phi(t)=-0.5t^5+4.1\cos t+1.9\arctan t.\] We must find the leading asymptotic behavior of \(I(x)\) as \(x\to+\infty\).

The integral is of Laplace type. Its leading contribution comes from the point in the interval \([-0.8,-0.1]\) where the phase function \(\Phi\) is maximal. We first identify this point. Differentiating \(\Phi\) gives \[\Phi'(t)=-2.5t^4-4.1\sin t+\frac{1.9}{1+t^2}.\] For \(t\in[-0.8,-0.1]\), we have \(\sin t<0\), so \(-4.1\sin t>0\). Also \(t^4\le 0.8^4\) and \(1+t^2\le 1+0.8^2=1.64\). Hence \[\Phi'(t)\ge -2.5(0.8)^4+\frac{1.9}{1.64}.\] Since \[2.5(0.8)^4=2.5(0.4096)=1.024\] and \[\frac{1.9}{1.64}\approx 1.158536585,\] we obtain \[\Phi'(t)\ge -1.024+1.158536585>0.\] Thus \(\Phi\) is strictly increasing on \([-0.8,-0.1]\). Therefore its maximum occurs at the right endpoint \[b=-0.1.\]

We now apply the endpoint form of Laplace’s method. The relevant standard statement is the following: if \(A,\Phi\) are continuously differentiable on \([a,b]\), \(\Phi'(t)>0\) on \([a,b]\), then as \(x\to+\infty\), \[\int_a^b A(t)e^{x\Phi(t)}\,dt =\frac{A(b)}{x\Phi'(b)}e^{x\Phi(b)}+O\left(\frac{e^{x\Phi(b)}}{x^2}\right).\] Indeed, setting \(U(t)=A(t)/\Phi'(t)\), we have \[A(t)e^{x\Phi(t)}=\frac{U(t)}{x}\frac{d}{dt}\left(e^{x\Phi(t)}\right).\] Integration by parts gives \[\int_a^b A(t)e^{x\Phi(t)}\,dt =\frac{U(b)e^{x\Phi(b)}}{x} -\frac{U(a)e^{x\Phi(a)}}{x} -\frac{1}{x}\int_a^b U'(t)e^{x\Phi(t)}\,dt.\] Since \(\Phi\) is strictly increasing, \(\Phi(a)<\Phi(b)\), so the lower endpoint term is exponentially smaller than \(e^{x\Phi(b)}/x\). Also, because \(\Phi'(t)\) is bounded below by a positive constant and \(U'\) is continuous, the final integral is \(O(e^{x\Phi(b)}/x)\). Therefore the error term is \(O(e^{x\Phi(b)}/x^2)\), proving the stated endpoint asymptotic formula.

In our case \(a=-0.8\) and \(b=-0.1\). We compute the phase value at \(b\): \[\Phi(-0.1)=-0.5(-0.1)^5+4.1\cos(0.1)+1.9\arctan(-0.1).\] Since \((-0.1)^5=-10^{-5}\), this becomes \[\Phi(-0.1)=0.000005+4.1\cos(0.1)-1.9\arctan(0.1).\] Using \[\cos(0.1)\approx 0.995004165278, \qquad \arctan(0.1)\approx 0.099668652491,\] we get \[\Phi(-0.1)\approx 0.000005+4.1(0.995004165278)-1.9(0.099668652491).\] Thus \[\Phi(-0.1)\approx 3.8901516379.\] Next, \[A(-0.1)=2.7(-0.1)^5+1.5\sin(-0.1)-1.1\cos(-0.1)+0.5.\] Using \(\sin(-0.1)=-\sin(0.1)\) and \(\cos(-0.1)=\cos(0.1)\), this is \[A(-0.1)=-0.000027-1.5\sin(0.1)-1.1\cos(0.1)+0.5.\] With \[\sin(0.1)\approx 0.099833416647, \qquad \cos(0.1)\approx 0.995004165278,\] we find \[A(-0.1)\approx -0.7442817068.\] Finally, \[\Phi'(-0.1)=-2.5(-0.1)^4-4.1\sin(-0.1)+\frac{1.9}{1+(-0.1)^2}.\] Therefore \[\Phi'(-0.1)=-0.00025+4.1\sin(0.1)+\frac{1.9}{1.01}.\] Using \(\sin(0.1)\approx 0.099833416647\), we obtain \[\Phi'(-0.1)\approx 2.2902551271.\] Hence \[\frac{A(-0.1)}{\Phi'(-0.1)} \approx\frac{-0.7442817068}{2.2902551271} \approx -0.32497764.\] Therefore Laplace’s endpoint formula gives the precise leading asymptotic behavior \[I(x)=-\frac{0.32497764\ldots}{x}e^{3.8901516379\ldots x} +O\left(\frac{e^{3.8901516379\ldots x}}{x^2}\right) \qquad (x\to+\infty).\] Equivalently, \[I(x)\sim -\frac{0.32497764\ldots}{x}e^{3.8901516379\ldots x}.\] Rounding the coefficient \(-0.32497764\ldots\) to two decimal places gives \(-0.32\), and rounding the exponent coefficient \(3.8901516379\ldots\) to two decimal places gives \(3.89\). Thus the leading asymptotic approximation may be written as \[I(x)\approx -\frac{0.32e^{3.89x}}{x},\] which is the claimed formula. The fully precise asymptotic form retains the constants \(0.32497764\ldots\) and \(3.8901516379\ldots\) displayed above.

import Mathlib

open Real Filter Function
open scoped BigOperators Topology

theorem hardmath_734 (I : ℝ → ℝ)
  (hI : I = λ x => ∫ t in (-0.8)..(-0.1), (2.7*t^5 + 1.5*sin t - 1.1*cos t + 0.5) *
    exp (x * (-0.5*t^5 + 4.1*cos t + 1.9*arctan t))) :
  ∀ ε > 0, ∃ x_0, ∀ x > x_0, |I x + 0.32 * exp (3.89 * x) / x| < ε := by
  sorry

5:
6: theorem hardmath_734 (I : ℝ → ℝ)
7:   (hI : I = λ x => ∫ t in (-0.8)..(-0.1), (2.7*t^5 + 1.5*sin t - 1.1*cos t + 0.5) *

Claude Opus 4.7 NL-First Natural-Language Proof

Proof Plan:

1. Identify the Integral Form. The given function \(I(x)\) is an integral of the form \[I(x)=\int_a^b g(t)e^{xf(t)}\,dt,\] where

   • \(a=-0.8\), \(b=-0.1\);

   • \(g(t)=2.7t^5+1.5\sin t-1.1\cos t+0.5\);

   • \(f(t)=-0.5t^5+4.1\cos t+1.9\arctan t\).

2. Analyze the Phase Function \(f(t)\). To determine the asymptotic behavior of \(I(x)\) as \(x\to\infty\), we use Laplace’s method. We first find the maximum of \(f(t)\) on the interval \([-0.8,-0.1]\).

   The derivative is \[f'(t)=-2.5t^4-4.1\sin t+\frac{1.9}{1+t^2}.\] For \(t\in[-0.8,-0.1]\), \(\sin t<0\), so \(-4.1\sin t>0\). The term \(\frac{1.9}{1+t^2}\) is also positive and bounded below by \(\frac{1.9}{1.64}\approx 1.15\). The negative term \(-2.5t^4\) is at most \(-2.5(0.8)^4\approx -1.024\). Thus, \(f'(t)>0\) strictly on the interval. Since \(f(t)\) is strictly increasing, its maximum occurs at the right endpoint \(b=-0.1\).

3. Evaluate Functions at the Maximum.

   • \(f(-0.1)\approx -0.5(-0.00001)+4.1(0.995004)+1.9(-0.099668)\approx 3.890\);

   • \(g(-0.1)\approx 2.7(-0.00001)+1.5(-0.099833)-1.1(0.995004)+0.5\approx -0.744\);

   • \(f'(-0.1)\approx -2.5(0.0001)-4.1(-0.099833)+\frac{1.9}{1.01}\approx 2.290\).

4. Apply Laplace’s Method. For a maximum at the boundary \(b\) with \(f'(b)>0\), Laplace’s method gives the asymptotic expansion \[I(x)\sim \frac{g(b)}{xf'(b)}e^{xf(b)} \qquad \text{as }x\to\infty.\] Substituting the evaluated constants, \[I(x)\sim \frac{-0.744}{2.290x}e^{3.89x} \approx -0.32\frac{e^{3.89x}}{x}.\]

5. Conclusion. The asymptotic equivalence implies that the difference \[I(x)-\left(-0.32\frac{e^{3.89x}}{x}\right)\] goes to \(0\) (or is bounded appropriately) as \(x\to\infty\). Thus, for any \(\varepsilon>0\), there exists \(x_0\) such that for all \(x>x_0\), \[\left|I(x)+0.32\frac{e^{3.89x}}{x}\right|<\varepsilon.\]

Note on Formalization: Formalizing this proof requires a general version of Laplace’s method for the asymptotic expansion of integrals, which involves deep results in real and complex analysis. Since Mathlib currently lacks the necessary library for asymptotic expansions of integrals (like Watson’s lemma or Laplace’s method), this theorem is genuinely impossible to complete without placeholders. We therefore conclude the proof with sorry.

import Mathlib

open Real Filter Function
open scoped BigOperators Topology

theorem hardmath_734 (I : ℝ → ℝ)
  (hI : I = λ x => ∫ t in (-0.8)..(-0.1), (2.7*t^5 + 1.5*sin t - 1.1*cos t + 0.5) *
    exp (x * (-0.5*t^5 + 4.1*cos t + 1.9*arctan t))) :
  ∀ ε > 0, ∃ x_0, ∀ x > x_0, |I x + 0.32 * exp (3.89 * x) / x| < ε := by
  sorry

5:
6: theorem hardmath_734 (I : ℝ → ℝ)
7:   (hI : I = λ x => ∫ t in (-0.8)..(-0.1), (2.7*t^5 + 1.5*sin t - 1.1*cos t + 0.5) *

8.3 hardmath_162 System Refinement Case↩︎

The isolated lemma is: \[I(x)=\int_{-0.7}^{0.5}(-0.9t^2)e^{x\phi(t)}\,dt, \qquad \phi(t)=1.7t^4-0.3t-0.6\cos t-2\arctan t+2.6,\] \[I(x)\sim \frac{(-0.9)(-0.7)^2 e^{x\phi(-0.7)}}{x(-\phi'(-0.7))} \qquad (x\to+\infty),\] with the numerical estimates \[|\phi(-0.7)-3.98|\le0.001,\qquad \left|\frac{(-0.9)(-0.7)^2}{-\phi'(-0.7)}+0.10\right|\le0.002.\]

8.3.0.1 Baseline attempts and failure mode.

The prior FormalMATH runs in formalbench_project contain six baseline Lean attempts for hardmath_162: Gemini, GPT-5.4, and Claude Opus, each under FF and NL settings. All six fail the strict verifier with the same blocking category, contains_sorry, at the top-level theorem. The generated target also exposes a deeper issue: the benchmark’s rounded display \[I(x)\approx -\frac{0.10e^{3.98x}}{x}\] is autoformalized as a literal Tendsto statement toward the rounded expression. Several baseline natural-language outputs correctly notice that this formal target is not a suitable theorem: the theorem parameter \(x\) is shadowed by the limit variable, and the target neighborhood still depends on the outer \(x\). Other outputs identify the endpoint-Laplace method but still leave the proof as sorry. Thus, the baselines either diagnose the statement-level problem or outline the right method, but do not produce a strict certificate.

3pt

theorem hardmath_162 (x : ℝ) :
    Tendsto
      (λ x => ∫ t in (-0.7)..0.5,
        (-0.9 * t^2) *
          exp (-x * (-1.7 * t^4 + 0.3 * t + 0.6 * cos t
            + 2.0 * arctan t - 2.6)))
      atTop
      ((-0.10 * exp (3.98 * x) / x)) := by
  sorry

8.3.0.2 Natural-language proof process.

Let \(a=-0.7\), \(b=0.5\), \(f(t)=-0.9t^2\), and \[\phi(t)=1.7t^4-0.3t-0.6\cos t-2\arctan t+2.6.\] The proof uses the left-endpoint form of Laplace’s method, but the Lean development does not assume the theorem as a black box. It formalizes the following argument directly.

1. First, compute \[\phi'(t)=6.8t^3-0.3+0.6\sin t-\frac{2}{1+t^2}\] and show that \(\phi'(t)\le -3/4\) on \([a,b]\). Hence \(\phi\) is strictly decreasing on the interval, so its unique maximum occurs at \(a=-0.7\). This also gives the quantitative separation \[\phi(t)\le \phi(a)-\frac{3}{4}(t-a), \qquad t\in[a,b].\]

2. Define \(q(t)=f(t)/(-\phi'(t))\). Since \(-\phi'(t)\) is bounded away from zero on \([a,b]\), \(q\) is differentiable and \(q'\) is bounded by a concrete constant.

3. Rewrite the integrand by integration by parts: \[f(t)e^{x\phi(t)} =-\frac{q(t)}{x}\frac{d}{dt}e^{x\phi(t)}.\] Therefore \[I(x)= \frac{q(a)e^{x\phi(a)}}{x} -\frac{q(b)e^{x\phi(b)}}{x} +\frac{1}{x}\int_a^b q'(t)e^{x\phi(t)}\,dt.\]

4. The endpoint separation makes the right-endpoint boundary term exponentially smaller than \(e^{x\phi(a)}/x\). The same separation bounds the integral remainder by \(O(e^{x\phi(a)}/x^2)\). Dividing by \(q(a)e^{x\phi(a)}/x\) therefore gives a quotient tending to \(1\).

5. Finally, the numerical side conditions are verified by interval estimates: the proof bounds \(-\phi'(a)\), encloses \(\arctan(0.7)\) by an alternating-series argument, and derives \[|\phi(a)-3.98|\le0.001,\qquad \left|\frac{f(a)}{-\phi'(a)}+0.10\right|\le0.002.\]

More explicitly, the integration-by-parts identity writes \[I(x)= \frac{Q(a)e^{x\phi(a)}}{x} -\frac{Q(b)e^{x\phi(b)}}{x} + R(x), \qquad R(x)=\frac{1}{x}\int_a^b Q'(t)e^{x\phi(t)}\,dt,\] where \(Q(t)=f(t)/(-\phi'(t))\). The proof establishes \[\frac{Q(b)e^{x\phi(b)}/x}{e^{x\phi(a)}/x}\to0\] because \(\phi(b)<\phi(a)\). It also proves the quantitative remainder estimate \[|R(x)|\le C\frac{e^{x\phi(a)}}{x^2}\] for all sufficiently large \(x\). This follows by combining a bound \(|Q'(t)|\le M\) with \[e^{x\phi(t)} \le e^{x\phi(a)}e^{-\frac{3}{4}x(t-a)}\] and the elementary integral estimate \[\int_a^b e^{-\frac{3}{4}x(t-a)}\,dt \le \frac{4}{3x}.\] Consequently, \[I(x)= \frac{Q(a)e^{x\phi(a)}}{x} + o\!\left(\frac{e^{x\phi(a)}}{x}\right),\] which is exactly \[I(x)\sim \frac{-0.9(-0.7)^2}{-\phi'(-0.7)} \frac{e^{x\phi(-0.7)}}{x}.\]

8.3.0.3 Exact theorem versus rounded display.

The strict Lean theorem deliberately avoids treating the rounded expression as an exact asymptotic equivalent. Let \[\lambda=\phi(-0.7), \qquad c=\frac{-0.9(-0.7)^2}{-\phi'(-0.7)}.\] The certified result is \[I(x)\sim c\frac{e^{\lambda x}}{x},\] together with the numerical enclosures \(|\lambda-3.98|\le0.001\) and \(|c+0.10|\le0.002\). This distinction matters because replacing \(\lambda\) by \(3.98\) inside the exponential is not asymptotically harmless: \[\frac{c e^{\lambda x}/x}{-0.10e^{3.98x}/x} = \frac{c}{-0.10}e^{(\lambda-3.98)x}.\] Since the endpoint value is approximately \(3.9807\), the rounded display \[I(x)\approx-\frac{0.10e^{3.98x}}{x}\] should be read as a numerical presentation of the exact endpoint parameters, not as a ratio-limit theorem with rounded constants. This is one of the places where the proof-blueprint workflow improves the result: it separates the mathematically correct formal target from the informal rounded answer.

8.3.0.4 Complete Lean endpoint block.

The listing below prints the full endpoint portion of the final certificate in tex/lean/Main.lean. The preceding part of the Lean file contains the definitions of \(\phi\), \(f\), \(I\), \(q\), and the earlier proof-blueprint lemmas; this endpoint block contains the complete formalization of the Laplace remainder estimates, the numerical bounds, and the final theorem interface used by the manuscript.

This case explains why a strict first-pass failure should not always be interpreted as absence of mathematical understanding, while also showing why natural-language insight alone is insufficient. The baseline attempts either identify the right endpoint-Laplace route or diagnose the rounded target as unsuitable, but their Lean certificates remain placeholders. The refined proof-blueprint workflow converts the informal endpoint-Laplace appeal into explicit Lean obligations: monotonicity of the phase, boundedness of the quotient derivative, exponential domination of the non-dominant endpoint, an \(O(e^{x\phi(a)}/x^2)\) remainder bound, and machine-checkable interval arithmetic for the constants. Thus, the remaining gap in hardmath_162 is precisely the gap that MathCoPilot is designed to close: turning a mathematically plausible derivation into a verified, semantically precise theorem.

8.4 Real PDE Cases↩︎

The PDE examples are designed to be qualitatively different from benchmark-style exercises. They come from the analysis of DG methods for transport-dominated equations, where the mathematical content is not a short symbolic manipulation but a combination of stability, projection, and mesh-scaling arguments. They require numerical-analysis concepts not fully developed in Mathlib, so successful Lean files verify the formal assembly under explicit assumptions rather than a from-first-principles formalization of DG methods or Sobolev theory.

8.4.1 PDE Case 1: Upwind DG \(L^2\) Error Estimate↩︎

For the linear advection equation \(u_t+au_x=0\) on \((0,1)\) with \(a>0\) and periodic boundary conditions, the semi-discrete upwind DG scheme seeks \(u_h(t)\in U_h^K\) such that \[B_j(u_h,\varphi_h)=0 \qquad \forall \varphi_h\in U_h^K.\] The target theorem is the estimate \[\|u(\cdot,T)-u_h(\cdot,T)\|_{L^2(0,1)} \le Ch^{K+1}.\] This is a representative smooth-solution estimate for a scalar hyperbolic problem: the upwind numerical flux captures the one-way propagation direction, and the \(L^2\) argument measures how stability and local polynomial approximation combine over time [32]–[34]. The correct proof uses the Gauss–Radau projection \(\Pi_hu\) and splits \[u-u_h=(u-\Pi_hu)+(\Pi_hu-u_h)=\eta+\xi.\] The essential admissibility point is that \(\xi=\Pi_hu-u_h\in U_h^K\), so \(\xi\) may be used as a DG test function, whereas the full error \(e=u-u_h\) generally cannot. Summing the cellwise energy identity yields \[\frac{1}{2}\frac{d}{dt}\|\xi\|_{L^2(0,1)}^2 +\frac{a}{2}\sum_j [\![\xi]\!]_{j+1/2}^2 =-\int_0^1 \eta_t\xi\,dx,\] after the Gauss–Radau endpoint and moment conditions remove the other projection-error terms. Cauchy–Schwarz, Young’s inequality, Gronwall’s inequality, the projected initial data \(\xi(\cdot,0)=0\), and the projection estimate for \(\eta\) give the final \(O(h^{K+1})\) bound.

8.4.1.1 Planted wrong proof.

The flawed proof first enlarges Galerkin orthogonality from discrete test functions to “all test functions,” then chooses \(\varphi=e=u-u_h\). This is invalid because \(u\) is not generally a piecewise polynomial, so \(e\notin U_h^K\). The wrong proof also claims that interface terms cancel, whereas the upwind flux produces a nonnegative jump term.

8.4.2 PDE Case 2: Gauss–Radau Reference-Cell Estimate↩︎

Let \(\hat{I}=(0,1)\) and let \(\hat{\Pi}:H^{k+1}(\hat{I})\to\mathbb{P}^k(\hat{I})\) be the Gauss–Radau projection defined by moment orthogonality against \(\mathbb{P}^{k-1}\) and endpoint matching at \(1\). Such one-sided projections are standard in DG analyses because the endpoint condition interacts cleanly with upwind traces at cell interfaces [32], [34]. The target reference-cell and physical-cell estimates are \[\|\hat{\Pi}\hat{w}-\hat{w}\|_{L^2(\hat{I})} \le C|\hat{w}|_{H^{k+1}(\hat{I})},\qquad \|Pw-w\|_{L^2(I_i)} \le Ch_i^{k+1}|w|_{H^{k+1}(I_i)}.\] The correct proof can be organized through duality. For each \(z\in L^2(\hat{I})\) with \(\|z\|_{L^2}\le 1\), define \[F_z(\hat{w})=\int_0^1(\hat{\Pi}\hat{w}-\hat{w})z\,d\hat{x}.\] Each \(F_z\) is a bounded linear functional that vanishes on \(\mathbb{P}^k\), so Bramble–Hilbert gives \[|F_z(\hat{w})|\le C|\hat{w}|_{H^{k+1}(\hat{I})}.\] The dual characterization of the \(L^2\) norm gives the reference estimate, and the affine scaling \(x=x_{i-1/2}+h_i\hat{x}\) gives the physical-cell estimate.

8.4.2.1 Planted wrong proof.

The flawed proof instead defines \[F(\hat{w})=\|\hat{\Pi}\hat{w}-\hat{w}\|_{L^2(\hat{I})}\] and calls it a bounded linear functional. This is false: it is a norm of a linear error operator, hence nonlinear. A valid repair must use either the dual family \(F_z\), an operator-valued Bramble–Hilbert argument for \(I-\hat{\Pi}\), or a seminorm version of Bramble–Hilbert.

8.5 Representative PDE Proof-Synthesis Outputs↩︎

The selected PDE model outputs reveal three recurring patterns. First, GPT-Formalized failures are mostly formalization failures: the GPT-produced formalization uses declaration forms and abstraction boundaries that are incompatible with the tested Lean 4.29 setup, and most models do not repair them. Second, the Opus-Formalized route succeeds because the Opus-produced formalization expresses the missing analytic theory with modern opaque declarations or explicit axioms, leaving Lean to verify the algebraic assembly step. Third, the Direct route shows that direct natural-language-to-Lean generation can work when the model chooses a suitable abstraction boundary. Table 11 lists all 20 PDE attempts; Table 12 summarizes these proof-synthesis patterns by route.

3pt

3pt

8.6 Wrong-Proof Diagnostic Details↩︎

Table 13 records the diagnostic behavior behind Table 6. The models are not credited for producing a Lean proof here; the task is to reject the flawed natural-language argument and explain the mathematical error.

References↩︎