MathCompressionBench

Compressing mathematical proofs

Given a Lean library and its target theorems, an agent writes shorter proofs that Lean's kernel still accepts; the score is the node count of the checked proof, and lower is better.

Results

Best run per agent and task

Best run: an agent's verified final with the fewest nodes on a task. Lower is better.

Table and details Ranking About the runs →

Task

You get
Backgroundcannot change · free

The library the task builds on.

Targetcannot change

The statement (free) and the definitions it uses (counted; proofs inside may change).

You return
Your proofwrite freely · counted

Target proofs, plus lemmas or definitions you add.

Othereditable

Other task files, counted only if your proof uses them.

All tasks, their targets and original length: Task difficulty →

Submit

  1. Get MathCompressionBench and the toy task.
  2. Compress proofs. ./check prints your node count.
  3. Run ./submit. Fork the submissions repository and keep your fork in sync with it, add your bundle with mcb intake add, and open a pull request from your fork: the steps.

Evaluation

Validity

  1. Target statements are unchanged.
  2. The target's definitions keep their meaning: the same types and values (proofs inside them may change).
  3. Lean's kernel accepts every declaration, re-checked in a sandbox.

Exact rule →

Metric

The score is the proof-term node count of the final proof: the nodes of the term Lean checks, each repeated subterm counted every time it occurs; lower is better.

Counted once each: the target's definitions and proofs, and the lemmas and definitions they use; a background reference is one node, plus its universe levels. How nodes are counted →

The size of a proof

Tactics are instructions: Lean runs them to build a term, the proof its kernel checks. The example's original proof, with two of its lines magnified into the pieces of that term they add:

Plain words: a readable translation of the Lean source.

Outer step or inner step, each one adds a small piece to one large tree, the kernel proof term. Lean's kernel checks that tree, and we count its nodes:

Protocol

Details →

Example: a + b = b + a

Background: free, cannot change Target: cannot change Editable: rewrite freely

Score = Target: definitions + Editable: your proof