AI Proof Verification: A Verifier Supply-Chain Drill

OpenAI released ten mathematical and theoretical-computer-science results on August 1, each accompanied by a manuscript, a reasoning walkthrough, and a Lean certificate. On the same day, Lean’s creator published a postmortem explaining how an AI-assisted, sorry-free disproof of the Collatz conjecture had recently passed both the official Lean kernel and an old version of an independent checker because the two implementations contained different bugs.

Those events do not cancel each other out. The Collatz artifact does not show that formal proof is useless, and the ten new certificates do not show that expert review is finished. Together they expose a more useful product lesson: a certificate is an executable claim whose meaning depends on the exact verifier supply chain that accepted it.

That lesson extends beyond mathematics. Small teams increasingly receive AI-generated outputs with a green signal attached: a schema validation, a policy check, a signed provenance record, a test suite, a static-analysis result, or a machine-generated audit. The green signal is valuable. It is not self-interpreting. You still need to know which artifact ran, which checker ran, which dependencies it loaded, whether an independent path was genuinely independent, whether known-bad inputs fail, and what happens when a checker is patched.

The product risk appears when that signal authorizes the next irreversible step: publishing a claim, moving money, migrating data, or removing human review.

For this field note, I cloned OpenAI’s public ten-proofs repository at commit 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6, inspected its toolchain and dependency locks, installed its pinned Lean 4.32.0 toolchain in an isolated temporary directory, downloaded the mathlib cache, and built the MulticolorTriangleRamsey target successfully. Lake reported 8,656 completed jobs after retrieving 8,639 cached files.

That is a native replay, not an independent verification. I did not run Comparator because its documented trusted environment requires landrun, a Linux sandboxing dependency, while this run used macOS. The correct receipt is therefore “native replay passed; independent checker not run,” not “proof independently verified.” The distinction is the point of the drill below.

What happened: two releases, one trust question

OpenAI says its internal Astra model generated arguments for ten long-open problems across geometry, coding theory, group theory, complexity, cryptography, and combinatorics. Humans and the same model prepared manuscripts, after which the model formalized each argument as a Lean certificate. OpenAI also states that it takes responsibility for correctness while inviting the mathematical community to examine the results (official release). Those are consequential, checkable artifacts—not proof that every result has completed independent scholarly review.

The public certificate repository is unusually useful because it exposes more than PDFs. It pins Lean 4.32.0, records exact dependency revisions in lake-manifest.json, names the main declarations and permitted axioms in formalization.yaml, and supplies Comparator challenges. Its manifest reports zero sorry placeholders for the listed main results. That makes the release inspectable.

The Lean incident supplies the necessary boundary. According to Leonardo de Moura’s official postmortem, a July 25 AI-assisted Collatz “disproof” exploited a kernel implementation bug involving phantom parameters in nested inductive types. On July 28, the artifact was reduced to a proof of False, issue #14576 was opened, and a fix was pushed about an hour later. The frontend would reject the ill-typed construction; direct metaprogramming could reach the vulnerable kernel path.

The same artifact also passed an older nanoda checker. The postmortem says this required a separate projection-type-name bug in that checker, already fixed before the Lean bug was reported. This was not one shared line of code failing twice. It was a rare composition of two implementation defects and stale verifier versions.

The useful question for a product team is not “Can formal verification be trusted?” It is narrower:

What evidence do we require before promoting a machine-checkable artifact from “accepted somewhere” to “release evidence we can defend and later revoke”?

Define five states instead of one green check

Teams often compress every successful command into verified=true. That boolean destroys important information. Use five states:

