Primary evidence
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problemsS1 · Primary research · Paper · 2024-06-06
- Lean Workbook dataset releaseS1 · Primary research · Dataset
Lean Workbook releases a large formal-informal mathematics dataset
An iterative generation-and-filtering pipeline translates natural-language math problems to Lean 4 statements and back.
What happened?
Lean Workbook released about 57,000 formal-informal question pairs together with searched proofs and 21 new IMO questions.
Why it matters
The dataset lowered a key bottleneck for training larger Lean provers: the scarcity of aligned formal and informal mathematics.
Significance rationale: Lean Workbook expanded the supply of paired natural-language and Lean problems for training autoformalizers and provers.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Substantive AI support
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Informal, Formal, Hybrid
- AI contribution
- Models participate in synthetic translation and proof search used to construct the dataset.
- Human contribution
- Researchers designed the iterative data pipeline, filtering criteria and release.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- lean-workbook, lean
- Organizations
- shanghai-ai-laboratory
- Problems
- formalization-data
- Methods
- synthetic-data, autoformalization, proof-search
Sources & artifacts
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problemsS1 · Primary research · Paper · accessed 2026-09-10
- Lean Workbook dataset releaseS1 · Primary research · Dataset · accessed 2026-09-11
- Lean Workbook formal-informal datasetArtifact · Dataset
Verification history
- 2024-06-06 · Paper released · E2 · Research record
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
This corpus refresh added a directly inspectable public artifact maintained by the authors or releasing organization. E3 records artifact-level inspectability and does not imply independent verification of the underlying scientific or mathematical claim.
Corrections
No corrections recorded.