Large Language Model-Guided Theorem Proving

Latest papers

40 papers7 papers in the last four weeks, with none the four weeks before. 0.0% of all new papers.

LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning
Mar 22, 2026Jianing Wang, Jianfei Zhang, Qi Guo +24Large Language Model-Guided Theorem Proving Automated Theorem Proving
Meituan LongCat Team
Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
Mar 20, 2026Guillaume Baudart, Marc Lelarge, Tristan Stérin +1Large Language Model-Guided Theorem Proving Automated Theorem Proving
IRIF, Université Paris Cité, Inria, CNRS · DI ENS, PSL University, Inria · PRGM DEV
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
Mar 20, 2026Baoding He, Zenan Li, Wei Sun +4Large Language Model-Guided Theorem Proving Automated Theorem Proving
State Key Laboratory of Novel Software Technology, Nanjing University, China · School of Computer Science, Nanjing University, China · Department of Computer Science, ETH Zurich, Switzerland +1
s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
Mar 15, 2026Balaji Rao, John Harrison, Soonho Kong +2Large Language Model-Guided Theorem Proving Automated Theorem Proving
Stevens Institute of Technology Hoboken, NJ 07030 · Amazon Web Services Seattle, WA 98101
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Mar 3, 2026Austin Letson, Leopoldo Sarra, Auguste Poiroux +9Automated Theorem Proving Lean Theorem Proving
Axiomatic AI · Math, Inc. · EPFL +8
A Minimal Agent for Automated Theorem Proving
Feb 27, 2026Borja Requena, Austin Letson, Krystian Nowakowski +2Large Language Model-Guided Theorem Proving Automated Theorem Proving
Axiomatic AI, Barcelona, Spain.
LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
Feb 27, 2026Antoine Peyronnet, Fabian Gloeckle, Amaury HayatMathematical Reasoning Benchmarks Automated Theorem Proving
1Ecole Normale Superieure de Rennes · 2Ecole des Ponts Paris · 3Korean Institute for Advanced Study
Early Evidence of Vibe-Proving with Consumer LLMs: A Case Study on Spectral Region Characterization with ChatGPT-5.2 (Thinking)
Feb 21, 2026Brecht Verbeken, Brando Vagenende, Marie-Anne Guerry +2Large Language Model-Guided Theorem Proving LLM Mathematical Reasoning
Data Analytics Lab, Vrije Universiteit Brussel, Pleinlaan 5, 1050 Brussel, Belgium · imec-SMIT, Vrije Universiteit Brussel, Pleinlaan 9, 1050 Brussels, Belgium · School of Engineering and Applied Sciences, Harvard University, Cambridge, Massachusetts 02138, USA
Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study
Jan 22, 2026Zachary BurtonInference-Time Search RL for Language Model Reasoning
Massachusetts Institute of Technology, Cambridge, MA, USA.
Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
Sep 16, 2025Kazumi Kasaura, Naoto Onda, Yuta Oriike +3Automated Theorem Proving In-Context Learning
OMRON SINIC X Corporation · RIKEN AIP · AutoRes +7

Mar 22, 2026J/K move · Enter open · S save

LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learning

Jianing Wang, Jianfei Zhang, Qi Guo, Linsen Guo+23

Meituan LongCat Team

Large Language Model-Guided Theorem Proving Automated Theorem Proving Autoformalization RL for Language Model Reasoning Agentic RL

Open paper AskPDF arXiv

We introduce LongCat-Flash-Prover, a flagship 560-billion-parameter open-source Mixture-of- Experts (MoE) model that advances Native Formal Reasoning in Lean4 through agentic tool-integrated reasoning (TIR). We decompose the native formal reasoning task into three independent formal capabilities, i.e., auto-formalization, sketching, and proving. To facilitate these capabilities, we propose a Hybrid-Experts Iteration Framework to expand high-quality task trajectories, including generating a formal statement based on a given informal problem, producing a whole-proof directly from the statement, or a lemma-style sketch. During agentic RL, we present a Hierarchical Importance Sampling Policy Optimization (HisPO) algorithm, which aims to stabilize the MoE model training on such long-horizon tasks. It employs a gradient masking strategy that accounts for the policy staleness and the inherent train-inference engine discrepancies at both sequence and token levels. Additionally, we also incorporate theorem consistency and legality detection mechanisms to eliminate reward hacking issues. Extensive evaluations show that our LongCat-Flash-Prover sets a new state-of-the-art for open-weights models in both auto-formalization and theorem proving. Demonstrating remarkable sample efficiency, it achieves a 97.1% pass rate on MiniF2F-Test using only 72 inference budget per problem. On more challenging benchmarks, it solves 70.8% of ProverBench and 41.5% of PutnamBench with no more than 220 attempts per problem, significantly outperforming existing open-weights baselines.