State	Minimum evidence	What you may say	What you may not say
Received	Artifact and source location preserved	“We received a certificate”	“It is valid”
Pinned	Artifact, verifier, dependencies, and config have immutable identities	“The verification environment is reproducible in principle”	“We reproduced it”
Native-replayed	The producer’s intended checker path passes in your environment	“The pinned native replay passed”	“An independent implementation agreed”
Cross-checked	A separately maintained checker accepts the same claim under a recorded policy	“Two recorded checker paths accepted it”	“The claim is mathematically or operationally complete”
Reviewed	Domain experts evaluated statement, assumptions, relevance, attribution, and surrounding argument	“Technical and domain review reached the recorded decision”	“Future verifier bugs cannot change the result”

The OpenAI repository arrived in a strong pinned state. This field-note run reached native-replayed for one target. It did not reach cross-checked because the independent path was not executed here. The broader mathematical results remain matters for expert engagement even when certificates build.

This vocabulary prevents two common errors. First, a build failure does not automatically refute the claim; it may reveal a missing dependency, incompatible platform, or incomplete receipt. Second, a build success does not prove that the statement matches what readers think it means. A checker establishes acceptance under a formal system, not novelty, attribution, usefulness, or real-world applicability.

Build a verifier SBOM before running anything

A software bill of materials lists components in a product. A verifier SBOM lists the components that give a certificate its acceptance meaning.

At minimum, record:

verification_receipt:
  claim_id: "multicolor-ramsey-main-result"
  artifact_repo: "https://github.com/openai/ten-proofs"
  artifact_commit: "94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6"
  target: "MulticolorTriangleRamsey"
  statement_id: "ErdosProblems.MulticolourTriangleRamsey.erdos_problem_183_explicit"
  native_checker: "leanprover/lean4:v4.32.0"
  dependency_lock: "lake-manifest.json sha256:<record-at-run>"
  permitted_axioms:
    - "propext"
    - "Classical.choice"
    - "Quot.sound"
  native_replay:
    status: "pass"
    platform: "macOS arm64"
    command: "lake build MulticolorTriangleRamsey"
    jobs_completed: 8656
  independent_check:
    status: "not_run"
    reason: "documented landrun/Linux sandbox unavailable in this environment"
  known_bad_suite:
    status: "not_run"
  domain_review:
    status: "not_assessed"
  decision: "hold_at_native_replay"

Do not copy the observed values above into another run. Recalculate the artifact hash, manifest hash, platform, command, and result. The schema is reusable; the evidence is not.

The repository’s formalization.yaml is a good starting artifact because it maps human-readable results to Lean declarations, files, axioms, and Comparator configurations. The lockfile then binds packages such as mathlib, Comparator, lean4export, and Lean4Checker to revisions. A useful receipt connects both layers: what claim is being checked, and what software interpreted the certificate.

Reproduce the native path without inflating the result

A native replay answers a basic but necessary question: can your team reconstruct the producer’s intended acceptance path from the published materials?

The run for this field note used an isolated temporary directory and a temporary ELAN_HOME. It checked out the fixed repository commit, installed the declared Lean 4.32.0 toolchain, ran lake exe cache get, and then ran:

lake build MulticolorTriangleRamsey

The build completed successfully. That observation is narrower than “the ten proofs are independently confirmed.” Only one target was selected, the standard Lean path was used, no Comparator challenge was executed, and no mathematical novelty review occurred. Cached dependencies were downloaded from the configured mathlib cache; they were pinned by revision but this run did not establish a separate signed supply-chain provenance for every cache object.

This limitation is not a footnote to hide. It determines the status. A good build log should include:

immutable artifact revision;
verifier version and binary origin;
dependency lock and cache source;
platform and architecture;
exact command and exit status;
target coverage;
start and finish timestamps;
network access during setup and checking;
warnings, skipped steps, and reviewer identity.

If the repository builds only after an undocumented edit, record the patch as a new input. If the current default branch moves, do not silently follow it. If a cache is trusted, say so. Reproducibility is not the absence of judgment; it is the preservation of judgments as inspectable inputs.

Make the independent path prove its independence

“We used a second checker” is too weak. Two commands can share the same parser, exported representation, library cache, kernel logic, or bug family.

