KINGY OPENAI FORMAL-PROOF PILOT — PROTOCOL v1
Prepared October 6, 2026 (America/Vancouver)
Status: planned; Kingy proof checks executed: 0.

Purpose

Test whether three released formal targets can be checked from pinned public
materials in a fresh environment, and measure the resources and intervention
needed. Report formal checking and correspondence to the manuscript separately.
This is a selected-case reproducibility study. Three cases cannot estimate the
correctness rate of the collection or establish mathematical novelty.

Fixed selection

Use openai/math commit adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Select PiExponent because the published Kingy comparison discusses its scope.
Select the first two other JSON configurations in bytewise alphabetical order
under lean/ComparatorChallenges. Retain failures and blocked targets; do not
substitute easier targets. The complete directory list is selection-universe.json.

Execution order:
1. AbhyankarSathaye.json — OAI.AbhyankarSathaye.exists_noncoordinate_polynomial.
   The challenge concerns a noncoordinate polynomial over C, in each dimension
   n >= 4, whose quotient ring is isomorphic to a polynomial ring in n-1 variables.
2. AffineBernstein.json — OAI.AffineBernstein.affine_bernstein.
   The challenge concerns dimensions 3 through 9 under its stated smoothness,
   convexity, Hessian positivity, maximality and completeness hypotheses.
3. PiExponent.json — OAI.PiExponent.main.
   The challenge combines a rational-approximation bound with a supremum
   characterization. Family 017 excludes the Flint–Hills convergence consequence.

targets.json preserves exact configurations, module paths and theorem names.
Each selected configuration has no definition holes, permits propext, Quot.sound
and Classical.choice, and disables nanoda. Preserve those settings for the pilot.
Challenge files contain expected sorry placeholders. Their presence alone is not
a failed solution. Inspect the selected proof's dependency closure through the
checker; a text search for sorry is not sufficient acceptance evidence.

Environment and resource envelope

Use a dedicated disposable Linux VM, an unprivileged checking user, Landlock,
and the systemd restriction described in the pinned current Comparator README.
Use no host home-directory mounts, credentials or Docker socket. Freeze the VM
image digest, kernel, architecture, compiler versions and enabled restrictions.
The inspected workstation is arm64 macOS; docker and colima are on PATH, but
Linux availability and capacity have not been established. No Lean, Lake or elan
was found on PATH. Do not infer readiness from the presence of a CLI.

Proposed caps, not expected usage: 4 vCPUs, 16 GiB VM RAM, swap disabled, 80 GiB
total task storage, 2 hours for setup and controls, 60 minutes per target per
fresh run, and 8 hours overall. Run one target at a time. Confirm host capacity
before reserving these resources. If unavailable, report an environment blocker.
Enforce time, memory and disk limits over the whole process tree/VM. Stop the
affected run when a limit is reached and retain its logs. Cap paid infrastructure
and API expenditure at $0; local electricity is unmeasured, not zero cost.

Version preparation and compatibility checkpoint

The release pins leanprover/lean4:v4.34.1 and mathlib commit
d13f23b723b8a846827a245b89c10fc7d3f11612. Preserve every dependency revision in
the supplied lake-manifest.json, not just mathlib. The lakefile applies bundled
compatibility patches; capture their hashes and resulting dependency diffs.
These are part of the release, distinct from any later Kingy repair.

Current Comparator ca04cfc72b550331658ec314bf47685281bfd4bf targets Lean
4.35.0-rc4. Do not run its binary against the release and assume compatibility.
The initial compatibility candidate is Comparator
d03acab154d269c06e60e4de7e4cc85deebff94b, whose own toolchain is 4.34.0 and whose
exporter is pinned to 076e8e57707e813375e8f9da8bf989799ace9680. In separate tool
checkouts, attempt to build these sources with Lean 4.34.1; save the exact
toolchain override/diff and resulting binary hashes. Compatibility is UNTESTED.
Pin Landrun source to 811cfff51ceaf3d9843708aa6d22e9b84ccac8b4.

If that candidate cannot build or pass controls under the required restrictions,
stop with TOOLCHAIN_BLOCKED. Do not change the OpenAI Lean version, weaken the
sandbox, use fake-landrun, silently follow a branch, or modify proof sources to
get the baseline working. A later tool repair requires a new recorded protocol
revision before targets run. No claim of an execution-ready toolchain is made.

Controls before target execution

In a separate fixture project on exactly the same toolchain and wrapper, check:
- A valid proof of a simple fixed statement: acceptance expected.
- A valid proof of a different statement with the same declaration name:
  statement-mismatch rejection expected.
- The matching statement with a sorry proof: disallowed-axiom rejection expected.

Record fixture sources/configuration hashes, command, full logs and exit status.
A missing file, compilation failure or generic nonzero exit does not satisfy a
negative control. Verify the rejection reason. A failed control blocks all three
targets. Repeat the controls in each newly prepared run environment.

Preparation and runs

