MathAtlas - Definitions: leaderboard
Metric: Correctness (%; share of all definitions whose Lean 4 formalization compiles against Mathlib (Lean v4.24.0) and is judged faithful to the informal text by CriticLean-32B; zero-shot prompt). Source: arxiv.org. Saturation forecast: Around 2029. 2 models tracked.
Top models
| # | Model | Score |
|---|---|---|
| 1 | GPT-OSS-120B | 6.6 |
| 2 | GPT-OSS-20B | 2.2 |
Interactive version: theaggregate.ai/benchmark?slug=mathatlas-definitions · How It Works · Data refreshed daily, snapshot 2026-09-26.