Haivian Completes Four Mathematical Audits of OpenAI Research
Across graph theory, combinatorics, geometry and Boolean analysis, Haivian reconstructed the claims, inspected their Lean theorem and axiom boundaries, and replayed author-configured checks with Lean’s default kernel—then published exactly what the evidence did and did not establish.
Four ambitious results. Four frozen source editions. One question: does the evidence survive scrutiny?
Haivian Technology has completed and published four version-bounded audits of mathematical results authored by OpenAI. The papers range from directed graph theory and extremal combinatorics to high-dimensional geometry and Boolean analysis. Each audit combined conventional mathematical reconstruction with direct inspection and execution of the associated Lean formalization.
A mathematical result does not become reliable merely because an artificial-intelligence system produced a persuasive proof—or because several AI reviewers agreed that it looked right. Reliability begins when the claim, assumptions and computational evidence are pinned down tightly enough to be challenged.
The result is not a blanket certification of a laboratory, model or repository. It is four public reports identifying the frozen editions, checked formal targets, observed axiom dependencies, Comparator outcomes and remaining boundaries.
What the audit process actually did
For each result, Haivian began by identifying an exact source edition rather than auditing a moving target. The mathematical argument was reconstructed and compared with the stated formal target. Supplied Lean modules were compiled, selected theorem types and axiom closures were inspected, and the authors’ unchanged Comparator configuration was executed against the submitted solution. Acceptance was replayed through Lean’s default kernel.
Those steps test different failure modes. A readable argument can conceal a gap. Compiling code may prove less than the prose suggests. A theorem may depend on unexpected assumptions, while a custom evaluator does not provide the same assurance as kernel checking. A serious audit asks how these layers agree—and records where they do not fully overlap.
Procedurally separated, human-directed AI contexts accelerated reconstruction and evidence review, but model agreement was never treated as proof. The conclusions rest on inspected mathematics and actual formal outputs.
Four different mathematical frontiers
Seymour’s second-neighborhood conjecture
The first report examined a proof concerning finite, nonempty, oriented, unweighted graphs. All 43 supplied Lean modules compiled. Four selected axiom closures contained only the declared permitted foundations, and the unchanged author Comparator accepted the chosen endpoint using Lean’s default kernel.
The report is deliberately narrower than a celebratory headline might imply. Its completed formal scope concerns the exact finite oriented-graph theorem. Weighted variants and cycle consequences were not newly certified as separate formal targets.
A finite-host counterexample to Sidorenko’s conjecture
The second audit examined a submitted finite-host counterexample to Sidorenko’s conjecture. The cumulative execution compiled 31 retained and four newly completed solution modules. Four inspected closures used only the declared permitted axioms, and the unchanged author Comparator accepted the finite-host endpoint with Lean’s default kernel.
The result concerns the stated finite-host, all-homomorphisms construction. It excludes the forcing discussion as a formal target and makes no smallest-host or exhaustive-novelty claim.
A nine-dimensional counterexample to Borsuk’s covering assertion
The third report addressed a compact counterexample in nine-dimensional Euclidean space. All 269 supplied Lean modules compiled, and six inspected closures used only the declared permitted foundations. The unchanged author Comparator accepted its projector-form target; a separately labelled audit-authored Comparator also accepted the literal nine-dimensional theorem with Lean’s default kernel.
The audit supports the compact construction and selected endpoints, but not that every sentence of the conventional full-cycle argument was independently formalized. It makes no minimal-dimension claim and does not replace the compact set with a finite point cloud.
Boolean functions beyond the square-root degree bound
The fourth audit examined a result asserting unbounded violations of a square-root degree bound for Boolean functions. All 21 supplied Lean modules compiled. Seven selected closures were inspected, and the author-configured Comparator’s default-kernel replay accepted the solution.
For every positive real constant, the formal statement provides a positive finite dimension and nonconstant Boolean function meeting the claimed violation; both may depend on that constant. It does not supply a small practical witness for every threshold.
Read the Boolean-functions audit
Why this matters beyond four papers
AI is increasing the speed at which researchers can propose arguments, write code and explore unfamiliar mathematical territory. That is an extraordinary expansion of research capacity. It also creates a corresponding need for systems that can separate an exciting claim from the evidence that actually supports it.
Haivian’s audit pipeline is designed for that gap. It does not ask readers to trust an AI personality, a prestigious name or a chorus of automated approval. It turns the work into inspectable questions: Which version? Which theorem? Which assumptions? Which execution? Which checker? Which limits?
These four reports demonstrate the model across substantially different mathematical domains. They also show why an audit report should preserve uncertainty rather than erase it. A bounded conclusion with a visible evidence trail is more useful than an inflated declaration that cannot survive inspection.
Scope and disclosure
OpenAI authored the four reviewed mathematical manuscripts and provides the models used in the same-provider AI-assisted review. Haivian audited the identified frozen editions; it did not perform the work for OpenAI. The audits do not imply an OpenAI partnership, commission or endorsement.
Richard Janutka of Qonduit Limited NZ commissioned the audits and controls the Haivian audit and journal operation. Haivian Technology is the corporate author of the validation reports. The process is not external human peer review, independent-provider AI corroboration, a clean-room rebuild of every dependency or verification by a second independent proof kernel. Nanoda was not run. Each public report states its own mathematical, technical and evidentiary limits.
Put a research claim through the pipeline
Haivian accepts mathematics and science for evidence-led research auditing—from claim reconstruction and computational checking through a publication-ready validation record.