OpenAI formal proof pilot — private results

Executed October 6, 2026 Pacific / October 7 UTC. Unpublished.

Six local attempts across three selected targets. 2 attempts received affirmative checker acceptance; 4 stopped at the memory boundary without a proof verdict. No paid services were used.

Target | Run | Outcome | Wall time | Cgroup memory peak

AbhyankarSathaye | run1 | CHECKER_ACCEPTED | 77.3 s | 2.667 GiB

AffineBernstein | run1 | RESOURCE_LIMIT | 410.9 s | 7.000 GiB

PiExponent | run1 | RESOURCE_LIMIT | 235.1 s | 7.000 GiB

AbhyankarSathaye | run2 | CHECKER_ACCEPTED | 64.8 s | 2.276 GiB

AffineBernstein | run2 | RESOURCE_LIMIT | 232.8 s | 7.000 GiB

PiExponent | run2 | RESOURCE_LIMIT | 276.2 s | 7.000 GiB

What these results establish

Each accepted attempt matched the frozen challenge statement, passed the configured axiom checks, and produced the Comparator message “Lean default kernel accepts the solution.” A zero wrapper exit code alone was never counted as acceptance. Resource-limited attempts remain unassessed for correctness under this budget.

The controls used a valid proof, a mismatched theorem statement, and a proof containing sorryAx. Their expected acceptance or rejection was checked before every target attempt. All 21 control checks (one initial set and six per-attempt sets) behaved as expected. Challenge/configuration hashes and checker/exporter/sandbox binary hashes were verified after each attempt. The same machine performed both passes; this is a local repeat, not an independent replication by another operator.

Frozen inputs

OpenAI source: adc7f1241b42e322a6451854ab7e4b4c146bf78a; Lean 4.34.1; Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612. All 42 resolved dependency revisions were audited.

Comparator: d03acab154d269c06e60e4de7e4cc85deebff94b. Exporter: 076e8e57707e813375e8f9da8bf989799ace9680. Their toolchain files were changed from 4.34.0 to 4.34.1 and the tools rebuilt; both diffs are retained. Landrun: 811cfff51ceaf3d9843708aa6d22e9b84ccac8b4.

PiExponent was chosen for its connection to the original article. The other two targets are the first two other configuration basenames alphabetically at the frozen snapshot. Outcomes did not change the selection. Exact theorem names, axioms and configurations are in targets.json. Nanoda was disabled in the supplied configurations.

Resources and timing

The dedicated ARM64 Linux VM had 4 vCPUs, 8 GiB RAM and a 32 GiB virtual disk. Each target had a 7 GiB cgroup memory ceiling, zero swap and a 60-minute time limit. These are below the protocol maxima of 4 vCPUs, 16 GiB RAM and 80 GiB total task storage. The lower memory allocation was selected before target execution to leave room for other work on the 24 GiB host.

Setup took 46.2 minutes, within its two-hour limit. The overall deadline was 2026-10-07T11:11:29.114131+00:00. Wall times include challenge/solution building and checker work; setup and control time are separate. CPU values for stopped attempts are lower bounds from the last available telemetry.

Cgroup memory peak includes memory charged to the process tree, including cache. It is not a minimum-RAM recommendation or an RSS-only measure. The disk high-water values in results.json cover the guest filesystem, including its OS and shared dependencies. Host-wide task storage was not sampled continuously; fixed VM disk size and host free-space safeguards bounded the principal storage use. Electricity cost and complete network-transfer bytes were not measured. Paid-service expenditure was $0.

Build and trust conditions

Each attempt used a new OverlayFS writable layer over the same read-only prepared source/dependency baseline. No target build outputs carried into the next attempt. Shared dependency objects were prefetched from the release’s cache workflow, hashed, and trusted. OS caches could remain warm. This was not a fully source-built dependency audit. Release-supplied dependency patches were retained and recorded; they explain the local-change warnings in build logs.

The VM had no host filesystem mounts or forwarded credentials. Proof work ran as an unprivileged user. Landrun and the recorded AF_UNIX restriction constrained checker/exporter processes. The OS image and Lean archive were verified against recorded digests.

Execution deviations and limitations

The initial Ubuntu VM boot failed to expose SSH. Applying Lima’s internal_netplanOptional setting recovered SSH; the guest agent remained degraded. The experiment used SSH and did not depend on guest file sharing. A final setup disk-size logger returned exit 1 because a target build directory did not yet exist; the dependency and cache preparation had completed.

The first AffineBernstein attempt hit the 7 GiB boundary and was stopped after operator telemetry review. Later attempts automatically stopped at the first sampled memory.max event (approximately two-second sampling). The ceiling stayed fixed, but stop latency changed; resource-limited wall times should not be treated as comparable benchmark scores. The original runner was reconstructed by removing that single patch and is labelled as reconstructed.

Systemd can report wrapper exit 0 after an external stop, and completed transient units may lose their properties. Classification therefore uses affirmative raw checker output, worker exit status, resource-stop markers and live cgroup telemetry.

No human mathematician reviewed manuscript-to-formal-statement correspondence. Novelty, proof discovery, and the correctness of claims outside the selected formal statements were not assessed. PiExponent does not test the separate Flint–Hills-series consequence. These results do not estimate success across the full OpenAI release, recreate OpenAI’s generation compute, or establish an OpenAI-versus-DeepMind winner.

Evidence and rerun guidance

results.json contains the six assessed receipts and measurements. evidence/ contains raw logs, live telemetry, controls, dependency diffs, cache hashes and each attempt’s build-output archive. SHA256SUMS covers the retained local bundle. protocol-v1.txt and targets.json preserve the original plan. execution-notes.txt records interventions.

To repeat, reconstruct the dedicated VM from vm-retry.yaml, use the pinned source/tool acquisition and preparation scripts, validate the controls, then run fresh-workspace.sh, run-controls.py, validate-controls.py, run-target.py and finish-attempt.sh for each target in the recorded order. The scripts use the explicit /home/proof and /opt/pilot paths and need the same VM/user setup. Reacquire public dependencies/cache objects at their recorded revisions and compare the retained hashes. The exact executed target commands are in each receipt.

The evidence bundle is local. No results were published or sent to an external service.

The complete pilot, including setup and evidence cleanup, took 76.5 minutes. The dedicated VM was deleted after evidence verification. The public OS-image cache was retained.
