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

Jianing Wang; Jianfei Zhang; Qi Guo; Linsen Guo; Rumei Li; Chao Zhang; Chong Peng; Cunguang Wang

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

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

Panel of Figure 1 — 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-Formalization	Combi-	FormalMath-	MathOlympiad-	MiniF2F-	ProofNet-	Prover-	Putnam-
	Bench	Lite	Bench	Test	Test	Bench	Bench
	${}_{\text{(Pass@8)}}$	${}_{\text{(Pass@8)}}$	${}_{\text{(Pass@8)}}$	${}_{\text{(Pass@8)}}$	${}_{\text{(Pass@8)}}$	${}_{\text{(Pass@8)}}$	${}_{\text{(Pass@8)}}$
Open-Weights Reasoning Models
DeepSeek-V3.2	65.0	95.2	85.6	97.5	81.8	83.0	46.7
Kimi-K2.5	84.0	97.9	91.1	98.4	88.2	91.7	82.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-Proving	MathOlympiad-	MiniF2F-	ProofNet	Prover-	Putnam-
	Bench	Test	Test	Bench	Bench
	${}_{\text{(Pass@32)}}$	${}_{\text{(Pass@32)}}$	${}_{\text{(Pass@32)}}$	${}_{\text{(Pass@32)}}$	${}_{\text{(Pass@32)}}$
Open-Weights Reasoning Models
DeepSeek-V3.2	14.7	77.9	20.4	42.8	5.8
Kimi-K2.5	7.5	76.6	19.9	44.3	1.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-Proving	MathOlympiad-	MiniF2F-	ProofNet-	Prover-	Putnam-
Theorem-Proving	Bench	Test	Test	Bench	Bench
Open-Weights Prover Models
Kimina-Prover-72B	-	87.7 † / 1,024	-	-	-
w/ TTRL	-	92.2 † / UNK	-	-	-
DeepSeek-Prover-V2-671B	-	88.9 † / 8,192	37.1 † / 1,024	59.1 † / 512	7.1 † / 1,024
Self-play Theorem Proving	-	67.6 † / 2,560	26.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

a

b

denotes to the accuracy

a

with limited budget

b

(i.e., Pass@

b

). “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 Tasks	Prior	Ours
	LongCat-Flash-	LongCat-Flash-
	Thinking-2601	Prover
AIME-25 ${}_{\text{(Avg@16)}}$	99.6	97.7
HMMT-25 ${}_{\text{(Avg@16)}}$	93.4	90.8
IMO-AnswerBench ${}_{\text{(Avg@4)}}$	78.6	77.3
AMO-Bench EN ${}_{\text{(Avg@16)}}$	61.6	62.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.

Appendix figures & tables2 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 5: The workflow of agentic lemma tree search.

Pattern & Description	Code Example
Original Problem Definition Example: putnam_2025_b3 .	⬇ import Mathlib open Finset theorem putnam_2025_b3 : (( True ) : Prop ) $\leftrightarrow$ $\forall$ S : Set $\mathbb{N}$ , S . Nonempty $\rightarrow$ ( $\forall$ n $\in$ S , 0 < n ) $\rightarrow$ ( $\forall$ n $\in$ S , $\forall$ d : $\mathbb{N}$ , 0 < d $\rightarrow$ d \| (2025 ^ n - 15 ^ n ) $\rightarrow$ d $\in$ S ) $\rightarrow$ S = { 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 $\mathbb{N}$ , S . Nonempty $\rightarrow$ ( $\forall$ n $\in$ S , 0 < n ) $\rightarrow$ ( $\forall$ n $\in$ S , $\forall$ d : $\mathbb{N}$ , 0 < d $\rightarrow$ d \| (2025 ^ n - 15 ^ n ) $\rightarrow$ d $\in$ S ) $\rightarrow$ S = { 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 $\mathbb{N}$ , S . Nonempty $\rightarrow$ ( $\forall$ n $\in$ S , 0 < n ) $\rightarrow$ ( $\forall$ n $\in$ S , $\forall$ d : $\mathbb{N}$ , 0 < d $\rightarrow$ d \| (2025 ^ n - 15 ^ n ) $\rightarrow$ d $\in$ S ) $\rightarrow$ S = { 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 $\mathbb{N}$ , S . Nonempty $\rightarrow$ ( $\forall$ n $\in$ S , 0 < n ) $\rightarrow$ ( $\forall$ n $\in$ S , $\forall$ d : $\mathbb{N}$ , 0 < d $\rightarrow$ d \| (2025 ^ n - 15 ^ n ) $\rightarrow$ d $\in$ S ) $\rightarrow$ S = { 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 $\mathbb{N}$ ) ( h_ne : S . Nonempty ) ( h_pos : $\forall$ n $\in$ S , 0 < n ) ( h_div : $\forall$ n $\in$ S , $\forall$ d : $\mathbb{N}$ , 0 < d $\rightarrow$ d \| (2025 ^ n - 15 ^ n ) $\rightarrow$ d $\in$ S ) : S = { 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 $\mathbb{N}$ , S . Nonempty $\rightarrow$ ( $\forall$ n $\in$ S , 0 < n ) $\rightarrow$ ( $\forall$ n $\in$ S , $\forall$ d : $\mathbb{N}$ , 0 < d $\rightarrow$ d \| (2025 ^ n - 15 ^ n ) $\rightarrow$ d $\in$ S ) $\rightarrow$ S = { 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

Large Language Model-Guided Theorem Proving

See all 40 papers

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
Jun 10, 2026Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian +5Automated Theorem Proving Efficient Language Model Training
Imperial College London · University of Edinburgh · Nanyang Technological University +1
OProver: A Unified Framework for Agentic Formal Theorem Proving
May 17, 2026David Ma, Kaijing Ma, Shawn Guo +7Automated Theorem Proving Lean Theorem Proving
M-A-P
AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness
Oct 4, 2026Prithwish Jana, Viet Bach Hoang, Logan Luna +9Mathematical Reasoning Benchmarks Automated Theorem Proving
Georgia Institute of Technology, USA · University of Pennsylvania, USA · Foothill College, USA +3

Jun 10, 2026J/K move · Enter open · S save

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

Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu+4

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

Automated Theorem Proving Efficient Language Model Training Lean Theorem Proving

Open paper AskPDF arXiv

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.

Abstract

Large Language Model-Guided Theorem Proving

Explore similar work

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

OProver: A Unified Framework for Agentic Formal Theorem Proving

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