Formally Solving Answer-Construction Problems in Lean

Technical Summary: Formally Solving Answer-Construction Problems in Lean

Problem Definition
Mathematical competition problems generally fall into two categories: theorem proving (verifying a given statement) and answer construction (constructing a specific object that satisfies a property). While recent advances in Large Language Models (LLMs) have significantly improved formal theorem proving, formal answer construction remains underexplored. A critical gap exists between informal reasoning systems, which are strong at conjecturing but weak at formal verification, and formal prover LLMs, which are optimized for proofs but struggle to discover the necessary witnesses to eliminate existential quantifiers.

A specific challenge in formalizing answer construction is admissibility. Standard Lean proof checkers verify that a proof term has the correct type but do not inherently enforce that the constructed witness is a canonical, closed-form answer. For instance, a proof might satisfy an existential statement $\exists x, P(x)$ by returning a non-canonical term like sInf PropertySet (the infimum of the set being defined) rather than an explicit natural number (e.g., 245). Such "circular" or non-closed-form witnesses are mathematically valid within the logic but inadmissible as contest answers.

Methodology: Enumerate-Conjecture-Prove (ECP)
To address these challenges, the authors introduce Enumerate-Conjecture-Prove (ECP), a neuro-symbolic framework designed for end-to-end answer construction with formal proofs in Lean 4. ECP separates the process into distinct stages while maintaining a formal verification loop:

1. Problem Formalization & Admissibility Checking:

   • Problems are formalized as functional synthesis tasks: finding a function $\Psi$ such that $\forall X, P(X) \to Q(X, \Psi(X))$.
   • An admissibility checker is implemented to ensure the synthesized answer uses only a predefined "admissible vocabulary" (e.g., specific constants, arithmetic operators, and standard constructors). It structurally extracts semantic constants from the Lean term and filters out administrative constants (like typeclass instances or compiler-generated artifacts) and non-canonical definitions (like sInf).

2. Enumerate Stage (Tool-Assisted Exploration):

   • A general-purpose LLM (e.g., GPT-5.4) is equipped with Python tool execution capabilities.
   • The LLM writes and executes Python code to perform bounded enumeration over small domains to find tuples satisfying the problem constraints.
   • These execution traces serve as empirical evidence to identify patterns, invariants, and functional forms.

3. Conjecture Stage (Answer Synthesis):

   • Using the evidence from the Enumerate stage, the same general LLM synthesizes a candidate answer function $\Psi'$.
   • The candidate undergoes two filters before proceeding:
     • Syntactic Verification: The term must compile in Lean with the correct type.
     • Admissibility Verification: The term must only use constants from the allowed vocabulary.
   • If a candidate fails, the system iterates with the failure message included in the prompt.

4. Prove Stage (Formal Verification):

   • Once a valid candidate $\Psi'$ is constructed, the system attempts to prove the instantiated theorem $Stmt(T)|_{\Psi=\Psi'}$.
   • Refutation Loop: Before attempting a proof, the system tries to refute the candidate by proving the negation. If refutation succeeds, the candidate is discarded, and the system returns to the Conjecture stage.
   • Proof Generation: If refutation fails, the system attempts to prove the positive statement using a combination of Lean's built-in automation (tactics like simp, aesop, ring, norm_num) and a specialized prover LLM (e.g., Goedel-Prover-V2). If automation fails, the prover LLM is invoked with a repair loop to generate or fix the proof.

Key Contributions

• Framework for Answer Construction: ECP is the first framework to explicitly separate answer construction from proof generation while enforcing admissibility constraints within a formal verification loop.
• Admissibility Enforcement: The paper introduces a structural method to filter out non-canonical witnesses (e.g., circular definitions) that standard Lean checkers would otherwise accept, ensuring the output matches contest requirements.
• Neuro-Symbolic Integration: The framework effectively combines the exploratory reasoning of general LLMs with Python tools and the rigorous proof capabilities of specialized prover LLMs.
• Benchmarks and Autoformalization: The authors autoformalized 75 problems from the 2026 MathArena Final Answer Comps (AIME, HMMT, APEX) and 346 answer-construction problems from PutnamBench, creating a new evaluation standard for this problem type.

Experimental Results
The system was evaluated on MathArena 2026 (75 problems) and PutnamBench (346 problems) against baselines including direct proof-generation LLMs (GPT-5.4, Goedel-Prover-V2).

• End-to-End Performance: ECP outperformed direct proof-generation baselines.
  • MathArena: ECP solved 18/75 problems (Pass@32), compared to 13/75 for the best LLM-only baseline (GPT-5.4).
  • PutnamBench: ECP solved 17/346 problems (Pass@32), compared to 8/346 for GPT-5.4 and 7/346 for Goedel-Prover-V2-32B.
• Answer-Only Accuracy: Tool-assisted answer construction significantly improved the accuracy of the general LLMs in generating correct candidates. For GPT-5.4, tool usage increased correct answer construction on PutnamBench from 290/346 to 303/346.
• Admissibility Impact: Analysis revealed that many proofs generated by baselines were Lean-compilable but contained inadmissible answers (e.g., circular witnesses). ECP's explicit admissibility check was crucial for filtering these out.
• Ablation Studies:
  • Removing the prover LLM correction step reduced performance on MathArena (18 $\to$ 16) and PutnamBench (17 $\to$ 16).
  • Removing Lean automation had a severe impact on MathArena (18 $\to$ 11) but less on PutnamBench in the specific run, suggesting MathArena problems rely more on automation tactics while PutnamBench relies more on prover capacity.
  • Using a smaller prover (8B) maintained MathArena performance but significantly dropped PutnamBench results (17 $\to$ 7), indicating Putnam problems are more proof-search limited.

Significance and Claims
The paper claims that ECP successfully bridges the gap between informal answer generation and formal theorem proving. By explicitly handling the "answer construction" phase and enforcing admissibility, ECP solves instances that are currently intractable for direct proof-generation approaches. The authors emphasize that their approach is particularly effective for problems requiring the construction of a specific witness (existential quantification) rather than just verifying a fixed conclusion.

The work highlights that current formal benchmarks often omit the difficulty of answer construction, focusing instead on "with-answer" versions of problems. ECP demonstrates that combining general LLMs with tool execution for enumeration, followed by specialized prover LLMs for verification, is a viable path toward solving complex, open-ended mathematical problems in formal systems. The authors note limitations regarding the heuristic nature of admissible vocabulary labeling and the potential for combinatorial explosion in the enumeration stage for highly complex combinatorics problems.