verify: evidence-led replay of OpenAI ten-proofs

[ghost]

AEGIS Ω Verification Ledger — OpenAI Ten Proofs

This draft PR is a public, exact-commit verification record for:

• upstream: openai/ten-proofs
• commit: c510a55434c0935cde446e5a372699a4671438f6
• Lean toolchain: leanprover/lean4:v4.32.0
• AEGIS harness branch: verify/openai-ten-proofs-2026-08-01

Why this exists

The goal is not to restate published mathematics or manufacture certainty. The goal is to expose every authority transition:

published source → exact checkout → Lean build → placeholder audit → independent checker → immutable receipt

A stage that fails remains visible. A stage that was not executed is not promoted to verified.

Run 1 — recorded outcome

Workflow run 30703012816 produced:

• exact source checkout: PASS
• source identity binding: PASS
• lake build All: PASS
• placeholder audit: FAIL
• independent Lean replay / Nanoda: NOT MEASURED
• final verification conjunction: FAIL

The failed audit scanned ComparatorChallenges/ and .lake/, conflating intentionally incomplete challenge material and third-party dependencies with the authoritative top-level Lean corpus. The failure is preserved as evidence of a harness-scope defect; it is not rewritten as mathematical failure.

Harness correction

Commit 89f3b99df35413b6ab4a5c8311c620837b40622c:

• restricts the placeholder audit to top-level authoritative Lean sources;
• records exact sorry and admit counts;
• forces the independent checker stage to run after a successful Lean build even when another gate fails;
• writes build, audit, and independent-check outcomes into the receipt;
• enforces the final result as a strict conjunction.

Admission rule

This PR may claim complete exact-environment verification only when all mandatory clauses pass:

• exact commit binding;
• lake build All;
• sorry_count == 0;
• admit_count == 0;
• independent Lean environment replay;
• Nanoda with allow_sorry: false;
• uploaded receipt.

Explicit non-claims

This harness does not establish:

• that AEGIS discovered the ten mathematical advances;
• universal correctness of the associated informal papers;
• equivalence between every prose statement and every Lean theorem;
• validity under other commits, toolchains, or environments;
• evidence for a universal common generator G.

Current status

REVALIDATION_IN_PROGRESS

The first run remains a valid failed preregistration record. The corrected run must generate a new receipt; no earlier evidence object is mutated.

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
hook-generator	Ready	Preview	Aug 1, 2026 5:34pm
hub	Ready	Preview	Aug 1, 2026 5:34pm
platform-picker	Ready	Preview	Aug 1, 2026 5:34pm

[cloudflare-workers-and-pages]

Deploying with    Cloudflare Workers

The latest updates on your project. Learn more about integrating Git with Workers.

Status	Name	Latest Commit	Preview URL	Updated (UTC)
✅ Deployment successful! View logs	aegisomega	89f3b99	Commit Preview URL Branch Preview URL	Aug 01 2026, 05:34 PM

[ghost]

Sealed predictive certificate PEC-G-0001 before completion of workflow run 30703012816.

Seal commit: 3ee522eb298fd3bb2d1082107ad67c96db846818
Certificate: evidence/predictive/PEC-G-0001.yaml
Seal time: 2026-08-01T16:51:07+02:00

At seal time, checkout and source binding had already passed; lake build All was still in progress, while the placeholder audit, Lean environment replay, Nanoda check, final conclusion, and receipt remained unobserved. The certificate predicts success for every remaining mandatory stage and resulting_realization_state: VERIFIED. Any failed, cancelled, timed-out, placeholder-detecting, or verifier-rejecting mandatory stage contradicts the certificate. Result interpretation is append-only; thresholds cannot be changed after measurement.

[ghost]

External seal anchor for the predictive certificate, posted while workflow run 30703012816 is still in progress:

• certificate file: evidence/predictive/PEC-G-0001.yaml
• certificate SHA-256: 314a9cd87950fd75212dc63441d2ed14b8b884e3ad40d85dd07cb54a8c406664
• certificate size: 3411 bytes
• sealing commit: 3ee522eb298fd3bb2d1082107ad67c96db846818
• upstream target: openai/ten-proofs@c510a55434c0935cde446e5a372699a4671438f6
• workflow run: 30703012816

This GitHub comment is the third-party timestamp anchor for t_seal < t_measurement. The certificate's load-bearing scope is verifier convergence for the declared commit, toolchain, workflow run, and environment; it does not establish empirical closure of a universal generator G.

[ghost]

Append-only result for externally anchored certificate hash 314a9cd87950fd75212dc63441d2ed14b8b884e3ad40d85dd07cb54a8c406664:

• workflow run: 30703012816
• final workflow/job conclusion: failure
• exact source binding: success
• lake build All: success — 8,666 jobs completed; all declared top-level proof modules built
• placeholder audit: failure
• independent Lean replay / Nanoda: skipped because the preceding audit failed
• receipt artifact: 8820000233
• artifact digest: sha256:1e66802ad893b8af93e89fa3daf9cfd4e77bcc4e5e8947b3b61dd5ef59151a9a
• receipt verification time: 2026-08-01T14:58:07Z

Under the certificate's frozen conjunctive criterion, the prediction is CONTRADICTED.

Failure localization: the audit used recursive grep over the entire checkout, including ComparatorChallenges/ (45 intentional sorry occurrences) and .lake/packages/ dependencies/tests. No placeholder hit was reported in the top-level proof modules themselves. Therefore this run verifies exact-commit Lean buildability, but it does not execute Nanoda and does not establish independent checker convergence. A corrected audit and Nanoda run must be issued as a new certificate/run; this result must not be reinterpreted retroactively.