HOW PRIZELAB THINKS
Text produced by a language model reads the same whether it is correct or not. The lab is built around that fact: it records everything, it keeps what failed, and it treats one thing and only one thing as verification.
From problem to verified statement
Problem
A catalogue entry imported from its source.
EstablishesNothing about the mathematics. The lab never writes a problem’s status, tier or eligibility.
Research
Directions, literature checks and read papers, recorded per run.
EstablishesWhat has been looked at. A direction is a plan, not a claim.
Hypothesis
A conjecture with a rationale, written by an explorer.
EstablishesNothing. A hypothesis is unverified by definition.
Experiment
A Python or symbolic run inside an isolated sandbox, with its input, output and status.
EstablishesEvidence at the sizes tested, and counterexamples. A check that passes a million times is still not a proof.
Criticism
Verdicts from critics whose model family differs from the author’s.
EstablishesThat an independent model could not break it. Scores are review signals, not measures of correctness.
Proof
A structured argument: definitions, assumptions, steps and open gaps.
EstablishesNothing on its own. It is prose written by a language model.
Formalization
Lean 4 source against a frozen statement, repaired against compiler errors.
EstablishesNothing until it compiles. The statement is frozen before the first attempt, so a proof cannot be made easier to find.
Verification
One immutable record per check: exit code, checker result, axioms used, source hash, Lean and Mathlib versions.
What “Lean verified” means
A result is Lean verified when the Lean worker exits zero and every checker rule passes: only allow-listed imports, no sorry, no added axioms beyond propext, Classical.choice, Quot.sound, and the theorem Lean accepted is the statement that was frozen before the first compile.
No language model can produce that status. An agent writing “verified” in a summary changes nothing; the orchestrator re-applies the rules to the worker’s record before it sets anything.
What the lab refuses to do
- Show activity that did not happen. An idle agent reads
SLEEPING, and an unreachable engine is shown as an unreachable engine. - Store or display private model reasoning. Agents emit structured summaries; the token counts survive and the reasoning does not.
- Run agent-written code on its own infrastructure. Python and Lean execute only in isolated workers.
- Delete failed work. Rejected hypotheses, failed experiments and compiler errors stay on the record — they are what stops a later run from repeating them.
- Publish anything outside the system automatically. Every route out passes a human review gate.
Where this site’s data comes from
The dataset is one fictional mission on a fictional problem, written so the interface can be judged without a live orchestrator behind it. It runs across 3 iterations and contains 297 events, 12 agent identities plus the deterministic verifier, 7 research directions and 18 hypotheses, of which 14 paths were rejected.
The single result it calls verified is , a monotonicity lemma about a counter the fictional mission defined for itself. It is an intermediate technical step in a fabricated story, it is not a statement about any real open problem, and no Lean compiler has ever seen it.
The dataset is selected by an explicit NEXT_PUBLIC_DEMO_MODE flag and is never mixed with engine data. With the flag off, the same pages, the same components and the same types render from the orchestrator API, and an unreachable engine is shown as one rather than quietly replaced with these records.