mlsanityData to 7 Oct 2026

LeanReasoner: Boosting Complex Logical Reasoning with Lean

arXiv 2403.13312 ↗First posted 20 Mar 2024cs.CLcited by 28

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

Large language models (LLMs) often struggle with complex logical reasoning due to logical inconsistencies and the inherent difficulty of such reasoning. We use Lean, a theorem proving framework, to address these challenges. By formalizing logical reasoning problems into theorems within Lean, we can solve them by proving or disproving the corresponding theorems. This method reduces the risk of logical inconsistencies with the help of Lean's symbolic solver. It also enhances our ability to treat complex reasoning tasks by using Lean's extensive library of theorem proofs. Our method achieves state-of-the-art performance on the FOLIO dataset and achieves performance near this level on ProofWriter. Notably, these results were accomplished by fine-tuning on fewer than 100 in-domain samples for each dataset.

Key facts. Cited by 28 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 14 of its 33 references that are in the map. First posted on arXiv 20 Mar 2024.

Builds on

14 of 33 references.

References · 14

  1. 2023GPT-4 Technical Reportcited by 18,132
  2. 2021Training Verifiers to Solve Math Word Problemscited by 9,743
  3. 2020Measuring Massive Multitask Language Understandingcited by 7,768
  4. 2022Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language modelscited by 1,970
  5. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  6. 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoningcited by 379
  7. 2022FOLIO: Natural Language Reasoning with First-Order Logiccited by 233
  8. 2023TheoremQA: A Theorem-driven Question Answering datasetcited by 189
  9. 2022Language models show human-like content effects on reasoning taskscited by 171
  10. 2023Solving Math Word Problems by Combining Language Models With Symbolic Solverscited by 124
  11. 2023SatLM: Satisfiability-Aided Language Models Using Declarative Promptingcited by 100
  12. 2023LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyondcited by 37
2 more
  1. 2023RECKONING: Reasoning through Dynamic Knowledge Encodingcited by 17
  2. 2023Certified Deductive Reasoning with Language Modelscited by 8

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 7; 2025: 11; 2026: 10.

28 papers.

Sort:

By area:

  1. 2024To CoT or not to CoT? Chain-of-thought helps mainly on math and symbolic reasoningcited by 257
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  3. 2024Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Provingcited by 35
  4. 2025Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematicscited by 22
  5. 2024Consistent Autoformalization for Constructing Mathematical Librariescited by 20
  6. 2025Improving Chain-of-Thought Reasoning via Quasi-Symbolic Abstractionscited by 17
  7. 2024CoMAT: Chain of Mathematically Annotated Thought Improves Mathematical Reasoningcited by 16
  8. 2025Theorem Prover as a Judge for Synthetic Data Generationcited by 13
  9. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  10. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  11. 2025Faithful and Robust LLM-Driven Theorem Proving for NLI Explanationscited by 8
  12. 2024RATIONALYST: Mining Implicit Rationales for Process Supervision of Reasoningcited by 6
16 more
  1. 2026Learning to Disprove: Formal Counterexample Generation with Large Language Modelscited by 4
  2. 2025Integrating Expert Knowledge into Logical Programs via LLMscited by 3
  3. 2025LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4cited by 3
  4. 2025Abductive Logical Rule Induction by Bridging Inductive Logic Programming and Multimodal Large Language Modelscited by 3
  5. 2025RefGrader: Automated Grading of Mathematical Competition Proofs using Agentic Workflowscited by 3
  6. 2025A Survey of Large Language Models in Discipline-specific Research: Challenges, Methods and Opportunitiescited by 2
  7. 2024MATATA: Weakly Supervised End-to-End MAthematical Tool-Augmented Reasoning for Tabular Applicationscited by 1
  8. 2026Evaluating Robustness of Reasoning Models on Parameterized Logical Problemscited by 1
  9. 2026Inferring Latent Intentions: Attributional Natural Language Inference in LLM Agentscited by 0
  10. 2026Decompose-and-Formalise: Recursively Verifiable Natural Language Inferencecited by 0
  11. 2026ORACLE: Optimizing Reasoning Abilities of Large Language Models via Constraint-Led Synthetic Data Elicitationcited by 0
  12. 2026Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representationscited by 0
  13. 2026LitPivot: Developing Well-Situated Research Ideas Through Dynamic Contextualization and Critique within the Literature Landscapecited by 0
  14. 2026Reasoners or Translators? Contamination-aware Evaluation and Neuro-Symbolic Robustness in Tax Lawcited by 0
  15. 2026GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Researchcited by 0
  16. 2026NanoProof: Open and Efficient Automated Theorem Proving in Lean 4cited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
  2. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
  3. 2024Lean-STaR: Learning to Interleave Thinking and Proving
  4. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
  5. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
  6. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
  7. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover
  8. 2026Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification