leanerThe fine-tuning dataset
A proof can be correct and still have room to improve. Leaner turns that gap into training examples.
The benchmark produces two versions of a theorem’s proof: a reference adapted from Mathlib and a model-generated solution. Comparing them provides material for teaching a model to find a more direct argument, reuse a useful lemma, or express the same idea more clearly.
The current export contains 406 examples. The selection script keeps solutions recorded as passing, excludes those whose proof text contains the target theorem’s name, and requires the generated file to be at least 20 characters longer than its reference. That length difference is a practical selection rule, not a measure of mathematical quality; the name check is a heuristic, not a complete dependency audit.
For each selected pair, GPT-5.4 is asked for up to two short suggestions, phrased in the first person, to guide an improvement without giving away the reference proof. Each training example then pairs the request “Help me improve this Lean proof” and the generated Lean file with an assistant response containing the hints followed by the Mathlib reference file.
The data is stored as chat-format JSONL: one conversation per line, with a user message and an assistant message. The Lean files retain the imports and surrounding context needed to understand the theorem. This is a dataset for improving existing proofs; it is not a report of a fine-tuned model’s performance.
The broader project also preserves compiler diagnostics and their source positions. Those records can support future work on proof repair, although the current hint dataset is built from accepted solutions.
View the dataset Generation script
Based on the cached Leaner export. Mathlib-derived material retains its upstream licensing; consult the source repository before redistribution.