Rules and scoring

What cannot change, what is scored, what is valid.

In short
Tasks
Score
Validity
Your tools
How every run was checked
Which file is scored
Kinds of change
Glossary

In short

A task	Target theorems in a Lean library; you compress their proofs.
Cannot change	The background, and the target (its statements and the definitions they use; proofs inside those may change). Editable: everything else.
Counted once each	The target proofs and every non-background declaration they reach, statement and proof (an inductive type with its constructors and recursor).
Free	Target statements, library references (one node each, plus universe levels), running tactics.
Valid	The kernel re-checks everything. Statements and definitions stay unchanged. Only allowed imports and axioms may be used.
Score	N_final; fewer wins.

Tasks

Scroll sideways for every column →

Exact definition

Score: proof-term node count

The score is the number of nodes in the kernel proof terms of everything charged. Fewer wins.

The formula, sum by sum

N = Σ_{targets t} N(proof t) + Σ_{lemmas, definitions d} [ N(statement d) + N(body d) ] + Σ_{inductive types I} [ N(type I) + Σ_{constructors c} N(type c) + N(I.rec type) + Σ_{rules r} N(r) ]

What is charged

Kind	What counts	For example
Target proofs	Only the proof of each target theorem; its statement is free.	`theorem target … := by rw […]`: the term `rw` leaves
Helper lemmas	Every lemma in the task's files that a charged proof uses, directly or indirectly: statement and proof, once however often it is used.	`theorem double (n : Nat) : n + n = 2 * n := …`
Definitions used	For definitions, instances and structures in the task's files that a statement or proof uses, we count the type and value once. Those a statement uses are the target's definitions. Proofs inside them may change.	the toy task's `def add : MyNat → MyNat → MyNat` and `instance : Add MyNat`, used by its statements through `+`
Declarations Lean generates	Equation lemmas (`f.eq_1`), auxiliary proofs (`_proof_1`), `match` and `casesOn` definitions are charged like any declaration when something charged uses them.	`rw [f]` uses `f.eq_1`
Inductive types	Using the type, any constructor or a projection charges the type, every constructor and its recursor. Each pays its type, and the recursor also pays its rules, one per constructor.	`inductive MyNat \| zero \| succ (n : MyNat)`: see below

An inductive type, expanded

For an inductive type Lean generates its recursor MyNat.rec, the principle of proof by induction and definition by recursion. Its rules say what it computes on each constructor: MyNat.rec z s zero = z and MyNat.rec z s (succ n) = s n (MyNat.rec z s n). The table gives the counter's numbers for this file.

Other generated declarations, such as MyNat.casesOn, count only when something charged uses them.

How the nodes of a term are counted

Each kernel node costs as below, plus its children.

Kernel constructor	Counts as
`f a` (application)	1 + N(f) + N(a)
`fun x : T => b`, `∀ x : T, b`	1 + N(T) + N(b)
`let x : T := v; b` (also `have`)	1 + N(T) + N(v) + N(b)
constant `c.{u}`	1 + nodes of its universe levels; the name's length is free
`Sort u`	1 + nodes of u
projection `e.i`	1 + N(e)
bound variable; literal (any size)	1
metadata wrapper; binder names and binder info	0
a subterm that occurs twice	counted twice
example: `@congrArg.{1,1} MyNat MyNat n m succ ih`	17

The example, node by node

applications, one per argument: 6
congrArg.{1,1}: 1, plus 2 for each universe level 1 (successor of zero): 5
MyNat, twice: 2
n, m (bound variables): 2
succ: 1
ih (bound variable): 1
total: 17

The counter gives the same 17 for this term, the proof of succ_congr in the inductive example above without its three binders.

A whole proof, node by node: zero + n = n

A three-line induction on the toy task's MyNat:

Every node costs one: a name, a variable, a fun, and each argument a function is applied to. A name also pays for its universe level nodes (.{0}: one, .{1}: two). Open a part to see every node.

What is free

Library	A reference to a background constant costs one node per use, plus its universe levels. Its own proof is never counted.
Target statements	The statements of the targets.
Tactics, metaprograms	Running them costs nothing. Only the terms they leave are counted, and those are often large.
Kernel computation	What the kernel evaluates while checking (for example `decide`) is not counted. Only the per-declaration heartbeat limit applies.
Names	Names of constants, binder names and binder info.
Literal size	A number or string literal is one node, whatever its size.

A complete example

The counter measures one target using a helper lemma twice and a library lemma once.

Comparing runs

Combining runs

On each task an agent's result is its best run: the smallest verified final node count among its runs. Agents are ranked on each task by it, fewest nodes first; an agent with no verified run on a task ranks last there, and tied agents share the average of the places they take: two agents tied for first both rank 1.5, and agents without a verified run on a task share the last places the same way. The overall ranking is the average rank over the tasks, each task weighted equally; lower is better. Tables count runs without a verified score under “No score”.

A real run: .

Validity

Any failed check means rejection without a score.

