mlsanityData to 7 Oct 2026

Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

arXiv 2210.12283 ↗First posted 21 Oct 2022cs.AI cs.LGcited by 278

Not on the map. Why?

Cited by 88 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

The formalization of existing mathematical proofs is a notoriously difficult process. Despite decades of research on automation and proof assistants, writing formal proofs remains arduous and only accessible to a few experts. While previous studies to automate formalization focused on powerful search algorithms, no attempts were made to take advantage of available informal proofs. In this work, we introduce Draft, Sketch, and Prove (DSP), a method that maps informal proofs to formal proof sketches, and uses the sketches to guide an automated prover by directing its search to easier sub-problems. We investigate two relevant setups where informal proofs are either written by humans or generated by a language model. Our experiments and ablation studies show that large language models are able to produce well-structured formal sketches that follow the same reasoning steps as the informal proofs. Guiding an automated prover with these sketches enhances its performance from 20.9% to 39.3% on a collection of mathematical competition problems.

Key facts. Cited by 278 papers in the map (data through 7 Oct 2026). Builds on 26 of its 42 references that are in the map. First posted on arXiv 21 Oct 2022.

Builds on

26 of 42 references.

References · 26

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  3. 2022PaLM: Scaling Language Modeling with Pathwayscited by 5,304
  4. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  5. 2014Sequence to Sequence Learning with Neural Networkscited by 2,974
  6. 2019The Curious Case of Neural Text Degenerationcited by 2,881
  7. 2022Competition-Level Code Generation with AlphaCodecited by 1,427
  8. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  9. 2022Quantifying Memorization Across Neural Language Modelscited by 755
  10. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  11. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  12. 2019Deep Learning for Symbolic Mathematicscited by 266
14 more
  1. 2022Autoformalization with Large Language Modelscited by 252
  2. 2018A Simple Method for Commonsense Reasoningcited by 223
  3. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  4. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  5. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  6. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  7. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  8. 2021A Neural Network Solves, Explains, and Generates University Math Problems by Program Synthesis and Few-Shot Learning at Human Levelcited by 96
  9. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  10. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  11. 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
  12. 2018TacticToe: Learning to Prove with Tacticscited by 43
  13. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  14. 2019Learning to Reason in Large Theories without Imitationcited by 27

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2022: 2; 2023: 45; 2024: 55; 2025: 92; 2026: 84.

278 papers.

Sort:

By area:

  1. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  2. 2023A Survey of Large Language Modelscited by 2,537
  3. 2024OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problemscited by 1,099
  4. 2023Large Language Modelscited by 774
  5. 2023CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquingcited by 751
  6. 2023Faith and Fate: Limits of Transformers on Compositionalitycited by 496
  7. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  8. 2023Augmented Language Models: a Surveycited by 398
  9. 2023Llemma: An Open Language Model For Mathematicscited by 385
  10. 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoningcited by 379
  11. 2023OBELICS: An Open Web-Scale Filtered Dataset of Interleaved Image-Text Documentscited by 316
  12. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
38 more
  1. 2023G-LLaVA: Solving Geometric Problem with Multi-Modal Large Language Modelcited by 208
  2. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  3. 2023TaskMatrix.AI: Completing Tasks by Connecting Foundation Models with Millions of APIscited by 184
  4. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  5. 2023ReWOO: Decoupling Reasoning from Observations for Efficient Augmented Language Modelscited by 174
  6. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  7. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  8. 2023Progressive-Hint Prompting Improves Reasoning in Large Language Modelscited by 147
  9. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  10. 2024From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Modelscited by 136
  11. 2023Domain Specialization as the Key to Make Large Language Models Disruptive: A Comprehensive Surveycited by 134
  12. 2023Self-Taught Optimizer (STOP): Recursively Self-Improving Code Generationcited by 128
  13. 2024ChartX & ChartVLM: A Versatile Benchmark and Foundation Model for Complicated Chart Reasoningcited by 127
  14. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  15. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  16. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  17. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  18. 2023M3Exam: A Multilingual, Multimodal, Multilevel Benchmark for Examining Large Language Modelscited by 109
  19. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  20. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  21. 2023Cumulative Reasoning with Large Language Modelscited by 94
  22. 2023A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validationcited by 91
  23. 2025DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoningcited by 84
  24. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  25. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  26. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 78
  27. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  28. 2023ReCEval: Evaluating Reasoning Chains via Correctness and Informativenesscited by 76
  29. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  30. 2022Parsel: Algorithmic Reasoning with Language Models by Composing Decompositionscited by 62
  31. 2024ToolNet: Connecting Large Language Models with Massive Tools via Tool Graphcited by 59
  32. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
  33. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  34. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  35. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 54
  36. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 54
  37. 2024Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalizationcited by 53
  38. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50

50 most cited of 278 All 278 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2026Automated Conjecture Resolution with Formal Verification
  2. 2026AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
  3. 2026FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
  4. 2025Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
  5. 2026MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis
  6. 2026MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize
  7. 2026Advancing Mathematics Research with AI-Driven Formal Proof Search
  8. 2026Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification