Independent investigation · Plain-English edition

A computer can check every step and still miss the point.

That is the idea behind this audit of OpenAI’s ten machine-checked math results. It is also the problem companies will face as AI agents begin doing real work.

Understand it in 60 seconds Open the technical evidence

What the checker can prove

The proof follows the formal rules.

Every logical step is accepted by the checker, with the allowed assumptions and definitions.

What still needs judgment

The formal rules describe the right problem.

A flawless proof of the wrong statement is still a flawless proof. The checker cannot recover human intent from the proof alone.

01 / THE WHOLE POINT

Five things to know. No math background required.

Formal verification is powerful. The mistake is treating it as a guarantee about everything surrounding the proof.

OpenAI published ten mathematical advances.

It also released formal proof artifacts that software can inspect line by line.

That is much stronger than “the model said so.”

A proof checker rejects a step that does not logically follow.

The checker only sees the formal statement.

It does not know the private intent, headline, paper narrative or business goal behind it.

The exact software versions matter.

“It checked” means specific files were accepted by specific checker versions at a specific time.

Someone still has to decide what is safe to rely on.

Verification informs that decision. It does not make the accountability decision disappear.

Verification is local. It proves a specific relationship between specific artifacts.

The confidence does not automatically spread backward to the original intent or forward to the real-world outcome.

02 / THE CLEAREST EXAMPLE

One of the twelve result bundles needs a different kind of review.

Eleven bundles ask the system to fill in proofs. The GapCVP bundle also lets it supply four definitions.

A narrow technical difference with a big meaning

It is like filling in part of the contract, then proving you followed it.

For most bundles, the trusted file already fixes the statement and asks for a proof. In the GapCVP bundle, four definition bodies are also supplied by the solution.

The checker can confirm that those definitions have the required names, types, safety level and permitted assumptions. That is real assurance.

But the shape of a definition is not the same thing as its intended meaning. Lean’s Comparator documentation therefore calls for an additional verifier when definition holes are involved.

What this does not mean: we found no evidence that the GapCVP result is false. The finding is that its review path is structurally different and should be made explicit.

03 / WHY A BUSINESS LEADER SHOULD CARE

An AI agent can leave a perfect audit trail for the wrong task.

The enterprise version of this problem will not look like a math proof. It will look like a workflow that completed exactly as designed.

Example request

“Follow up with every qualified lead.”

The agent uses the company’s qualification rule, sends the emails, updates the CRM and creates the follow-up tasks.

Every recorded step is true. The workflow reports 100% completion.

The execution receipt looks perfect.

01Lead records loadedComplete

02Qualification rule appliedComplete

03Emails sentComplete

04CRM updatedComplete

05Tasks createdComplete

?The qualification rule was six months out of dateNot checked

Everything in the log can be true.

The system really did complete every recorded action.

The business outcome can still be wrong.

The wrong leads were contacted because the specification was stale.

What was the intended outcome?

Not just the prompt. The real business result.

Who authorized the action?

And within what limits?

Which rule and version governed?

Policies and definitions change.

What evidence was used?

How fresh was it, and what remained uncertain?

What changed in the outside world?

Do not confuse “workflow ended” with “outcome occurred.”

Who owned the exception?

Someone still accepts, rejects or escalates the remaining risk.

I turned those questions into a simple AI Action Assurance Record: a portable receipt for consequential actions, not another dashboard.

Open the action record

04 / WHAT THE AUDIT FOUND

The release is strong. The remaining boundary is specific.

This is not an argument against formal verification. It is an argument for describing its guarantee precisely.

10announced mathematical advances

12formal result bundles

38named theorem targets

0proof holes reported in the solution manifest

12configurations requesting an independent checker

1bundle with four definition holes and a different review path

99.8% / 0.2%

We removed our own most memorable statistic.

The first release compared proof-file bytes with statement-file bytes. That ratio was real, but the interpretation was not useful: file size is not a measure of confidence, effort or consequence. The better insight is that a small trust surface can control the meaning of a much larger checked artifact.

05 / CHOOSE YOUR DEPTH

The main argument is above. The receipts are below.

No technical knowledge is required to understand the finding. Technical readers can inspect every source and assumption.

Technical appendix

Explore all twelve result bundles

Exact theorem targets, source excerpts, assumptions and caveats. The old progress-style bars have been removed.

Machine-readable

Download the audit manifest

The repository commit, toolchain, findings, limits and definition-hole boundary in JSON.

Enterprise template

Open the AI Action Assurance Record

A clean printable worksheet for intent, authority, evidence, execution, outcome, validation and human control.

Implementation

Use the JSON schema

A starting structure for adding action assurance records to an agent or operating system.

What exactly is a “definition hole”?

A theorem hole asks the solver to provide a proof of a statement whose surrounding definitions are already trusted. A definition hole also asks the solver to provide the body of a named definition. Comparator can verify that the supplied definition has the expected formal interface and uses permitted assumptions. An extra review is needed to judge whether that body represents the intended concept.

Are you saying OpenAI’s math is wrong?

No. This audit found no evidence that any result is false. It is an assurance and release-artifact audit, not mathematical peer review. The finding is about the scope and portability of the verification claim.

Why do checker versions matter if a proof is timeless?

The mathematical relationship may be timeless. The statement “this artifact was accepted” describes an event performed by particular software, dependencies and configurations. A durable assurance claim should name and hash those exact inputs so another party can reproduce the same check later.

The proof can be machine-checkable. The assurance case should be understandable.

That is the standard this page now tries to meet—and the standard consequential AI systems should eventually meet too.

Use the action record Inspect the technical evidence