FLTEval

Agents complete the formal Lean proofs and define the new mathematical concepts in real pull requests to the Fermat's Last Theorem (FLT) formalization project. Lean and SafeVerify check each submitted diff.

Mistral introduced it with Leanstral in 2026-03 and open-sourced the harness with Leanstral 1.5 in 2026-07. The harness is shaped like SWE-bench and the repo ships a 162-instance sample.

Made by Mistral AI Released Mar 2026 Formal proofs All tasks public Last in a launch post Jul 2026 , dropped before it saturated Last model added Jul 2026

Level: Research frontier Researchers, on open problems or tasks that take days
Scored: Checked automatically A program checks the result against an answer key, unit tests or the expected final state.
Answers: Agent task Many steps in a terminal, browser, desktop, app, game or robot.

mistralai/FLTEval 8 stars mistral.ai

Models scored in lab cards

Launch posts list it, from 1 lab

System cards report it, from 1 lab

Leanstral 1.5 leads with 43.2

Best score per model as labs report them in their own cards. Labs pick their own settings, so these compare less cleanly than independent runs.

Bars Table

1 Leanstral 1.5 43.2
2 Leanstral 31.9

#	Model	Score	Setting	Date	Source
1	Leanstral 1.5	43.2		Jul 2026	Model card
2	Leanstral	31.9		Mar 2026	Model card

Scores over time

All the scores we have, one dot each, so a model tested at several settings appears more than once.

Reported by the lab in its model card

Labs headline it less often now, last in Jul 2026

Launch posts from every lab that has listed it, one tick per post. Tall colored ticks include it, and short gray ones leave it out.

Mistral AI

Date	Launch post	Score	As the post writes it
2 Jul 2026	Leanstral 1.5	43.2	FLTEval pass@8 43.2 (pass@1 28.9)
16 Mar 2026	Leanstral	31.9	FLTEval score, Leanstral pass@16 (pass@1 21.9)

2 system cards report it, from 1 lab

Besides launch posts, we read the system cards, model cards and technical reports labs publish with a release. They report far more, including safety and frontier-risk tests.

Date	Document	Score	As the document writes it	Section
2 Jul 2026	Leanstral technical report	31.9	FLTEval Leanstral 1.0 pass@16, cost $290. pass@8 31.0, pass@4 29.3, pass@2 26.3, pass@1 21.9 (Table 3)	Capabilities
2 Jul 2026	Leanstral 1.5 technical report	43.2	FLTEval pass@8, cost $216. pass@4 38.9, pass@2 34.6, pass@1 28.9 (Table 3)	Capabilities

Leanstral 1.5 leads with 43.2

Scores over time

Labs headline it less often now, last in Jul 2026

2 system cards report it, from 1 lab

More in Math