One OpenAI Math Proof Target Passed Twice. Two Hit Our Memory Cap.

Six local attempts, three selected targets, and a fixed 7 GiB memory ceiling. One target received kernel acceptance on both runs. The other two remained unassessed under that budget.

Kingy.ai tried to check three formal proof targets from OpenAI’s mathematics release on a local machine. The Abhyankar–Sathaye target passed twice. Affine Bernstein and Pi Exponent each reached our memory cap twice before the checker returned a proof verdict.

That gives us one target with repeatable local acceptance and two unresolved cases under the conditions we chose. The four stopped attempts did not establish that either proof was wrong. They established that our checking workflow reached its resource boundary before it could finish.

The pilot follows our coverage of OpenAI’s 722-manuscript release and our comparison of OpenAI and Google DeepMind’s mathematical evidence. This time, we moved from reading disclosures to executing a small, bounded check of released artifacts.

The test ran on October 6, 2026, Pacific time. Codex configured and operated the local environment, collected the logs, and assessed the recorded checker outcomes. No human mathematician reviewed the correspondence between the formal statements and their accompanying manuscripts.

Source: Kingy’s recorded pilot results. Times include building and checking within each attempt, excluding setup and controls. Memory is the peak charged to the process group, including cache; it is not an estimate of minimum computer RAM. Stop handling changed after the first Affine Bernstein attempt, so resource-limited times are not directly comparable.

We selected Pi Exponent because of its connection to the original article. For the other two cases, we took the first two remaining Comparator configuration filenames in alphabetical order at the frozen source revision. We kept that selection regardless of the outcomes. It is a deliberately small, non-random sample, so a percentage calculated from these three targets would tell readers little about the full release.

The accepted target’s formal name is OAI.AbhyankarSathaye.exists_noncoordinate_polynomial. On both attempts, its log recorded Lean default kernel accepts the solution, followed by Your solution is okay!. Each attempt also completed with the checker’s exit code zero. The raw evidence is retained for attempt one and attempt two.

Comparator checks a supplied solution against a specified formal challenge. Under its documented trust assumptions, success establishes agreement with that challenge statement, compliance with the allowed axioms, and acceptance by the Lean kernel. Our selected configurations allowed propext, Quot.sound, and Classical.choice. The optional Nanoda checker was disabled. The pinned Comparator documentation sets out those guarantees and assumptions.

There is still a separate question about whether a formal challenge captures everything a reader understands the accompanying paper to claim. We did not perform that mathematical review or assess novelty. For Pi Exponent, OpenAI’s own scope note says the selected statement excludes the paper’s Flint–Hills-series convergence consequence. Our pilot could not have validated that consequence even if this target had passed.

The resource choice matters to every result in the table. We used an ARM64 Linux virtual machine with four virtual CPUs, 8 GiB of RAM, and a 32 GiB virtual disk. Each proof attempt had a 7 GiB process-group memory ceiling, no swap, and a one-hour time limit. The host had 24 GiB of RAM; the smaller allocation left room for its other work.

The protocol allowed up to 16 GiB of VM memory. We selected the lower allocation before testing and kept it fixed. The two unresolved targets might behave differently with more memory or a different build configuration, but this pilot does not answer that. It also does not establish a minimum RAM requirement for either target.

All four resource-limited attempts hit the 7 GiB boundary. The recorded out-of-memory-kill counters remained zero. The stopping rule ended the work at the resource boundary; these were not four checker rejections or four observed operating-system OOM kills. A wrapper process could even report exit code zero after an external stop. We therefore required affirmative checker output and the checker’s own successful exit status before counting an acceptance.

There was one change in how the stopping rule was enforced. Codex stopped the first Affine Bernstein attempt after inspecting its telemetry. Later attempts stopped automatically at the first sampled memory-limit event, using roughly two-second sampling. The memory ceiling stayed the same, but that change affected stop latency. The shorter second Affine Bernstein attempt is not evidence of a faster proof.

Before each target attempt, we ran three controls: a valid proof, a mismatched theorem statement, and a proof containing sorryAx, an axiom representing an admitted proof. The valid proof had to pass; both invalid controls had to be rejected for the expected reason. Including the initial setup checks, all 21 control checks behaved as expected. That tests specific checker behavior without replacing a broader security or correctness audit.

Each attempt began with a fresh writable build directory over the same read-only prepared baseline. We reused trusted dependency caches, but carried no target build outputs into the next attempt. Operating-system caches could remain warm. Both passes ran on the same machine under the same operator, so the repeat demonstrates local consistency rather than replication by an independent team.

We pinned the OpenAI source snapshot, used Lean 4.34.1, and audited all 42 resolved dependency revisions. The selected Comparator and exporter revisions specified Lean 4.34.0; their toolchain files were changed to 4.34.1 and the tools rebuilt. Those diffs are preserved. Downloaded dependency objects were hashed and trusted, so this was not a complete rebuild and audit of every dependency from source. Release-supplied dependency patches were retained.

Setup took 46.2 minutes. The complete pilot, including evidence cleanup, took 76.5 minutes. Setup included recovering from an initial VM boot problem; a disk-size logging error and the toolchain adjustments are also documented in the technical report. The accepted target’s roughly one-minute attempt times exclude that preparation.

Paid-service expenditure for the pilot was $0. We used local computing resources and downloaded public software and cache artifacts. Hardware cost, electricity, and the full volume of network transfers were not measured. These figures describe the cost of this checking exercise; they do not measure OpenAI’s cost to discover, generate, or formalize the original arguments.

The outcome also supplies no OpenAI-versus-DeepMind ranking. We ran no matched DeepMind experiment and made no new model-generation calls. Our result concerns the behavior of three selected released artifacts under one recorded configuration.

The local evidence bundle preserves the protocol, exact commands, source and tool revisions, raw logs, resource telemetry, dependency diffs, and build-output archives. All six build archives and the recorded target and tool hashes were verified. The temporary VM was deleted after the evidence was copied and checked.

Download the public evidence package and its SHA-256 checksums. The export notes explain what is included. Original files retain their historical “private” or “unpublished” labels; publication was authorized after the experiment. The complete local archive is broader than this public export.

A useful next experiment would give the two unresolved targets a separately recorded memory budget and repeat the same frozen inputs. A separate mathematical review would examine whether each formal challenge expresses the manuscript claim accurately. Neither follow-up has been performed.