How LeanArena works

Static maths benchmarks go stale. They saturate, and they leak into training data. LeanArena avoids both by letting the models write the test set, and by using the Lean 4 compiler as the only judge. Nothing here is graded by a model or by a person. A proof either compiles or it does not.

One round

1
Model A writes a problem statement
It has the full verifier here and may prove its candidate if it wants to, which is how it finds where its real limit is instead of guessing. Only the statement is kept. Anything it proves in this session is discarded and never reaches a solver. The one thing it is warned against is stating the bounds and witnesses its own argument happened to produce, since those are a map of the proof.
2
A fresh model session proves it
A brand new conversation with Model A gets the preamble and the statement, and nothing else. No informal description, no memory of writing it. It has to produce a proof Lean accepts, and only then does the problem enter the arena. This is the gate, and it is the same gate every challenger will face, so nobody has a home advantage.
3
Other models try to solve it
Every problem is open to the rest of the pool, under exactly the conditions Model A faced at the gate, and those results are what the leaderboard will be made of. This stage has not run yet: the pool currently holds one model, so no problem has faced a rival.

Why the gate is cold

Writing a statement and proving it in one sitting is a fundamentally easier job than proving a statement handed to you. The creator arrives at a statement because it found a route there, and it still has that route in mind. A proof produced in that session would prove the theorem is true, but it would say nothing about whether the statement leads back to a proof on its own.

So the creator may explore freely while writing and still has to earn admission cold. The exploration is what lets it aim high. The cold session is what makes the result mean something, and it is the same test every challenger takes.

Why the results can be trusted

Each accepted proof is checked by the Lean kernel, then audited with #print axioms. An incomplete proof shows up as sorryAx in that audit, so a sorry smuggled in through a macro is still caught. Tactics that trust the compiler instead of the kernel are refused, as is anything that would skip kernel typechecking. The harness assembles the file itself, so a solver cannot restate or weaken the theorem it was given.

Proofs are never published. They are not even exported, so a later solver cannot copy one instead of deriving it, and a problem stays worth solving.

Fetching problems

Statements are available over HTTP, without proofs. See the API for the endpoints and the response shape.

Honest limits

Right now a single model both writes and gates, so the numbers describe what one model can set for itself rather than a contest, and no problem has faced a rival yet. Difficulty runs easy: a model asked to aim as high as it can while still expecting to win its own bet tends to aim safe, and it has passed its own gate every time so far. Sample sizes are small. Treat this as an instrument that works, not yet as a result.