A. Preserve the protocol, target list and source hashes before execution.
   Acquire the pinned repository, including lean/patches, and named dependencies
   in the isolated environment. Read/audit build hooks before invoking Lake.
   Review challenge imports and definitions as the trusted statement boundary.
   Do not precompile solution modules before invoking Comparator.

B. Follow the release's dependency setup in isolation. Save the manifest before
   and after lake update; reject unrecorded revision drift. Preserve expected
   release patches. If the supplied manifest cannot be reproduced, report the
   setup failure rather than accepting a newly resolved baseline. Download only
   identified trusted dependency caches; record provenance, hashes and bytes.
   State explicitly that cached dependency objects are trusted. Do not label
   this a complete source rebuild. Keep OpenAI target build outputs absent.

C. Run each unchanged target through Comparator from the repository's lean/
   directory. The invocation follows the documented systemd wrapper with
   RestrictAddressFamilies=~AF_UNIX, --user, --pty, the frozen working directory,
   and the explicit pinned binary paths. Its inner command is:

   lake env /absolute/pinned/comparator ComparatorChallenges/<target>.json

   Implement the recorded time/memory/disk limits around that process tree.
   This command is a plan template, not a tested runnable script. Preserve full
   stdout/stderr and the actual exit status; logging through a pipeline must not
   replace the checker's exit code with the logger's. Build only selected targets
   and required imports, following the release's small-portion build guidance.

D. Do a second run for every target, including initial failures, starting from a
   fresh working directory/VM snapshot containing identical tools and approved
   dependency caches but no outputs from the first target run. No warm recheck
   counts as independent repetition. Record cache policy and setup costs. This
   is same-platform repetition; another machine/operator is a separate study.

E. Preserve failure outcomes. At most one retry for a documented transient
   download interruption is allowed during setup, within the original caps.
   Log both attempts. No edited-proof retries enter the baseline. Any later
   patched experiment keeps its own source diff, identifier and result row.

Record and interpret

For each run retain: target/config and source hashes; complete dependency and
tool revisions; binary hashes; OS/kernel/architecture; exact command and cwd;
start/end UTC; exit code or signal; logs; wall time; user/system CPU time;
cgroup memory peak for the process tree; OOM events; disk high-water mark;
download/cache bytes where measurable; cache provenance; operator interventions
and hands-on minutes. Null means unmeasured, never zero. Save SHA-256 checksums
for the complete evidence bundle. Keep setup separate from per-target checking.

Use separate status fields:
- execution: NOT_RUN, ENVIRONMENT_BLOCKED, TOOLCHAIN_BLOCKED, DEPENDENCY_ERROR,
  BUILD_ERROR, TIMEOUT, RESOURCE_LIMIT, CHECKER_REJECTED, CHECKER_ACCEPTED,
  or INDETERMINATE.
- repeatability: NOT_ASSESSED, AGREEMENT or DISAGREEMENT.
- manuscript correspondence: NOT_REVIEWED, REVIEWED_WITH_LIMITS, MISMATCH,
  or HUMAN_ACCEPTED, with reviewer identity and explicit evidence for acceptance.

CHECKER_ACCEPTED requires successful controls, unchanged target configuration,
recorded trust assumptions, exit zero and affirmative acceptance of the requested
declaration by the pinned checker. Do not equate compilation with acceptance.
CHECKER_REJECTED records the exact statement/axiom/kernel failure; it does not
by itself establish that the mathematical theorem is false. Environmental and
resource failures do not count as proof rejections. Same result twice records
agreement, but only two accepted runs support repeated successful checking.

For manuscript correspondence, map the formal theorem to the paper's exact
numbered claim and inspect quantifiers, domain, hypotheses, definitions and
excluded consequences. AI-assisted inspection is labelled as such. Human
acceptance stays null until an identified qualified reviewer attests it. The
PiExponent report must preserve the family-017 Flint–Hills exclusion.

Public report proposed after execution

Publish all three selected cases and both runs, including blocked cases, with
reproduction instructions and raw evidence. Say precisely how many targets were
accepted, rejected or unassessed. Explain source-built versus cached components.
Checking time is not OpenAI's discovery compute or training cost. No collection-
wide success percentage, 722-paper validation claim, or OpenAI-versus-DeepMind
winner follows from this pilot. A useful article angle is: "Can we reproduce
three checks from OpenAI's mathematics release? Our commands, costs and limits."

Work completed for this plan

Read and saved selected public documentation, challenge files and JSON configs;
resolved tool versions; preserved hashes; prepared empty result records. No
installation, VM start, solution compilation, Comparator execution, paid call,
mathematical acceptance, or publication was performed for this planning request.
The existing published comparison article was not modified.

Sources

All archived URLs and checksums are in source-manifest.json. Key references:
https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/017.md
https://github.com/leanprover/comparator/blob/ca04cfc72b550331658ec314bf47685281bfd4bf/README.md
https://github.com/leanprover/comparator/tree/d03acab154d269c06e60e4de7e4cc85deebff94b
https://github.com/Zouuup/landrun/tree/811cfff51ceaf3d9843708aa6d22e9b84ccac8b4
