Efficient Proof Generation for Lean Statements with Multiple Candidate Answers

Pengzhen Lin; Ke Zhang; Maziar Raissi; Zhouxing Shi

cs.CLOct 25, 2026

Efficient Proof Generation for Lean Statements with Multiple Candidate Answers

Authors: Pengzhen Lin, Ke Zhang, Maziar Raissi, Zhouxing Shi

Organizations: University of California, Riverside

Abstract

In formal systems such as Lean 4, efficiently finding answers to mathematical problems and generating verifiable proofs is an important task in automated mathematical reasoning. In the traditional way where an upstream solver provides multiple candidate answers, the common workflow requires searching for proofs for each candidate separately, incurring redundant computational cost. To this end, we propose a joint proof framework that integrates candidate answer selection, answer supplementation, and formal proof generation into a unified reasoning process. At its core is a trained prover that selects given or proposes new answers and generates a proof for at least one answer in a single call. Joint proof can also reuse generated proofs to check for faithfulness errors. For problems with a unique answer, if two distinct answers both obtain verifiable proofs under the same formal statement, this confirms the statement does not faithfully preserve the original problem semantics. On MATH-500, AMC 2023, and AIME 2024/2025/2026, our framework achieves the same formal proof success rate as per-candidate proof generation with about one sixth of the token cost, and identifies at least 6.1% of the formalized statements as unfaithful without requiring additional judges. Our model and code are available at https://github.com/Linppz/Gobble-Prover.

Figures & tables

Figure 1: Our joint proof framework versus the original per-candidate pipeline. For $k$ candidates, the number of prover and Lean calls drops from $O(k)$ to $O(1)$ , and the prover can explore a larger space (answer E). Left: each formal statement is specific to a candidate answer for answer-construction problems. Right: candidates combined.

Figure 2: An unfaithful formal statement lets two values pass Lean. The problem asks how many kids share 12 candies when each gets 4, so the answer is 3, but the formalizer only asks which number divides 12 (dropping the condition that each kid gets 4), so every divisor of 12 becomes provable. Code A proves the statement with 3 (since $12=3\cdot 4$ ) and Code B with 6 (since $12=6\cdot 2$ ), two proofs (type 1); Code C proves both values in one proof (type 2). The only difference between the two types is whether the two values are proved in the same generation; our training additionally rewards type 2. Candidate 5 (not a divisor of 12) fails under all three codes.

Figure 3: Answer selection results ( Section 4.2 ). The first two panels plot accuracy (y-axis) against average prover output tokens per problem (x-axis). Accuracy is the fraction of problems whose correct answer Lean accepts within eight attempts. Markers indicate upstream solvers. Arrows go from each base prover (per-candidate) to our Gobble-Prover (joint proof). The third panel plots accuracy under a per-problem token budget (x-axis), pooling both prover pairs. Joint proof reaches the final per-candidate accuracy at 16.4K tokens instead of 104.7K. The fourth panel plots cumulative Lean CPU wall-clock relative to per-candidate proof generation (y-axis) as problems are processed (x-axis). Even when verifying all declared values, joint proof needs only 45% of that time.

Figure 4: Unfaithfulness detection ( Section 4.3 ), taking the union of Gobble-Prover-4B and 1.7B at pass@10. Bar height is the share of statements accepted by Lean. The purple part is the share flagged as unfaithful, i.e., with two distinct accepted values. Letters name the autoformalizers above the bars. Harder datasets have shorter bars but a larger purple fraction. In total, 46% of statements pass Lean and 5.4% are flagged. Per-prover results are in Appendix D.2 .

Gobble-Prover-1.7B	0%			100%
Gobble-Prover-1.7B	Pass	Unf.	Lean	Pass	Unf.	Lean
no out-of-set + top-2	6.6	2.5	16.1	33.9	2.6	18.9
out-of-set + top-2	22.3	2.6	19.1	35.7	2.7	19.8
no out-of-set + all	7.4	3.5	123.9	35.8	4.0	141.3
out-of-set + all	24.2	3.6	127.5	37.8	4.1	142.4
Kimina-1.7B , no out-of-set + all				8.1	0.7	16.8

Table 1: Ablation over the five datasets. Column groups: the share of formal statements whose candidate set contains the correct answer (0% and 100%). Pass: Lean pass rate (%); Unf.: unfaithfulness detection rate (%); Lean: number of Lean calls (

\times 10^{3}

). top-2 / all: send the first two declared values / all candidates and proposed values to Lean. † Untrained. Results for all shares and datasets are in Table 9 (Appendix E.1 ).