Lean’s Comparator checks that named solution theorems match challenge statements, use only permitted axioms, and are accepted by the Lean kernel. It can also enable nanoda. Its own README makes the trusted computing base explicit: the operating system, hardware, sandbox, Lean installation, landrun, lean4export, and possibly prebuilt caches all matter. That disclosure is a strength because it makes “independent” testable.

For each second path, record four forms of distance:

Distance	Question	Weak example	Stronger evidence
Implementation	Is checking logic separately implemented?	Same binary with another flag	Separately maintained kernel
Representation	Does it consume the same derived artifact?	Same cached success marker	Exported proof declarations rechecked
Environment	Does it share mutable state?	Same working directory and cache	Isolated sandbox and recorded inputs
Freshness	Is it current enough to contain known fixes?	“Latest”	Exact revision plus upstream-fix comparison

The Lean incident shows why freshness belongs beside independence. De Moura’s postmortem says the Collatz artifact passed a week-old nanoda, while the relevant nanoda bug had already been fixed. An independent implementation that is stale is still independent, but its decision may not represent the checker you think you are relying on.

Our macOS run stopped before this gate. Installing a substitute sandbox or declaring the ordinary native build “independent” would have changed the method to rescue a green label. The correct next action is to schedule the published Comparator challenge in a compatible, isolated Linux environment and attach that result to the same receipt.

Test the verifier with known-bad artifacts

Positive fixtures show that a checker accepts expected inputs. They do not show that it rejects the failures you care about. Every certificate pipeline needs a known-bad corpus.

The Lean Kernel Arena provides the relevant operating model: run multiple checkers against artifacts expected to be accepted, rejected, or declined, and publish the matrix. The project tracks checker revisions, acceptance coverage, soundness-oriented rejections, runtime, and memory. The postmortem says regression cases for #14576 and a related non-uniform-parameter case were added to the Arena.

For a small team’s non-mathematical verifier, a known-bad corpus might include:

a signed record whose payload was changed after signing;
a schema-valid object with a semantically invalid currency or unit;
a policy decision made with an expired rule bundle;
a test report pointing to a different commit;
a certificate with a permitted-but-unexpected axiom or exception;
a valid output whose dependency manifest is missing;
a previous production incident minimized to one deterministic fixture.

Run this corpus whenever the verifier, exporter, sandbox, dependency resolver, or cache policy changes. A second checker should reject the same dangerous artifacts for reasons you can explain. Agreement on good inputs without disagreement tests can create false diversity.

Add a patch and revocation drill

Checker defects are ordinary software defects with unusually consequential labels. A release process must answer what happens after a patch.

Lean’s initial fix PR #14577 added the missing parameter check and was merged on July 28. A follow-up PR #14582 strengthened uniformity checking for nested inductive parameters. The public response also included patch releases, regression cases, additional hardening, and daily tracking of nanoda for Comparator and lean-eval.

Your drill should simulate this sequence without waiting for a crisis:

Mark the affected verifier range and certificate population.
Stop issuing new “verified” labels from that range.
Re-run the known-bad corpus on the patched checker.
Re-run previously promoted certificates, beginning with high-impact claims.
Compare old and new decisions; preserve both logs.
Downgrade or revoke claims whose evidence no longer passes.
Notify the owners of downstream decisions, not merely the verifier maintainer.
Sign a new receipt with the patch revision and residual unknowns.

This is where many certificate products become ordinary badge systems. They can issue a green mark but cannot enumerate which marks depended on a vulnerable verifier. The ability to revoke is part of verification, not an incident-response extra.

Separate checker acceptance from claim review

Formal acceptance answers a precise question: does this declaration pass this formal system under these assumptions and implementations? A product decision often needs several other answers.

