# LeanReasoner: Boosting Complex Logical Reasoning with Lean

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

## Key facts

- Cited by 28 papers in the map (data through 14 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.

## Placed in

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

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Measuring Massive Multitask Language Understanding](https://mlsanity.com/paper/2009.03300/) (2020)
- [Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language models](https://mlsanity.com/paper/2206.04615/) (2022)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [TheoremQA: A Theorem-driven Question Answering dataset](https://mlsanity.com/paper/2305.12524/) (2023)
- [Language models show human-like content effects on reasoning tasks](https://mlsanity.com/paper/2207.07051/) (2022)
- [Solving Math Word Problems by Combining Language Models With Symbolic Solvers](https://mlsanity.com/paper/2304.09102/) (2023)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyond](https://mlsanity.com/paper/2305.14540/) (2023)
- [RECKONING: Reasoning through Dynamic Knowledge Encoding](https://mlsanity.com/paper/2305.06349/) (2023)
- [Certified Deductive Reasoning with Language Models](https://mlsanity.com/paper/2306.04031/) (2023)

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

- [To CoT or not to CoT? Chain-of-thought helps mainly on math and symbolic reasoning](https://mlsanity.com/paper/2409.12183/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://mlsanity.com/paper/2405.01379/) (2024)
- [Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematics](https://mlsanity.com/paper/2504.01995/) (2025)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Improving Chain-of-Thought Reasoning via Quasi-Symbolic Abstractions](https://mlsanity.com/paper/2502.12616/) (2025)
- [CoMAT: Chain of Mathematically Annotated Thought Improves Mathematical Reasoning](https://mlsanity.com/paper/2410.10336/) (2024)
- [Theorem Prover as a Judge for Synthetic Data Generation](https://mlsanity.com/paper/2502.13137/) (2025)
- [A Survey on Mathematical Reasoning and Optimization with Large Language Models](https://mlsanity.com/paper/2503.17726/) (2025)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations](https://mlsanity.com/paper/2505.24264/) (2025)
- [RATIONALYST: Mining Implicit Rationales for Process Supervision of Reasoning](https://mlsanity.com/paper/2410.01044/) (2024)
- [Learning to Disprove: Formal Counterexample Generation with Large Language Models](https://mlsanity.com/paper/2603.19514/) (2026)
- [RefGrader: Automated Grading of Mathematical Competition Proofs using Agentic Workflows](https://mlsanity.com/paper/2510.09021/) (2025)
- [Integrating Expert Knowledge into Logical Programs via LLMs](https://mlsanity.com/paper/2502.12275/) (2025)
- [LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4](https://mlsanity.com/paper/2507.14722/) (2025)
- [Abductive Logical Rule Induction by Bridging Inductive Logic Programming and Multimodal Large Language Models](https://mlsanity.com/paper/2509.21874/) (2025)
- [A Survey of Large Language Models in Discipline-specific Research: Challenges, Methods and Opportunities](https://mlsanity.com/paper/2507.08425/) (2025)
- [MATATA: Weakly Supervised End-to-End MAthematical Tool-Augmented Reasoning for Tabular Applications](https://mlsanity.com/paper/2411.18915/) (2024)
- [Evaluating Robustness of Reasoning Models on Parameterized Logical Problems](https://mlsanity.com/paper/2602.12665/) (2026)
- [LitPivot: Developing Well-Situated Research Ideas Through Dynamic Contextualization and Critique within the Literature Landscape](https://mlsanity.com/paper/2604.02600/) (2026)
- [Inferring Latent Intentions: Attributional Natural Language Inference in LLM Agents](https://mlsanity.com/paper/2601.08742/) (2026)
- [Decompose-and-Formalise: Recursively Verifiable Natural Language Inference](https://mlsanity.com/paper/2601.19605/) (2026)
- [ORACLE: Optimizing Reasoning Abilities of Large Language Models via Constraint-Led Synthetic Data Elicitation](https://mlsanity.com/paper/2603.21140/) (2026)
- [Explorable Proofs: Making Written Proofs Explorable by Grounding Them in Formal Representations](https://mlsanity.com/paper/2604.02598/) (2026)
- [Reasoners or Translators? Contamination-aware Evaluation and Neuro-Symbolic Robustness in Tax Law](https://mlsanity.com/paper/2605.16052/) (2026)
- [GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research](https://mlsanity.com/paper/2609.36663/) (2026)
- [NanoProof: Open and Efficient Automated Theorem Proving in Lean 4](https://mlsanity.com/paper/2610.11605/) (2026)

## 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.