Model	Decl.	Lean
Kimina-Prover-Distill-1.7B (base)	0.329	0.041
+ SFT	75.185	20.905
+ SFT + RL (Gobble-Prover-1.7B)	98.025	29.712
Pythagoras-Prover-4B (base)	1.687	0.370
+ SFT	82.510	20.947
+ SFT + RL (Gobble-Prover-4B)	99.959	30.86

Table 2: Training-stage ablation. Decl.: outputs with a declared list (%). Lean: outputs with at least one Lean-accepted declared value (%).

Appendix figures & tables11 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 5: Template construction: the answer expression is masked as <candidate> , and candidate answers are substituted into the same template.

Solver	MATH -500	AMC 2023	AIME 2024	AIME 2025	AIME 2026	All
Kimina-1.7B (base)
Gemma 4B	45.2	40.0	3.3	3.3	0.0	38.7
Qwen 0.8B	41.6	25.0	0.0	0.0	0.0	34.6
Qwen 2B	48.6	35.0	3.3	3.3	3.3	41.3
Qwen 9B	49.8	42.5	6.7	3.3	3.3	42.9
Gobble-1.7B (ours)

Appendix

Table 3: Accuracy (%) by dataset for each prover and upstream solver, with at most eight attempts per problem (the setting of Figure 3 ). A problem counts as solved when Lean accepts its ground-truth answer. All: the 630 problems together. Solvers: Gemma-3-4B and Qwen3.5-0.8B/2B/9B.

Solver	MV	Kimina 1.7B	Gobble 1.7B	Pythagoras 4B	Gobble 4B
Gemma-3-4B	68.4	69.8	70.3	70.2	70.8
Qwen3.5-0.8B	52.9	55.6	59.8	56.7	59.5
Qwen3.5-2B	79.8	81.1	81.4	81.3	81.7
Qwen3.5-9B	94.1	94.3	94.6	94.4	94.7

Appendix

Table 4: Accuracy (%) on the 630 problems: majority voting over the eight upstream responses (MV) versus Lean-first selection with MV fallback, for each prover.

		MATH -500	AIME 2024	AIME 2025	AIME 2026	AMC 2023	Total
K	Pass	48.1	36.7	28.3	11.1	28.2	43.7
	Unf.	5.6	16.7	13.3	5.6	5.1	6.5
S	Pass	47.4	25.0	10.7	20.0	34.6	42.9
	Unf.	4.2	13.3	8.9	7.5	7.7	5.2
G	Pass	56.9	10.0	21.4	13.3	52.6	50.6
	Unf.	4.3	5.0	14.3	3.3	1.3	4.5

Appendix

Table 5: Unfaithfulness detection by dataset and autoformalizer, union of Gobble-Prover-4B and Gobble-Prover-1.7B (the data of Figure 4 ). Pass: formal statements with a Lean-accepted candidate (%); Unf.: statements flagged as unfaithful (%). K: Kimina-Autoformalizer-7B; S: StepFun-Formalizer-7B; G: Goedel-Formalizer-V2-32B; All: the three pooled.

	Gobble-Prover-4B						Gobble-Prover-1.7B
	Correct answer + NL			Incorrect answer + NL			Correct answer + NL			Incorrect answer + NL
Dataset	Solved	Unf.	Ratio	Solved	Unf.	Ratio	Solved	Unf.	Ratio	Solved	Unf.	Ratio
MATH-500	46.0	4.4	9.6	44.7	3.7	8.4	46.3	3.8	8.2	44.4	2.9	6.4
AIME 2024	17.8	13.3	75.0	16.7	10.0	60.0	18.9	6.7	35.3	15.6	4.4	28.6
AIME 2025	9.3	8.1	87.5	18.6	15.1	81.2	15.1	7.0	46.2	16.3	8.1	50.0
AIME 2026	5.2	2.6	50.0	9.1	2.6	28.6	10.4	2.6	25.0	14.3	3.9	27.3

Appendix

Table 6: Unfaithfulness detection at pass@10, by statement origin, aggregated across three autoformalizers. Solved: Lean-accepted statements (%); Unf.: detected unfaithful statements (%); Ratio: Unf./Solved (%). Statements built from correct and from incorrect answers show no clear difference in unfaithfulness.

Figure 6: Unfaithfulness detection on pass@10. Pink and purple represent the formal statements accepted by Lean, and the purple portion indicates the unfaithfulness our framework detects. Unfaithful formalization occurs more frequently on harder problems.

Prover	MATH-500	AIME 2024	AMC 2023	Total
4B	1.4 (7/496)	0.0	2.5 (1/40)	1.3 (8/626)
1.7B	0.8 (4/496)	3.3 (1/30)	2.5 (1/40)	1.0 (6/626)
Union	1.8 (9/496)	3.3 (1/30)	2.5 (1/40)	1.8 (11/626)

Appendix

Table 7: Unfaithfulness detection by our framework on the formal statements from the answer-selection experiment ( Section 4.2 ), with GPT-5.6 Sol as the formalizer. Rows: Gobble-Prover-4B (4B), Gobble-Prover-1.7B (1.7B), and their union; columns: datasets. Each cell is the share of problems flagged as unfaithful (%), with the number of flagged problems over the number of problems in parentheses.

Gemini 3.7 Flash	Faithful	Unfaithful	Uncertain	Total
	GPT-6 Astra
Faithful	17	20	0	37
Unfaithful	0	187	1	188
Uncertain	0	0	0	0
Total	17	207	1	225

Appendix

Table 8: Joint verdicts on the 225 flagged statements. Every statement in this table was flagged by at least one detection run in Section 4.3 or one ablation run in Section 4.4 .

Correct answer	Method	MATH-500			AIME 2024			AIME 2025			AMC 2023			AIME 2026			Overall
		Pass	Unf.	Lean	Pass	Unf.	Lean	Pass	Unf.	Lean	Pass	Unf.	Lean	Pass	Unf.	Lean	Pass	Unf.	Lean
0%	Gobble-Prover-1.7B
	no out-of-set + top-2	6.6	2.3	12.0	8.3	5.6	1.1	7.0	4.1	1.0	7.8	2.2	1.2	3.1	1.2	0.9	6.6	2.5	16.1
	out-of-set + top-2	24.7	2.5	14.4	12.2	5.6	1.2	13.4	4.1	1.1	16.8	2.2	1.3	7.5	1.9	1.1	22.3	2.6	19.1
	no out-of-set + all	7.4	3.4	99.9	8.3	6.7	5.8	7.0	4.7	5.4	9.5	3.0	7.7	3.1	1.9	5.1	7.4	3.5	123.9
	out-of-set + all	26.8	3.5	102.7	13.3	6.7	6.0	13.4	4.7	5.6	19.4	3.0	7.9	7.5	1.9	5.3	24.2	3.6	127.5

Appendix

Table 9: Full per-dataset results of the ablation in Table 1 . Col 1: share of formal statements with the correct answer in the candidate set; top-2 / all: the first two declared values / all candidates and valid declared values sent to Lean. Pass / Unf.: solve rate / unfaithfulness-detection rate (%, higher is better); Lean: calls (

\times 10^{3}

, lower is better). † Untrained.

Figure 7: Candidate set size study on our Gobble-Prover-4B (pass@8, MATH-500 StepFun) with the correct answer always in the candidate set. We show statements solved under per-statement budgets of generated tokens (left) and Lean calls (middle), alongside unfaithful statements detected under a Lean-call budget (right), for candidate sets of 6, 8, and 12. Solve rates and detection rates are almost the same across candidate set sizes.

Model	pass@1	pass@8	pass@16	pass@32
Kimina-1.7B (base)	50.4	65.2	69.7	70.9
Gobble-1.7B (ours)	50.8	66.4	67.2	70.9
Pythagoras-4B (base)	48.4	67.6	70.9	73.8
Gobble-4B (ours)	47.1	66.0	71.7	72.5

Appendix

Table 10: pass@

N

(%) on miniF2F-test (244 problems, 32 samples per problem).

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 160 papers

Formally Solving Answer-Construction Problems in Lean
May 24, 2025Jialiang Sun, Yuzhi Tang, Ao Li +2Lean Theorem Proving LLM Mathematical Reasoning
University of Toronto, Toronto, Canada · Georgia Institute of Technology, Atlanta, USA
LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
Oct 13, 2026Rodney Lafuente-Mercado, Salman Rahman, Jingyan Shen +3Process Supervision Process Reward Models
University of Texas at Austin · University of California, Los Angeles · New York University
LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
Jun 2, 2026Po-Nien Kung, Linfeng Song, Dawsen Hwang +10Mathematical Reasoning Benchmarks Large Language Model-Guided Theorem Proving
Google Cloud AI Research · Google Cloud · Google DeepMind

May 24, 2025J/K move · Enter open · S save

Formally Solving Answer-Construction Problems in Lean

Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison+1

University of Toronto, Toronto, Canada · Georgia Institute of Technology, Atlanta, USA

Lean Theorem Proving LLM Mathematical Reasoning

Open paper AskPDF 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.

Abstract

Automated Theorem Proving

Explore similar work

Formally Solving Answer-Construction Problems in Lean

LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks