Invigil

The public benchmark

Published in full, so that a score means something.

The public benchmark exists to prove the method. Everything needed to reproduce a result is released together: the problems, the harness, the toolchain pins and the complete model transcripts. A reader does not have to trust our numbers. They can regenerate them.

A release

What a release contains

01

The problem set

Every Lean 4 statement, with its source paper, publication date, and the SHA-256 hash of the statement file as the harness holds it.

02

The harness

The code that prompts, assembles, compiles and audits. Published at a tagged commit.

03

The toolchain pins

The exact Lean 4 version and Mathlib commit. A verdict is only meaningful against a named toolchain.

04

The transcripts

For every model and every problem: the prompt sent, the response received, the assembled file, the compiler output and the axiom report.

05

The results

Pass counts per model, per problem, with the run date and the model version string as reported by the provider.

06

The release hash

A single hash over the whole bundle, so a later copy can be checked against the one we published.

Versioning

Sealed, numbered, never edited

Releases are numbered and sealed. A release is never edited after publication; a correction is a new release that points at the one it supersedes. The set of problems in a release is fixed before any model is run against it, and the hash of that set is published before the results are. That ordering is what makes the result a measurement rather than a selection.

Because the public set is public, it is contaminated for any model trained after its release. That is expected and stated. The public benchmark measures the method; the private holdout measures the models.

Reproducing

How a third party reproduces a score

1 · obtainDownload the release bundle and verify its hash against the one published here.
2 · pinInstall the named Lean 4 version and check out the named Mathlib commit.
3 · assembleFor any transcript, run the harness's assembly step on the recorded model response. The output must match the recorded assembled file byte for byte.
4 · checkCompile the assembled file and run the axiom audit. The verdict must match the recorded verdict.
5 · rerun (optional)Send the recorded prompt to the same model version yourself. Responses will differ; the verdict on your response is a new data point, not a replication.

Steps 1 to 4 require no contact with Invigil and no cooperation from any lab. That is the point.

Access

The current release

The current release bundle is available to research and evaluation teams on request, together with the reproduction instructions above. Ask for it here, stating your organisation and how you intend to use it. Requests from frontier laboratories, safety institutes and academic groups are answered first.