Primary evidence
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level MathematicsS1 · Primary research · Paper · 2023-02-24
- ProofNet benchmark and replication repositoryS1 · Primary research · Repository
ProofNet benchmarks autoformalization and proving of undergraduate mathematics
The benchmark covers analysis, linear algebra, abstract algebra, topology and other textbook mathematics.
What happened?
ProofNet introduced 371 undergraduate-level examples pairing natural-language theorem statements and proofs with Lean 3 formal statements.
Why it matters
It created a shared target for measuring whether models can translate ordinary mathematical prose into proof-assistant representations.
Significance rationale: ProofNet broadened evaluation beyond Olympiad statements to textbook-level undergraduate mathematics and paired informal statements, proofs and Lean formalizations.
Historical context
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Computation only
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Informal, Formal, Hybrid
- AI contribution
- Models are evaluated on autoformalization and formal proving tasks built from the benchmark.
- Human contribution
- Researchers curated textbook problems, natural-language proofs and corresponding Lean statements.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-14
Technical details
- Systems
- proofnet, lean
- Organizations
- yale, carnegie-mellon-university
- Problems
- undergraduate-mathematics
- Methods
- benchmarking, autoformalization
Sources & artifacts
- ProofNet: Autoformalizing and Formally Proving Undergraduate-Level MathematicsS1 · Primary research · Paper · accessed 2026-09-10
- ProofNet benchmark and replication repositoryS1 · Primary research · Repository · accessed 2026-09-11
- ProofNet benchmark and replication codeArtifact · Dataset
Verification history
- 2023-02-24 · 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.