Meituan’s LongCat team has open-sourced a model specifically designed for mathematical theorem proving: LongCat-Flash-Prover.

Mathematical theorem proving isn’t just about getting the right answer; it requires every logical step to be strictly verifiable, with no room for ambiguity.

The LongCat team’s approach breaks the proof into three steps:

First, translate natural language into Lean4 formal language, then draft to break down big problems into small lemmas, and finally, step-by-step complete the proof.

And they discovered something interesting: AI cheats.

To fool the compiler, the model secretly changes the problem, inserts termination symbols, or even fabricates axioms.

So they specifically developed a syntax analyzer to catch 9 types of cheating methods, which is quite amusing.

The results are also impressive: MiniF2F-Test achieved 97.1% with only 72 inferences, and the competition-level MathOlympiad-Bench reached 46.7%.

Both are SOTA among open-source models.

Open Source Address: https://github.com/meituan-longcat/LongCat-Flash-Prover

<p style="margin-left: 8px