Primary evidence
- MizAR 40 for Mizar 40S1 · Primary research · Paper · 2013-10-10
MizAR 40 scales AI/ATP methods across the full Mizar Mathematical Library
The system scaled fast learned relevance methods over roughly 150,000 MML formulas and deployed them within the MizAR online reasoning service.
What happened?
The 10 October 2013 paper reported an AI/ATP system that automatically proved 40% of the theorems in the then-current Mizar Mathematical Library within 30 seconds on a 14-CPU machine.
Why it matters
The work made corpus-scale formal mathematics a practical target for integrated machine learning and automated reasoning rather than a small benchmark exercise.
Significance rationale: MizAR 40 demonstrated that a suite of learned premise-selection and ATP methods could operate at the scale of the entire Mizar Mathematical Library, turning large formal mathematics into an online AI-assisted reasoning service and corpus-wide evaluation surface.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Autonomous primary role
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Benchmark result
- Interface
- Formal, Symbolic
- AI contribution
- Learned relevance methods selected useful formulas and ATP systems attempted proofs across the library at scale.
- Human contribution
- Researchers engineered and optimized the learning methods, ATP portfolio, Mizar translations and online service.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- mizar, mizar40, mizar-online-reasoning
- Organizations
- university-of-innsbruck
- Problems
- large-theory-theorem-proving
- Methods
- machine-learning, premise-selection, automated-theorem-proving, large-theory-reasoning
Sources & artifacts
- MizAR 40 for Mizar 40S1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 2013-10-10 · Paper released · E2 · Research record
The arXiv paper establishes the system and reports the corpus-scale evaluation; Chronicle does not treat the percentage as independently reproduced.
Corrections
No corrections recorded.