Kernel replay	Lean's kernel re-checks every declaration
Statements	identical to the original
The target's definitions	Each definition a statement uses is part of the target: its type and value (and those of everything it depends on in the task, proofs inside excluded) must hash to the recorded value. `./check` and the verifier both reject a change; the verifier's message “frozen definition changed” means one of the target's definitions changed. No proof is ever compared.
Imports	editable files and the task's pinned background only
Axioms	`propext`, `Quot.sound`, `Classical.choice` only (no `sorry`, no `native_decide`)
Limits	kernel heartbeats per declaration decide the verdict. Memory and wall clock only stop a check, without a verdict
Allowed	any Lean code, metaprograms included; any proof may change, even one inside the target's definitions

Your tools: `./check` and `./submit`

`./check`	Builds your files with the task's pinned Lean toolchain, replays every editable file in Lean's kernel within the kernel heartbeat limit per declaration, checks the rules above and counts the nodes. The official verification runs the same code. Nothing is sent anywhere.
It prints	The task and its sha256, the scorer version, then the verdict, valid or invalid, with your node count and the original's, followed by a line that compares the two. `--verbose` also lists what each declaration pays; `--json` prints the result as JSON.
It fails when	A rule is broken: the verdict is invalid, with one line per problem, such as a changed target statement or target definition, an import or axiom that is not allowed, a declaration over the kernel heartbeat limit or a failed build, then the end of Lean's log (exit status 1). A safety limit (wall clock, memory, processes, disk) stops a check with no verdict (exit status 3). Time and memory never decide validity.
`./submit`	Checks again, then writes your bundle, `submissions/submission-<first 16 hex digits of its ID>.tar.gz`: your editable sources, the kernel terms they compile to, the node count and hashes, and the run's budget and time elapsed. `--log DIR` adds your log, `--tokens-json FILE` your token usage, `--track agent\|record` the kind of run (an agent alone, or any means), which decides the leaderboard tracks it can count on: `open`, and for an agent run within 60 or 120 minutes `agent-60` or `agent-120`. Nothing is sent anywhere.
It prints	The check's result, the bundle's path, its submission ID (the bundle's sha256) and how to submit it: a pull request that adds the bundle to the submissions repository.
It fails when	The check is invalid (“refusing to bundle an invalid submission”, exit status 1), a safety limit stopped the check (no bundle, exit status 3), or `--log` is not a directory or `--tokens-json` not a JSON object (exit status 1).

How every run was checked

MathCompressionBench's verifier re-checked every run's scored file in its sandbox.

Which file is scored

Verified test submissions (receipts)

Kinds of change

Glossary

Target	A theorem the task names, with the definitions its statement uses (target definitions). You compress its proof; its statement, and the types and values of those definitions, must stay exactly as they are.
Helper	A declaration in the task's own files, other than a target, that a target reaches: your lemmas, the task's definitions and what Lean generates for them.
Background	The libraries the task imports, such as Mathlib or Lean's core library. They are free to use and never edited.
Target definition	A definition, instance or structure that a target's statement uses, and part of the target. Its type and value must stay the same. Proofs inside it may change (validity).
Kernel	Lean's small trusted checker. It re-checks every declaration of a submission, and the terms it checks are what is counted.
Heartbeat	Lean's unit of checking work: a count of small memory allocations, the same on every machine. Each declaration must pass within the task's kernel heartbeat limit.
Universe level	The level of a `Sort` (`Prop` is `Sort 0`, `Type` is `Sort 1`), also given to constants such as `congrArg.{1,1}`. Zero and a level variable are one node each. Each successor adds one, so `1` is two nodes.
Recursor	The eliminator Lean generates for an inductive type, such as `MyNat.rec`, for induction and recursion over that type. Its rules, one per constructor, say what it computes on that constructor.
Automatic sharing pass	A fixed program of MathCompressionBench that writes each repeated subterm of the original proofs once (with `let`) and changes nothing else. It is a reference point, not an agent.
Receipt	The signed record MathCompressionBench's verifier writes when it checks a submission: its verdict, node count and hashes. A receipt file's sha256 identifies it. Its root hash is one sha256 chained over the task, the submission, its sources, the counted terms, the scores, the verdict and the verifier. Changing any of them changes the root hash.
Scorer version	The version of MathCompressionBench's checking and counting code: a release number, or a release candidate before the release. Every check names the version it used.
Study's first check	The check the study ran on each run's final during its experiments, with the checker it used then, not MathCompressionBench's verifier. A final it rejected could still count as valid when a second check of the same, unchanged file accepted it.
Failed, unconfirmed	The study's verdicts on runs without a valid final. Failed: the final source failed a check or did not build. Unconfirmed: the study's records show no checked final source. Both mean no score in the study. This site checks each run's scored file again (which file is scored).
Agent	A model with its harness and reasoning effort: .
Harness	The program that runs a model as an agent. It hands the model the task files and tools and runs the commands the model asks for.
Sharing metaprogram	Lean code an agent writes into its submission that, like the automatic sharing pass, writes each repeated subterm once; allowed, and only the terms it leaves are counted.
Task package	The files a participant gets for a task: the Lean project with its editable files and the scripts that check and score it.