A compiling file is not a proof of your theorem
Give a model a theorem and ask it to return a complete Lean file. Check whether the file compiles. Count a pass. This is how most formal-reasoning evaluations work, and it has a hole large enough to drive a leaderboard through: the model wrote the theorem statement too. It can add a hypothesis that makes the result trivial. It can replace a universal quantifier with an existential one. It can shadow a definition from the library with a weaker one of its own. It can declare an assumption of its own. Every one of these produces a file that compiles, and none of them proves what was asked.
Some of these are caught by a careful human reading the output afterwards. Most evaluations do not have one. None of them should need one.
Keep the statement, take only the proof
The Invigil harness asks the model for a proof body and nothing else. Whatever comes back, the harness inserts it into its own copy of the theorem statement and discards the rest. The model is then checked against the statement we hold, which it has never had write access to. Weakening the theorem is not detected; it is impossible. There is nothing to weaken.
Then the axiom audit. Lean can report every axiom a theorem ultimately rests on. A legitimate proof rests on at most the standard set. A proof that rests on anything else has smuggled in an assumption, whether by declaring one outright or by asking the kernel to trust compiled code. Both are rejected.
The verdict has to be the checker's, not ours
With those two mechanisms the pass verdict is entirely Lean's. Invigil does not judge proofs, does not read them for reasonableness, and cannot be argued with about grading, because there is no grading. A lab that disagrees with a verdict can take the transcript, the pinned toolchain and the harness, and obtain the same verdict on its own machine. That is a harder standard than any human-graded benchmark can meet, and it is the whole reason the number is worth paying for.