leanerHow the benchmark works
Leaner starts with existing mathematics, asks a model to reconstruct the proof, and uses Lean to check the result.
Building the problems
The project extracts theorem declarations from Mathlib into standalone Lean files. Each file imports Mathlib, preserves the surrounding variable declarations, and adapts names where needed so the reference proof can compile. Verified recreations are collected as benchmark targets; the selection pipeline uses a minimum reference proof-body length of 35 characters. The cached batch contains 1,513 targets.
The workspace pins both Lean and Mathlib to v4.29.0. This first batch is a selected collection of theorems, not a random or comprehensive sample of Mathlib.
Generating and checking a proof
For each target, the solver replaces the proof body with sorry and asks gpt-5.4 to return a complete Lean file. The first request includes the theorem statement and its context, but not the reference proof.
The candidate is checked by the Lean language server. If the server reports an error, its diagnostics—including source locations and highlighted text—are returned to the model for another attempt. The solver allows up to three attempts and stops at the first accepted candidate. It saves the final Lean file, the conversation transcript, and a pass/fail record with the attempt count.
Reading the result
The cached results log records 811 passes and 702 failures, giving 53.6% acceptance across 1,513 problems. Of the accepted solutions, 435 passed on attempt one, 242 on attempt two, and 134 on attempt three. The headline result includes retries with compiler feedback; it is not a first-attempt score.
The project README lists 713 failures alongside 811 successes and 1,513 proofs. Those numbers are inconsistent, so the GPT-5.4 result on this site uses the cached per-problem log as the source of truth.
What this run does—and does not—measure
The recorded pass criterion is the absence of compiler errors. The checker does not separately reject warnings about sorry or enforce that the model has preserved the theorem statement. Every target also imports the full Mathlib library, which can make the original theorem available to the model. Compiler acceptance alone therefore does not establish an independent proof of the intended problem.
The CSV export flags 128 of the 811 passing responses as containing the target theorem’s name in their proof text. That check is a useful signal of possible theorem reuse, but it is only a text heuristic. The headline score includes those responses. A stricter future evaluation would need to check theorem preservation, exclude admitted proofs, and prevent direct or indirect access to the target result.
The front-page example was selected separately: Associated.exists_mem_finset_dvd.lean is recorded as passing on attempt two, contains no sorry, preserves the target statement, and constructs an induction proof without calling the target theorem. Both the reference and generated files were also rechecked with the pinned Lean compiler for this site.
From evaluation to training data
Selected accepted proofs are paired with their Mathlib references and short improvement hints. The current export has 406 conversations. The dataset page explains the selection criteria and message format.