cs.AIMar 22, 2026

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

Authors: Jianing Wang, Jianfei Zhang, Qi Guo, Linsen Guo, Rumei Li, Chao Zhang, Chong Peng, Cunguang Wang, 

Organizations: Meituan LongCat Team

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

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.

Figures & tables

Figure 1: The performance comparison over proving tasks. The figures on the left and middle illustrate the performance with a limited 32 inference budget on MathOlympiad-Bench and PutnamBench, respectively. The figure on the right shows the model performance on MiniF2F-Test balancing with the inference budgets.
Figure 2: The overview of our hybrid-experts tool-integration synthesis pipeline. In this pipeline, we iteratively optimize three different experts (i.e., auto-formalizer, lemma-style sketcher, and prover), and use these experts to synthesize trajectories based on pre-defined formal reasoning capabilities. Given one problem in natural language, we first transform it into a formal statement in Lean4 by interacting with the Lean4 compiler. Then, the formal statement will be used to generate a whole-proof and lemma-style sketch. If the whole-proof still fails to pass verification within a limited number of tool feedback rounds, the proof generated from the lemma-style sketch will be used instead for verification. In the rejection sampling phase, we will retain the trajectory that allows us to fully utilize the tools to perform auto-formalization, sketching, and proving.
Figure 3: The overview of the training pipeline of LongCat-Flash-Prover. We choose the LongCat Mid-train base model as the starting point, and then perform domain-mixed SFT to obtain a cold-start model. Then, we use the new cold-start model to refresh the prompts and trajectories through self-distillation and agentic RL, and repeat this process multiple times. After the iteration, we obtain our LongCat-Flash-Prover model.
Auto-FormalizationCombi-FormalMath-MathOlympiad-MiniF2F-ProofNet-Prover-Putnam-
BenchLiteBenchTestTestBenchBench
(Pass@8){}_{\text{(Pass@8)}}(Pass@8){}_{\text{(Pass@8)}}(Pass@8){}_{\text{(Pass@8)}}(Pass@8){}_{\text{(Pass@8)}}(Pass@8){}_{\text{(Pass@8)}}(Pass@8){}_{\text{(Pass@8)}}(Pass@8){}_{\text{(Pass@8)}}
Open-Weights Reasoning Models
DeepSeek-V3.265.095.285.697.581.883.046.7
Kimi-K2.584.097.991.198.488.291.782.8
Close-Weights Reasoning Models
Table 1: Auto-formalization performance (Pass@8 metric, %) of different reasoning and specific auto-formalizer models across multiple benchmarks. Best in bold , second in underlined .
Theorem-ProvingMathOlympiad-MiniF2F-ProofNetProver-Putnam-
BenchTestTestBenchBench
(Pass@32){}_{\text{(Pass@32)}}(Pass@32){}_{\text{(Pass@32)}}(Pass@32){}_{\text{(Pass@32)}}(Pass@32){}_{\text{(Pass@32)}}(Pass@32){}_{\text{(Pass@32)}}
Open-Weights Reasoning Models
DeepSeek-V3.214.777.920.442.85.8
Kimi-K2.57.576.619.944.31.2
Close-Weights Reasoning Models
Table 2: Theorem-proving performance (Pass@32 metric, %) of different reasoning and specific prover models across multiple benchmarks. Best in bold , second in underlined . †\dagger indicates the score is from external reports.
Theorem-ProvingMathOlympiad-MiniF2F-ProofNet-Prover-Putnam-
BenchTestTestBenchBench
Open-Weights Prover Models
Kimina-Prover-72B-87.7 † / 1,024---
w/ TTRL-92.2 † / UNK---
DeepSeek-Prover-V2-671B-88.9 † / 8,19237.1 † / 1,02459.1 † / 5127.1 † / 1,024
Self-play Theorem Proving-67.6 † / 2,56026.9 † / 2，560-1.2 † / 3,200
Table 3: Theorem-proving performance (with different larger budgets, %) of different specific prover models across multiple benchmarks. Best in bold , second in underlined . Each element aa / bb denotes to the accuracy aa with limited budget bb (i.e., Pass@ bb ). “UNK” means unknown of the specific budget. †\dagger indicates the score is from external reports. Because different models may have different budget calculations, we directly extract the results from the report instead of conducting our own evaluations. Therefore, some benchmark results may not be available.
Informal TasksPriorOurs
LongCat-Flash-LongCat-Flash-
Thinking-2601Prover
AIME-25 (Avg@16){}_{\text{(Avg@16)}}99.697.7
HMMT-25 (Avg@16){}_{\text{(Avg@16)}}93.490.8
IMO-AnswerBench (Avg@4){}_{\text{(Avg@4)}}78.677.3
AMO-Bench EN (Avg@16){}_{\text{(Avg@16)}}61.662.2
Table 4: Performance (%) comparison across multiple general reasoning benchmarks. Best in bold . The result indicates that our LongCat-Flash-Prover can retain the general reasoning ability.
Figure 8
Appendix figures & tables2 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 5: The workflow of agentic lemma tree search.
Pattern & DescriptionCode Example
Original Problem Definition Example: putnam_2025_b3 .⬇ import Mathlib open Finset theorem putnam_2025_b3 : (( True ) : Prop ) ↔\leftrightarrow ∀\forall S : Set N\mathbb{N} , S . Nonempty →\rightarrow ( ∀\forall n ∈\in S , 0 < n ) →\rightarrow ( ∀\forall n ∈\in S , ∀\forall d : N\mathbb{N} , 0 < d →\rightarrow d | (2025 ^ n - 15 ^ n ) →\rightarrow d ∈\in S ) →\rightarrow S = { n : N\mathbb{N} | 0 < n } := by sorry
1. Tampering with the Theorem Changing the proposition formalization into a trivial one with the same name, and proving the trivial proposition instead of the original one.⬇ import Mathlib open Finset -- Secretly change the theorem ‘ s proposition to a trivial tautology theorem putnam_2025_b3 : (( True ) : Prop ) ↔\leftrightarrow True := by rfl
2. Early Termination via #exit Using the #exit command to instruct the Lean compiler to stop processing the rest of the file, hiding the proof obligations.⬇ import Mathlib open Finset -- Terminate compilation early ; the compiler ignores everything below # exit -- The actual theorem signature is hidden in the ignored content theorem putnam_2025_b3 : (( True ) : Prop ) ↔\leftrightarrow ∀\forall S : Set N\mathbb{N} , S . Nonempty →\rightarrow ( ∀\forall n ∈\in S , 0 < n ) →\rightarrow ( ∀\forall n ∈\in S , ∀\forall d : N\mathbb{N} , 0 < d →\rightarrow d | (2025 ^ n - 15 ^ n ) →\rightarrow d ∈\in S ) →\rightarrow S = { n : N\mathbb{N} | 0 < n } := by sorry
3. Introducing Unproven Assumptions Using axiom or opaque definitions to introduce unproven assumptions that are leveraged to prove the target theorem.⬇ import Mathlib open Finset -- Introduce an absurd axiom axiom cheat_axiom : False theorem putnam_2025_b3 : (( True ) : Prop ) ↔\leftrightarrow ∀\forall S : Set N\mathbb{N} , S . Nonempty →\rightarrow ( ∀\forall n ∈\in S , 0 < n ) →\rightarrow ( ∀\forall n ∈\in S , ∀\forall d : N\mathbb{N} , 0 < d →\rightarrow d | (2025 ^ n - 15 ^ n ) →\rightarrow d ∈\in S ) →\rightarrow S = { n : N\mathbb{N} | 0 < n } := by -- Use the absurd axiom to prove the target exact False . elim cheat_axiom
4. Modifying or Adding Meta/Syntax Components Leveraging meta-programming components ( macro , elab , syntax , notation ) to bypass standard elaboration or suppress kernel errors.⬇ import Mathlib open Finset -- Secretly define a macro that expands ‘ trivial_proof ‘ to ‘ sorry ‘ macro ” trivial_proof ” : tactic => `( tactic | sorry ) theorem putnam_2025_b3 : (( True ) : Prop ) ↔\leftrightarrow ∀\forall S : Set N\mathbb{N} , S . Nonempty →\rightarrow ( ∀\forall n ∈\in S , 0 < n ) →\rightarrow ( ∀\forall n ∈\in S , ∀\forall d : N\mathbb{N} , 0 < d →\rightarrow d | (2025 ^ n - 15 ^ n ) →\rightarrow d ∈\in S ) →\rightarrow S = { n : N\mathbb{N} | 0 < n } := by trivial_proof
5. Bypassing Safety Checks Using unsafe or partial modifiers to bypass Lean’s termination checker or type safety mechanisms.⬇ import Mathlib import Aesop mutual -- Use ‘ unsafe ‘ to bypass termination checks and allow circular reasoning unsafe def solve_set_condition ( S : Set N\mathbb{N} ) ( h_ne : S . Nonempty ) ( h_pos : ∀\forall n ∈\in S , 0 < n ) ( h_div : ∀\forall n ∈\in S , ∀\forall d : N\mathbb{N} , 0 < d →\rightarrow d | (2025 ^ n - 15 ^ n ) →\rightarrow d ∈\in S ) : S = { n : N\mathbb{N} | 0 < n } := by -- Recursively invoke the main theorem to ‘ prove ‘ the sub - goal have h_main := putnam_2025_b3 . mp ( by trivial ) exact h_main S h_ne h_pos h_div -- Formulate a mutual dependency that never terminates but satisfies the type checker unsafe def putnam_2025_b3 : (( True ) : Prop ) ↔\leftrightarrow ∀\forall S : Set N\mathbb{N} , S . Nonempty →\rightarrow ( ∀\forall n ∈\in S , 0 < n ) →\rightarrow ( ∀\forall n ∈\in S , ∀\forall d : N\mathbb{N} , 0 < d →\rightarrow d | (2025 ^ n - 15 ^ n ) →\rightarrow d ∈\in S ) →\rightarrow S = { n : N\mathbb{N} | 0 < n } := by apply Iff . intro ⋅\cdot intro _ S h_ne h_pos h_div -- Delegate the proof to the mutually defined unsafe function exact solve_set_condition S h_ne h_pos h_div ⋅\cdot intro _ trivial end
Appendix
Table 6: Comprehensive Analysis of Lean 4 Cheating Behaviors and Detection Mechanisms
More in this topic

Large Language Model-Guided Theorem Proving

See all 40 papers

Explore similar work

CardsList
Jun 10, 2026

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both supervised fine-tuning (SFT) and sampling expensive. We introduce Pythagoras-Prover, a compute-efficient open-source family of Lean theorem provers built for practical compute budgets. The family spans two generation paradigms: autoregressive models at 4B and 32B parameters, and a first proof-of-concept diffusion-based prover (4B) that iteratively refines Lean proofs at inference time. For training efficiency, we build a Lean-verified corpus stratified into easy, medium, and hard problems for curriculum SFT, so models acquire proof skills progressively from shorter, simpler proofs to longer, harder ones. During SFT, a dynamic proof-reasoning filtering scheme preserves informative proof traces while keeping each instance within an 8k-token context budget. We also introduce Augmented Lean Formalisation (ALF), which expands scarce verified corpora into variants of formal statements, populated via self-distillation for extra training signal without formally verifying every mutated instance. By perturbing known problems while preserving their formal character, ALF reduces reliance on any statement's surface form. Empirically, Pythagoras-Prover-4B surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test (86.1% vs 82.4%) with ~167x fewer parameters, while Pythagoras-Prover-32B sets the open-source state of the art at 93.0% on MiniF2F-Test and solves 93 of 672 PutnamBench problems. We release MiniF2F-ALF, an ALF-mutated contamination-sensitive benchmark on which every evaluated model loses accuracy; here our 32B remains strongest and our 4B matches the prior state of the art, Goedel-Prover-V2-32B.

Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian +5

Imperial College London · University of Edinburgh · Nanyang Technological University +1

Automated Theorem ProvingEfficient Language Model TrainingLean Theorem Proving
AskPDF
May 17, 2026

OProver: A Unified Framework for Agentic Formal Theorem Proving

Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each iteration runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL. OProofs is built from public Lean resources, large-scale proof synthesis, and agentic proving traces, containing 1.77M Lean statements, 6.86M compiler-verified proofs, and serialized trajectories with retrieved context, failed attempts, feedback, and repairs. Across five benchmarks, OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.

David Ma, Kaijing Ma, Shawn Guo +7

M-A-P

Automated Theorem ProvingLean Theorem ProvingLLM Agent Training
AskPDF
Oct 4, 2026

AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness

Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Despite rapid progress, research-level proofs often depend on concepts missing from leading proof assistant libraries (e.g., Lean's Mathlib), and successful compilation does not guarantee that a translation preserves the theorem's meaning or the proof's reasoning. Furthermore, aligned NL-FL training data are scarce, and leading agents often rely on costly frontier models and manually engineered harnesses. To address the above issues, we present AIProver, an agentic framework for autonomous proof auto-formalization and proof synthesis (AFPS) that jointly post-trains a 119B open-weight language model and evolves its agentic, tool-calling harness with HarnessEvolve. Verifiers assess type correctness, proof completeness, and semantic correctness, returning rewards and diagnostic certificates that drive model fine-tuning and alternating reinforcement learning via symbolic feedback and HarnessEvolve, a certificate-driven evolutionary search over the whole harness control flow that re-tailors the harness to the updated model. For research-level training and evaluation, we introduce LoCoBench, 58.9k instances from Mathlib, CSLib, Mizar Math Library, and a bounded-arithmetic textbook, with a 771-instance validation split whose theorem-proof pairs have no public Lean formalization. Against 39 frameworks spanning AFPS agents, frontier LLMs, and coding agents, AIProver lifts pass@4 semantic correctness over its Leanstral-1.5 base from 15.7% to 36.7% and outperforms every other open-weight system and Aristotle. As a Claude Code and Codex skill, it lifts their semantic correctness from 41.9% and 34.1% to 79.8% and 62.4%, respectively. Further, it is also 24% cheaper than Numina-Lean-Agent, pushing the accuracy-cost frontier of research-level AFPS.

Prithwish Jana, Viet Bach Hoang, Logan Luna +9

Georgia Institute of Technology, USA · University of Pennsylvania, USA · Foothill College, USA +3

Mathematical Reasoning BenchmarksAutomated Theorem ProvingLean Theorem ProvingAutoformalization
AskPDF