On 16 October Cristian Cobeli and Alexandru Zaharescu posted a proof, with no unproved hypothesis, that the lower limiting proportion of nontrivial zeros of the Riemann zeta function that are simple or lie on the critical line is greater than 8/9, zeros counted with multiplicity. The constant their method produces is about 0.88893. The previous unconditional bound in the paper’s own account is Lamzouri’s 0.88762. This is a statement about a proportion of the zeros. It says nothing about the remaining ninth, and it is not the Riemann Hypothesis. Page 3 sets it beside two other outside results.
Book 4 went the other way. Chapters 13, 14 and 14A had described a contact condition as equivalent to the Riemann Hypothesis. That equivalence is not shown, and on 19 October the claim was withdrawn: the RH paper gained a new §4.9, the chapters carry dated correction boxes, and a six-check script reproduces the numbers in about 47 seconds. Page 4 lists each change.
That is the thread of this issue. Page 2 puts the series’ own count of kernel-checked theorems next to what the count does and does not establish. Page 5 is the open desk: what is still unchecked.
None of the Lean was rebuilt for this issue. The Reading Room, Page 6, carries Part 9 of the serial, set from its source.
8/9 is 0.88889. The new constant is about 0.88893, so the margin is roughly 0.00004. The gain over the earlier bound is about 0.0013. The distance from 8/9 to certainty is the remaining 0.111.
The paper’s Sections 4–6 were not re-derived for this issue; the figures above are the paper’s own.
The count of kernel-checked theorems is the number people reach for first. It answers one question only: did the Lean kernel accept the file. Two further questions sit behind it. Does the theorem say what its name and docstring say, and does the model it describes match a real system?
| Repository | Kernel-checked | Vacuity-scanned |
|---|---|---|
| vol1-proofs | 82 (58 + 24) | yes, 0 flagged |
| geometry | 31 | no |
| io | 16 | no |
| Total | 129 | 82 |
The ledger records later io counts of 20 (21 September) and 30 (24 September); this table keeps the 25 August snapshot so every row is from one date. The 82 are 58 in PrincipiaVol1 and 24 in AutophagyDm3; geometry’s 31 are SaturnHexagon 5, NASAGaps 12 and G6Crystal 14.
Level 1: the kernel accepts it. Of the 82 Volume I theorems, 29 are named in geometry’s foundational documents and 53 are not. No mapping from a numbered Result to a Lean name exists in either repository. So “Volume I is machine-verified” is today a statement about a file in another repository.
Level 2: the content is checked. A vacuity scan flags conclusions that are trivially inhabited, such as True or ∃ _, True. It ships with five deliberate vacuous specimens and one honest control, so the instrument is tested before its verdict counts. It returned 0 flagged over the 82. It has not been run on geometry’s 31 or on io, which are kernel-checked and unverified for content.
Level 3: the model meets data. The dm³ toy model of Volume II has a contraction bound τ = √(c/κnoise) (Vol II Thm 3.2), with V = ρ² canonical. Volume I’s (c, κ) = (1, ¼) is stated without derivation, and no erratum is written until its origin is found. A row in the translation table moves from analogy to model to established only on that field’s data or a derivation, and nobody yet knows how close the toy model is to the empirical systems.
| Paper | What it claims | What checks it |
|---|---|---|
| Cobeli & Zaharescu, arXiv:2610.23467 (16 Oct 2026) | More than 8/9 of the nontrivial zeta zeros are simple or on the critical line, unconditionally, counted with multiplicity. | A proof read by referees and readers. The paper credits an earlier unconditional bound to a proof written by Claude and verified by Alpöge and Furman. |
| Glazer et al., FrontierMath, arXiv:2411.04872 (v7, Dec 2025) | A benchmark of hundreds of original problems; each has one exact answer checked automatically. | A script compares the final answer. It certifies the answer, not the reasoning. The paper’s “under 2%” is its original 2024 figure; current scores are not quoted here. |
| Marinov & Veselinov, arXiv:2602.09253 (9 Feb 2026) | An elementary meromorphic function whose derivative has infinitely many roots, at which f takes infinitely many distinct values, is not solvable in elementary functions. | A proof in one-dimensional topological Galois theory. The definitions of “solvable” and “elementary” are what the theorem is about. |
Cobeli and Zaharescu describe three ingredients for passing 8/9: a spectral remainder of a Gram matrix that the earlier proof dropped, an inequality for seven ordered points summed over blocks of 120, and a choice of parameter that sets the constant. The proofs in their Sections 4–6 were not rechecked here.
A kernel can accept a theorem whose conclusion is empty, and a script can accept a number reached by an unsound route. A human reader can miss a step. The series’ standing rule is the one that fits all three: read what the claim says, not what its name promises.
Continued on Page 4 · Corrections| Where | What changed |
|---|---|
| Book 4, RH paper (and the root RH_arithmetic_contact_structure.md) | New §4.9, “Editor’s correction (2026-10-19)”: the argument that the condition fails for σ > 1, the numbers, and the two known conditions that survive (Laguerre and Lagarias). A correction line under the abstract; Conjecture 6.1 and Step 4 reworded so they no longer claim equivalence. |
| Book 4, chapter 13 | The bridge to chapter 14 now says the condition is stated as a conjecture. |
| Book 4, chapter 14 | Dated correction box. “Equivalent to RH” changed to “conjecture” in the introduction, the ladder caption, the positivity list, §14.4, the inventory table and the interactive ladder. The claim that RH implies positivity is withdrawn until a written proof is supplied; chapters 11–12 were not checked for one. |
| Book 4, chapter 14A | Status box and Consequence line corrected. §8 now covers the commutator problem for bounded operators (the trace of a finite-matrix commutator is zero, so it cannot equal a nonzero multiple of the identity), why the p-adic coordinates of φ are constant, and the sign difference in how 14A and the paper define g. |
| Verify script | Six checks, all pass, about 47 seconds. Check 6 is the prime-by-prime test: each local factor repeats with period 2π/log p, averages to zero, and has size about log p·p−σ, so the limit over primes is the zero function, a fixed point but a trivial one. |
| chGravity-scales | Central claim reworded as a conjecture, with a list of what would make it a theorem (18 October). |
Lines that still say “equivalent to RH” are inside the corrections, about Weil’s criterion (a real theorem), or the conditional sentence about chapter 15.
Not yet done. §4.7 of the RH paper has not been updated for the Cobeli–Zaharescu bound. Until it is, that section’s statement of the proven proportion is out of date.
| Item | State |
|---|---|
| ZeoliteCommutation.lean, the −6 commutator | To be checked that the file states it as an assumption. The finite-matrix trace argument shows a bounded commutator cannot equal −6 times the identity. open |
| RH paper §4.7 | Needs the Cobeli–Zaharescu bound written in with its limits stated. open |
| Volume I: numbered Result to Lean name | 53 of 82 theorems unnamed in the foundational documents; no mapping yet. open |
| Volume I Lean port | A port-v4.32 branch exists; the claim of 82 rests on the pinned toolchain until it is done. open |
| The (c, κ) split in Vol I | Stated without derivation; unexplained; no erratum until found. open |
| Vacuity scan on geometry (31) and io | Not yet run; a probe file plus one CI step. open |
| Chapters 11–12 of Book 4 | Not checked for a proof of RH implying positivity. open |
You are invited to join a math study group that meets online, in the library. Everyone is welcome.
To join, or to ask when it meets, write to g6llc@proton.me.
The Reading Room follows on Page 6.
Continued on Page 6 · The Reading RoomThe buffalo did not so much land them as simply stop, at some point in the grey hour before dawn, in water shallow enough that stopping was possible, and Fermat understood only afterward that this had been its own kind of mercy — that the beast had chosen the moment of arrival as carefully as it had chosen everything else about the crossing, waiting until the storm's worst violence had spent itself before it allowed the two of them to slide, boneless, into the wet sand.
He lay there for a long time without moving, salt-crusted and blind with exhaustion, aware only that Marie was somewhere near him, breathing, which was more than he had let himself hope for during the worst of the swim. When he finally raised his head, the world had gone the flat, colorless grey of very early morning, and the buffalo — his buffalo, he found himself already thinking, with an ownership he had no right to and did not intend to examine — stood a few feet off, utterly unbothered, as though it had done nothing more remarkable than cross a particularly wide puddle.
"We're alive," Marie said. It was not a question, but it did not sound entirely certain either.
"We are extremely alive," Fermat said, "and extremely covered in sand, which I am given to understand is not the same as being safe, but is a considerable improvement on the alternative."
It was only now, with real light finally reaching the flats, that either of them properly saw the thing that had carried them. In the storm it had been a shape, a grip, a fact to be grateful for without examining too closely. In the grey morning it was simply enormous — a vast, slate-hided animal the size of nothing either of them had ever stood beside, horns swept back like something out of an old bestiary, entirely too large to have swum an open, storm-churned sea with two drowning Europeans clinging to its back, and entirely unbothered by having done exactly that.
Marie stared at it for a long moment, then pushed herself upright in the sand, brushing at her ruined skirts with the particular dignity of a woman determined to recover at least one scrap of composure.
"I am extremely grateful to it," she said. "I want that understood. But I would never ride such a creature again. Not for any reason."
"Noted," said Fermat, who had learned, over six years, exactly how much weight to put on Marie's declarations of what she would never do, which was to say: precisely as much weight as the next hour of circumstance allowed her to keep.
The sun came up fast, the way it seemed to do everywhere in this part of the world, with none of Europe's slow, apologetic dawns, and with the light came the tide's retreat, drawing back off the flats in front of them with a long, hissing sigh — and with the retreating water came the sand itself waking up.
Fermat saw the first claw before he understood what he was seeing: a bright, improbable blue, waving up out of a hole in the mud as though the earth itself had grown a hand. Then another, and another, dozens, then what looked like hundreds, the whole flat suddenly alive and bubbling and clicking with creatures the size of a man's open hand, shells the impossible colors of a court painter's most extravagant palette, advancing across the sand in a slow, scuttling, entirely serious tide of their own.
Marie made a sound he had never heard her make in six years of knowing her — not a court sound, not a composed sound, nothing that Versailles had ever trained into her — and scrambled backward so fast she nearly fell, catching herself instead on the buffalo's foreleg and hauling herself, with a speed her ruined skirts should not have permitted, up onto its broad wet back.
"Those are not natural," she said, from a height she clearly intended to keep.
"They are extremely natural," Fermat said, watching one particularly large specimen wave a claw the color of a robin's egg in what he chose to interpret as a greeting. "Nature has simply declined, in this part of the world, to consult European taste before deciding what a crab should look like."
"I don't care what they are, Pierre, I care that there are a thousand of them and they are coming this way."
He considered the advancing tide of claws with the same flat, assessing attention he had once given a difficult legal brief, weighed it against his own aching, sand-caked, sixty-four-year-old legs, and arrived, not for the first time in recent memory, at a conclusion his life's work had never quite prepared him to phrase so plainly.
"I find," he said, already turning to look for a handhold of his own on the buffalo's broad grey shoulder, "that I would very much rather be eaten by nothing at all than stay here to discover which of us they intend to try first."
The buffalo, for its part, showed no interest whatsoever in the small blue army assembling around its feet. It simply began to walk, unhurried, its great hooves finding the firm ground beneath the mud without any apparent effort, crushing an idle path directly through the scuttling ranks as though they were no more than a particularly loud patch of gravel — carrying an old mathematician and a woman who had once outlasted the sharpest tongues at Versailles, both of them equally undone, for the moment, by an army of crabs.
Part 9 of 18 · Fiction, drawn from the documented world; the ledger below says which is which. Set from its source file, as written.
Rights notice. Pierre et Mademoiselle is not covered by this issue’s CC BY 4.0 licence. The serial and the work it belongs to — a limited series in development — are © 2026 Pablo Nogueira Grossi / G6 LLC, all rights reserved. No licence to reproduce, adapt, translate or perform it is granted here.
Documented, as the series ledger (FACT_AND_FICTION.md) records it; not independently re-checked here. The route La Rochelle, Tortuga, the Guiana coast, Maranhão was a functioning French Atlantic corridor in these years. The buffalo legend of Marajó is a shipwreck around 1890 near Cabo Maguari; its survivors swam ashore. The ledger has no entry for the sandbar, the mangrove flats or the crabs, so this part asserts nothing documented about them.
Invented: the landing on the sandbar, the crabs and the remount, and the buffalo carrying the two travellers onward. The buffalo swimming people ashore is a relocation of the Marajó legend 224 years earlier, as the ledger says for No. 8, not a fabrication of the animal.
Each issue, when it goes out. No list bought, harvested, or lifted from a conference roster. Unsubscribe by replying with the word stop.
tools/corpus_count.py · tools/self_reference.py — entity-aware counting, and the vicious-circle test. Both standard library only.sorry, standard axioms only.