For AI-generated research, expert reviewers still need to assess whether the formal statement captures the manuscript’s intended theorem, whether assumptions are appropriate, whether prior work is attributed, and whether the result is novel or useful. OpenAI explicitly asks the community to place the ten results in context. Its certificate repository reports agent-reviewed status in the formalization manifest; that label should not be rewritten as external peer review.

For an AI-built product, the corresponding gaps are familiar. Passing a JSON schema does not mean a refund is fair. Passing a security policy does not mean the policy covers a new tool. Passing unit tests does not mean the user can recover from a partial side effect. Passing a provenance check does not establish truth.

Use separate receipt fields for:

syntactic validity;
checker acceptance;
independent-checker status;
semantic or domain review;
operational test status;
release decision;
revocation status.

Do not let one successful machine stage overwrite unknown values in the others.

Failure modes this drill is designed to catch

Floating toolchain. The artifact passes today because the verifier or dependency graph changed silently. Pin releases and record resolved revisions.

Stale independence. The second checker is architecturally separate but has missed a relevant upstream fix. Track its commit, release date, and known issue status.

Shared blind spot. Both paths consume the same malformed export, cache, or generated representation. Document shared components and test a route that bypasses them when possible.

Positive-only testing. All examples are expected to pass. Maintain a minimized negative corpus and fail the pipeline when an expected rejection becomes acceptance.

Statement drift. A certificate proves a nearby formal statement while the product or manuscript claims something broader. Bind the human claim to a stable statement identifier and require domain review.

Badge persistence. A verifier bug is fixed, but old green labels remain live with no affected-version query. Store verifier identities in every receipt and exercise revocation.

Platform rescue. A missing dependency or unsupported sandbox is worked around informally, then the altered run is reported as equivalent. Record not_run or create a new method with its own evidence.

When this protocol is appropriate—and when it is not

Use this drill when an AI-generated artifact will justify a high-impact decision and a deterministic or formal checker is part of the evidence: research claims, policy engines, generated migrations, cryptographic provenance, safety cases, financial transformations, or regulated reports.

Do not impose the full protocol on every low-risk draft, UI copy suggestion, or disposable prototype. The cost should follow the consequence of a false green result. For ordinary application code, a simpler version—pinned commit, clean build, negative tests, independent review, and rollback link—may be enough.

This protocol also cannot prove that two implementations are fully independent, that a formal model matches reality, or that no future bug exists. A known-bad corpus covers known classes. A native replay covers one environment. A second checker reduces some correlated risk. Expert review adds judgment. None turns uncertainty into zero.

A 48-hour verifier-supply-chain drill

Hours 0–4: inventory. Pick one consequential AI-generated certificate. Freeze its artifact revision. Record the human claim, formal statement or policy identifier, verifier version, dependencies, caches, platform, and owner.

Hours 4–12: native replay. Reconstruct the intended path in an isolated environment. Preserve commands, logs, exit status, and deviations. If it fails, classify the failure before editing inputs.

Hours 12–20: negative corpus. Add at least three known-bad artifacts, including one minimized prior failure and one stale-version case. Confirm the native path rejects them.

Hours 20–32: independent path. Run a separately maintained checker or an independently implemented validation route. Record shared dependencies and freshness. If the environment is incompatible, mark not_run and schedule the correct environment.

Hours 32–40: patch simulation. Pretend the primary verifier version is affected. Query the certificate population, block new labels, rerun one promoted artifact, and produce a revocation notice.

Hours 40–48: decision. Sign one of four outcomes: hold_at_received, hold_at_native_replay, cross_checked_pending_domain_review, or approved_for_bounded_use. State who can reopen the decision and what new evidence is required.

The goal is not to make every certificate suspicious. It is to make every trust transition observable. OpenAI’s ten-proof release demonstrates how much inspectable evidence a producer can publish. Lean’s rapid incident response demonstrates why checker versions, negative tests, and patch propagation remain part of the claim. A small team should borrow both habits: ship the artifact, and ship the conditions under which its green light deserves to survive.

A green proof is not the end of the verification chain