Problems come from the literature, after the training cutoff
Each problem is drawn from a research paper. For the private holdout, the paper must have been published after the training cutoff of the models under test, so the result cannot be in the model's training data even in informal form. For the public benchmark, the source is cited and the date recorded so a reader can judge exposure for themselves.
Written in Lean 4, reviewed twice
The statement is formalised in Lean 4 by a research engineer and reviewed by a second before it enters the library. A formalisation is accepted only when it compiles against the pinned toolchain, when a reference proof exists and checks, and when the reviewer agrees the formal statement says what the paper says. The reference proof is never shown to a model and never published for holdout problems.
The model receives the statement, not the file
The model is given the preamble and the theorem statement with the proof removed. It is asked to return only a proof body. It does not receive the reference proof, the reviewer's notes, or anything from any other problem in the set.
The harness assembles the file from its own copy of the statement
The proof body returned by the model is inserted into the harness's own copy of the theorem statement. Whatever the model returned around the proof body is discarded. This is the mechanism that matters most: a model cannot weaken the theorem, add a hypothesis, change a quantifier or redefine a symbol, because the statement it is checked against is never the one it wrote. Weakening is impossible by construction rather than detected afterwards.
Lean decides, and then the axioms are audited
The assembled file is compiled with the pinned Lean 4 toolchain and Mathlib revision in a sandbox with no network. If it compiles without errors and without any placeholder left in the proof, the proof is a candidate pass. Then the harness audits which axioms the proof ultimately rests on. A proof that depends on anything beyond the standard set is rejected, which closes the indirect routes to a false proof: an assumption smuggled into the body, or a step that asks the checker to trust compiled code rather than the kernel.
Correctness is decided by Lean, a free and open proof checker that Invigil does not own and cannot influence. We cannot make a failing proof pass, and a lab cannot make a passing proof fail.
Pinned toolchain, published transcripts
Every release names the exact Lean 4 version, the Mathlib commit and the harness commit. Every result publishes the full model transcript: the prompt as sent, the response as received, the assembled file, the compiler output and the axiom report. A third party with the same toolchain obtains the same verdict on the same transcript, without contacting us. For holdout results the transcripts are delivered to the customer; the problems themselves are not published.
The public set never touches the private set
The holdout lives on separate infrastructure with separate credentials. No problem appears in both sets. Canary problems are seeded into the holdout so that a leak would be detected in the next round of model outputs. Every contributor signs intellectual property assignment and non-publication terms before seeing holdout material, because the realistic leak is an author publishing their own work rather than an attack on the infrastructure.