Loading
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.
A catalogue entry imported from its source.
EstablishesNothing about the mathematics. The lab never writes a problem’s status, tier or eligibility.
Directions, literature checks and read papers, recorded per run.
EstablishesWhat has been looked at. A direction is a plan, not a claim.
A conjecture with a rationale, written by an explorer.
EstablishesNothing. A hypothesis is unverified by definition.
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.
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.
A structured argument: definitions, assumptions, steps and open gaps.
EstablishesNothing on its own. It is prose written by a language model.
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.
One immutable record per check: exit code, checker result, axioms used, source hash, Lean and Mathlib versions.
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.
SLEEPING, and an unreachable engine is shown as an unreachable engine.This deployment reads the orchestrator API. Every status, event and figure on the site comes from a row the engine wrote, and nothing is filled in when a field is missing.
A demo dataset exists for development and for showing the interface without a live engine. It is selected by an explicit flag, it is labelled on every screen it feeds, and it is never used as a fallback when the API cannot be reached.