Task difficulty
How far each task's original has been compressed, and how much of that the organizer's sharing pass alone removes. Per-target sizes measured .
Length ladder
Log scale; a line at each power of ten; darker is longer. Bubble size grows with the number of targets.
From the original to the best verified final
┃ original node count · ◆ after the organizer's automatic sharing pass · ● smallest verified final known; log scale. ◆ to ┃: removed by the organizer's sharing pass; ● to ◆: everything else, including agents' own sharing programs. No ◆: no published measurement. Only ┃: no runs yet. Lengths are node counts under MathCompressionBench's scoring, not a measure of mathematical difficulty.
By task
Scroll sideways for every column.
Per target, in proof-term nodes; — : not measured.
What the columns mean
| Targets | The theorems the task asks for (target). |
|---|---|
| Original proof | The target's proof term, the helpers only its proof reaches, and a 1/k share of each helper that k targets' proofs reach (helper). The 1/k split is this page's reporting convention for attributing a task's nodes to its targets: the score charges each helper once per task and never splits it. With it, a task's original proofs and its statement side add up to the original's node total, up to rounding. |
| From shared helpers | The nodes charged as 1/k shares ÷ all original proof nodes of the task. This is node-weighted, not a median. |
| After the sharing pass | The original proof after the sharing pass, a fixed program run by the organizer that writes each repeated subterm once (sharing pass). It is shown where the chart has ◆. |
| In the best verified final | The target's size in the chart's best verified final, not the best the target reached in any run. The toy's joint run was not measured per target. |
| Statement | The target's statement plus the task's own declarations it reaches, including proofs inside those definitions and instances. A library constant costs one node per use plus its universe levels (what is free). The statement itself is free in the score, and a definition several statements reach is counted in full in each of them, so statements do not add up to a task total. |
| Library lemmas per proof | Distinct library theorems the proof and its helpers mention (background). |
| Background | The library the task builds on is free of charge. It is Mathlib, or core Lean only (background). |
Other terms
| Proof-term nodes | The size of a kernel proof term, the score's unit (how nodes are counted). |
|---|---|
| Target | A theorem the task asks for (target). |
| Original | The proof the task provides. Its node count, the chart's ┃, is the task's baseline score: all its targets' proofs plus the charged definitions their statements reach. |
| Best verified final | The smallest final known for the task that MathCompressionBench's verifier accepted, the chart's ●. The chart names where it comes from. |
| Reaches | A declaration reaches the constants its statement and proof mention, and everything those reach (what is charged). When the original is split by target, a proof's reach is not followed into another target, which it names at the cost of a reference, or into a definition some statement reaches, which stays on the statement side. Every node is therefore charged to one place. |
| Statement side | The task's own charged definitions that its targets' statements reach, with the proofs inside them, each counted once. These are the original's nodes that no proof is charged for. |
| Organizer | The people who run MathCompressionBench. They publish its tasks, run the sharing pass and sign the receipts. |
| Extra examples | Rows not in lcbench-v1 and not ranked: the toy, a small prototype task on natural numbers defined from scratch in core Lean (worked example); and, as demonstrations, the fundamental theorem of arithmetic (worked example) and two tasks from a published Lean formalization of Fermat's Last Theorem, each on its own versions of Lean and Mathlib. FLT, small exponents n = 5, 7, 11, 13: the four classical small-exponent cases on its proof path, the smallest part of that proof that needs only Mathlib. Fermat's Last Theorem, whole project: one target, fermat_last_theorem, charged with everything its proof reaches; shown by its original only, with no runs yet. |