AI4Math ChronicleAI4Math 大事记

OpenAI's Lean prover uses expert iteration to solve formal Olympiad problems

The prover alternated proof search with retraining on newly discovered proofs over statements of varied difficulty.

What happened?

OpenAI reported 41.2% on miniF2F and automatic proofs of challenging AMC/AIME and two IMO-adapted problems using statement curriculum learning in Lean.

Why it matters

It connected language-model theorem proving with expert-iteration ideas that later became central to formal reasoning systems.

Significance rationale: The work showed that proof search interleaved with learning could create its own curriculum and reach a new state of the art on miniF2F.

Historical context

Earlier developments
Later developments

—

Related milestones

—

Primary evidence

Evidence & status at a glance

Significance
H2 · Field milestone
Verification
Paper released
Evidence level
E2 · Research record
AI role
AI primary, human verified
Formal assurance
Machine-checked

How should these labels be read? →

Contribution & verification

Mathematical novelty
Benchmark result
Interface
Formal, Symbolic
AI contribution
The neural prover searched for Lean proofs and used successful proofs as new training data.
Human contribution
Researchers curated statements, designed the expert-iteration loop and evaluated generated formal proofs.
Verification
Paper released · E2 · Research record · Machine-checked
Last reviewed
2026-09-11

Technical details

Systems
lean-statement-curriculum-prover, lean
Organizations
openai
Problems
minif2f, olympiad-mathematics
Methods
expert-iteration, proof-search, language-model

Sources & artifacts

Verification history

  • 2022-02-02 · 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.

Corrections

No corrections recorded.