# Formally Solving Answer-Construction Problems in Lean

arXiv: https://arxiv.org/abs/2505.18492 · HTML: https://mlsanity.com/paper/2505.18492/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 28 of its 62 references that are in the map.
- First posted on arXiv 24 May 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 28 of 28)

- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Scaling Laws for Neural Language Models](https://mlsanity.com/paper/2001.08361/) (2020)
- [Training Compute-Optimal Large Language Models](https://mlsanity.com/paper/2203.15556/) (2022)
- [TruthfulQA: Measuring How Models Mimic Human Falsehoods](https://mlsanity.com/paper/2109.07958/) (2021)
- [A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questions](https://mlsanity.com/paper/2311.05232/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning](https://mlsanity.com/paper/2402.06332/) (2024)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad](https://mlsanity.com/paper/2503.21934/) (2025)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [Proving Olympiad Algebraic Inequalities without Human Demonstrations](https://mlsanity.com/paper/2406.14219/) (2024)
- [Manthan: A Data Driven Approach for Boolean Function Synthesis](https://mlsanity.com/paper/2005.06922/) (2020)
- [Lean-auto: An Interface between Lean 4 and Automated Theorem Provers](https://mlsanity.com/paper/2505.14929/) (2025)
- [Functional Synthesis via Input-Output Separation](https://mlsanity.com/paper/1808.08190/) (2018)
- [Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving](https://mlsanity.com/paper/2505.04528/) (2025)
- [HOLL: Program Synthesis for Higher OrderLogic Locking](https://mlsanity.com/paper/2201.10531/) (2022)

## Built on by (most cited first, 1 of 1)

- [Conjecturing: An Overlooked Step in Formal Mathematical Reasoning](https://mlsanity.com/paper/2510.11986/) (2025)

## Abstract (arXiv)

Large language models (LLMs) have achieved remarkable progress in formal mathematical reasoning. Mathematical competition problems fall into two broad types: theorem-proving problems ask for a proof of a fully specified statement, whereas answer-construction problems ask the solver to construct an answer object and prove that it satisfies the stated specification. Existing mathematical reasoning engines mainly target theorem-proving problems, yet answer-construction problems remain less studied. This setting is challenging because model capabilities are misaligned, with general LLMs better suited to answer construction and prover LLMs better suited to proof generation, and because Lean proof checking alone does not rule out inadmissible circular witnesses. To close this gap, we introduce Enumerate-Conjecture-Prove (ECP), a neuro-symbolic framework for solving answer-construction problems in Lean. ECP uses general LLMs to perform bounded enumeration and construct candidate answers, and invokes prover LLMs to produce machine-checked proofs. ECP introduces admissibility checking to ensure that each answer is canonical and does not involve a circular argument. On answer-construction problems from PutnamBench and autoformalized MathArena, ECP formally solves 17/346 PutnamBench instances and 18/75 MathArena instances with admissible answers and proofs, outperforming LLM baselines at aligned inference budgets.