Two Auditors Found the Reversed Step Inside an AI-Generated Proof
Alfred Kempe published a proof of the four-colour theorem in 1879, and for eleven years the map problem was treated as closed. In 1890 Percy Heawood worked through the argument line by line and produced a map on which one of Kempe's cases collapsed. Kempe reported the error to the London Mathematical Society himself and said he could not repair it. Heawood then salvaged what could be salvaged: enough of Kempe's machinery survived to prove that five colours always suffice. The four-colour question stayed open until Appel and Haken closed it in 1976 with a computer-assisted argument that a good many mathematicians disliked, on the grounds that no person could read it end to end.
Two features of that century carry forward. The defect in Kempe's paper was local, the statement he was aiming at was true, and it was found by someone reading. And when machines finally arrived in the proof, the objection raised against them was about whether anyone could read the thing. In the past fortnight both halves have come back together.
Practical takeaway. A machine-checked formalization and the printed proof of the same theorem are two different artifacts, and only one of them is the one people read. Two audits published this month found real defects in AI-generated and AI-adjacent mathematics, and one of the two sits on the reduction chain that runs toward the lattice problems behind post-quantum cryptography. A third case, in software, ended with two firms unable to agree on what an automated review had actually read. Which of those states a claimed result is in now decides how much weight it can carry.
Chapter Six, read closely
On 3 August 2026 Mikołaj Sienicki and Krzysztof Sienicki posted a short note, Auditing an AI-Generated Mathematical Proof (arXiv:2608.14673). Their subject is Chapter 6 of OpenAI's Ten Advances in Mathematics and Theoretical Computer Science, which claims an exponential parallel-repetition theorem for all finite two-player, one-round entangled games — the guarantee that the chance of winning every round of a repeated game with entangled players falls off exponentially, which is what lets a protocol designer drive an error rate down by repeating it.
Early in that chapter the proof leans on a quantitative greedy conditioning lemma, which selects a small set of coordinates such that, once you condition on winning every coordinate in the set, a randomly chosen remaining coordinate is won with average probability at least 1 − δ. The auditors find the statement correct and the printed proof broken. The procedure's continuation test is written in terms of average success, while the step that follows requires a coordinate with a large conditional failure probability. That implication does not hold, and the note shows simple cases in which the printed procedure is left with no valid next move at all. It gives the counterexample, identifies the continuation condition that was intended, and supplies a complete corrected proof. The repair is local: the lemma's statement and the parameters the rest of the chapter draws from it are unchanged.
What the auditors decline to do carries as much weight. The note states plainly that the correction “should not, however, be read as an independent verification of the main parallel-repetition theorem.” They fixed one step and say so. Their closing observation is the durable one: a mathematically plausible machine-written argument can conceal a small but decisive reversal between complementary events, a swap of success for failure that reads perfectly well and is fatal anyway.
The file the machine checked is not the chapter you read
OpenAI published Lean 4 formalizations alongside the results, in the openai/ten-proofs repository. Quantum parallel repetition is the sixth entry in that repository's own list, and it has a file of its own. The manifest that ships with the repository records the certified declaration as QuantumParallelRepetition.distributionUniformExponential, with sorry_count: 0 and only the three standard Mathlib axioms. A sorry is Lean's placeholder for a step the author has not finished; zero of them means the proof kernel accepted every step of what was written into Lean.
So a machine certificate exists and an audit still found a false step. Both hold at once, with no paradox in it: what Lean certifies is the Lean file. The chapter is a separate object, composed for human readers, and the defect lived there. Assurance does not travel from one to the other by itself. The manifest is also quieter than it looks. Its declaration is named for a uniform case, while the chapter's claim covers all finite two-player, one-round entangled games, and the repository's own one-line description — “exponential parallel repetition for quantum games” — says nothing about how the two generalities line up. None of that suggests a discrepancy. It does mean a reader who wants to know which theorem was machine-checked has to go and read the Lean.
One step from the cryptography
The second audit landed on 17 August and sits much closer to money. Yuchen Guo and Shuo Yang published rigorous statements and proofs for three of Simon’s four lemmas (arXiv:2608.16598), addressing the Dihedral Coset Problem preprint by Daniel Simon of the AWS Cryptography Group that Quentir read closely on 10 August. Simon's analysis rested on four lemmas, three of them carrying proof sketches only.
Guo and Yang give each of those three a statement that admits a single reading, together with a complete proof, and corrections accumulate as they go. Lemma 1 holds with probability tending to one, where a constant was originally claimed. Lemma 3's amplitude bound follows from an exact Parseval identity and holds at every threshold with no well-behavedness hypothesis, so that predicate leaves the argument entirely. In Lemma 4 the exact balls-in-bins covariance carries a term that a fixed ball count omits, and the two branch amplitudes share a signed prefactor, so the counting estimates control the difference between them and never the ratio the lemma states; the authors prove the additive form.
Then the sentence that does the work. One hypothesis survives all of this: that the partition into the two sides be fixed independently of the measured string. The rule the algorithm gives for choosing that partition does not supply it. Establishing the four lemmas, Guo and Yang conclude, therefore does not by itself establish that the algorithm is correct.
Nothing standardized broke, and the practical status of ML-KEM is what it was in July. The connection here runs through a chain of reductions, not through the standard: Regev's route links certain lattice problems to the dihedral case, while FIPS 203 rests specifically on Module-LWE at concrete parameters that Simon's preprint does not reach. That parameter-and-regime gap is what Quentir's earlier reading set out in four conditions, and none of them has been met. What moved this fortnight is at the far end of the chain: a claim that read as “four lemmas, three sketched” now reads as “three rigorized, one hypothesis isolated and named.” That is a genuine change in the shape of a question that migration timetables quietly assume away, and two people reading produced it.
In code, the same week, a review that passed
On the same day Guo and Yang posted, the security firm Wiz disclosed a GitHub Actions injection in Snowflake's public .NET connector repository. The workflow file inserted an attacker-controlled issue title straight into a shell block, and because sanitization ran after GitHub's template expansion, a single quote in an issue title broke out of the quoted string and executed arbitrary commands on a runner holding internal Jira credentials. The change reached the main branch in pull request #1218 on 18 June 2026. Wiz's autonomous Red Agent found it, exploited it, reached the internal Jira and assessed the blast radius on 23 June without human intervention. Snowflake remediated the same day, rotated the token on 24 June, and found no evidence of unauthorized access.
Then the reading of the record came apart. The squash-merge commit lists “Copilot Autofix powered by AI” among its co-authors, and the first version of the disclosure took that as machine authorship of the flaw. GitHub disputed that reading, stating that a human wrote the contributions that led to the vulnerability and that Copilot Autofix neither reviewed nor contributed to them. On GitHub's account the unsafe refactor is dated 25 August 2025 and attributed to a named Snowflake engineer, Copilot's own documented change touched a different workflow file, and the co-author line rode along as an artifact of squashing the branch. Wiz revised its post the same day: Copilot was a co-author that checked the merged pull request, and whether the code change itself was AI-assisted is unclear.
Authorship of the vulnerable line, then, is on the record and belongs to a person. The question underneath it is still open, and the two firms have not closed it: whether an automated review looked at the code that shipped. Wiz's position is that the merged revision was scanned and the injection missed. GitHub's is that Copilot Autofix did not review those lines at all. The public pull request settles nothing either way — its automated annotation reports potential problems found, which is neither a clean pass nor a scoped audit — and the merge record cannot decide it, because a co-author field records participation in a pull request and says nothing about which lines were examined. Set that against the mathematics. An audit of Chapter 6 could name the exact inferential step that failed and hand back a corrected one. Here, two competent organizations read the same record and still disagree about what was checked. That matters beyond one repository, because when anti-hacking law looks through an autonomous agent to the human on the account, both the attribution and the assurance have to be supportable by the record.
How Quentir Reads It
The development worth naming is that verification has become a citable output with authors and a date on it. For most of the modern history of mathematics, checking was invisible labour absorbed by referees, seminars and graduate students, leaving almost no public trace. Two corrections in a fortnight, alongside a widening register of replication-grade negative results in applied quantum machine learning, suggests the corpus of claimed results has outgrown the system that used to absorb the reading, and the reading is surfacing as work in its own right.
That yields a usable three-grade scale. A claim on its own. A claim with a machine-checked artifact plus an explicit account of how that artifact relates to the prose. And a claim someone has read and, where necessary, corrected in public. Chapter 6 shows the second and third grades are no substitute for one another, which is no criticism of formalization; it is the reason a formalization manifest and a prose chapter deserve to be read as two documents.
For institutions whose obligations run through cryptography, the DCP thread is the one to hold. Migration deadlines now being written into procurement schedules assume the hardness assumptions underneath the standards hold. The past fortnight demonstrates how that assumption's status actually moves: through lemmas acquiring statements, hypotheses being isolated and named, and someone eventually publishing either a proof that the last one can be supplied or a demonstration that it cannot.
There is a civic edge here that the technical framing hides. The confidentiality of ordinary correspondence, of medical records, of payment instructions rests on a small number of mathematical assumptions that a small number of people have read closely. Machine-written mathematics leaves that arithmetic alone and changes the ratio between the two numbers. When the production of plausible argument scales and reading does not, the scarce resource is the reader. The Sienickis, and Guo and Yang, are what that resource looks like when it arrives on arXiv with a date attached.
These threads mean something in sequence — the DCP claim on 10 August, the attribution problem on 8 August, the rigorization this week — and the Quentir coverage linked here sits inside the All-access membership: what the membership adds over individual posts is continuity, the same threads carried edition to edition instead of restated.
Guo and Yang isolated one hypothesis and said in plain language that the algorithm's own rule does not supply it. As of today nobody has published either the proof that it can be or the demonstration that it cannot. Kempe waited eleven years for Heawood; this took a fortnight, which is progress of a sort. The number of people doing the reading has not obviously grown.
Sources: Mikołaj Sienicki and Krzysztof Sienicki, “Auditing an AI-Generated Mathematical Proof: A Correction to a Greedy Conditioning Lemma in Quantum Parallel Repetition” (arXiv:2608.14673), 3 August 2026. Yuchen Guo and Shuo Yang, “Rigorous Statements and Proofs of the Lemmas in Simon’s Algorithm for the Dihedral Coset Problem and Their Underlying Hypothesis” (arXiv:2608.16598), 17 August 2026. OpenAI, “Ten advances in mathematics and theoretical computer science”, August 2026, with the Lean 4 formalizations in the openai/ten-proofs repository and the formalization.yaml manifest that records the certified declaration and its sorry_count. NIST, FIPS 203, for the Module-LWE basis of ML-KEM. Wiz, “Red Agent exploits Snowflake vuln missed by GitHub Copilot”, 17 August 2026, including its 17 August update on Copilot Autofix's role, and the public pull request #1218 it concerns. TNW, “GitHub disputes Wiz’s claim that Copilot Autofix wrote a Snowflake flaw”, 18 August 2026. The Kempe, Heawood and Appel–Haken account follows the MacTutor History of Mathematics account of the four-colour theorem. All public pages checked 18 August 2026.
Published intelligence, built to inform your own decisions. Published: August 18, 2026.