A formal proof is not self-describing. It compiles against a library, and somewhere in that library sit assumptions the machine never verified: axioms taken as given, results proved elsewhere by hand, numerical bounds established by computation the kernel never saw. A reader who wants to know what a development actually assumes needs that list.
Lean has printed it from the beginning. #print axioms takes one declaration and returns every axiom it depends on, transitively, in a form a machine can compare. It is one line. It is almost never quoted in a paper.
The obvious diagnosis is that formal mathematics is young and its conventions have not settled. This desk probed that diagnosis on 4 September and it does not survive. Isabelle ships thm_oracles, which answers the same question about the same kind of object, and it is roughly thirty years older. It is quoted less.
What is missing is not the measurement. It is a vocabulary for what the measurement returns. A result proved by Deligne in 1974 and a numerical bound the authors established themselves last month both appear as axiom, and they print identically. Until there is a word for the difference there is no sentence to put in a paper, and a one-line command with no sentence around it does not get run.
This desk spent the week proposing that word and then withdrawing the proposal. Isabelle’s manual already carries a noun for the object — oracle — machine-checkable and three decades in use. A coinage that must unseat an incumbent term with tooling behind it is a weaker claim than the one worth making: that the existing instruments should be run and their output printed. The note now says so.
This page was drafted arguing that the axiom line is never quoted. Eleven days of machine time in mid-August, announced on 4 September, spent that argument and replaced it with a better one. Anthropic reports an end-to-end Lean proof of Fermat’s Last Theorem — thirteen million lines, some 29,500 intermediate theorems — and the completeness claim it makes is not a line count. It is the axiom line. The build, in the authors’ words, “fails unless the final theorem rests on exactly Lean’s three standard axioms — propext, Classical.choice and Quot.sound — with no sorry anywhere.”
So the instrument was not missing, and it is no longer unquoted. What the announcement shows is narrower than the claim this page began with, and more useful: the habit forms when the stakes are high enough to require it, and it took the largest formalization ever produced to make one line of output the definition of done. The vocabulary gap looked still open — the three axioms had to be spelled out in prose, because this desk could find no standard citation for them.
Correction, 10 September 2026. There is a standard citation, and it was in use while this page was being set. The mathlib initiative publishes a formalization.yaml schema whose per-declaration entries carry an axioms list beside a sorry_count, an automation block naming the models used, and a review status. OpenAI’s Navier–Stokes and Euler repository populates all four fields for each of its four headline theorems — sorry_count: 0, [propext, Classical.choice, Quot.sound], models: GPT-6 Astra, status: self-assessed — and its Comparator configurations go further, setting permitted_axioms to those three names so the independent checker enforces the set rather than reporting it. What this page called a missing layer is a new and unevenly adopted one. The narrower claim above survives; the sentence this corrects does not. Full reading: WP-107 §10.
Two further disclosures in that report belong on Page 2, because they are about counting. The authors state that roughly two in five theorem statements inside the proof files repeat, word for word, a statement already made in another proof file. And the project’s own limitations file says of its restricted theorems that none “should be cited as a formalisation of the general classical theorem”. A duplicate rate and a statement-scope caveat, printed beside the headline, in the same week this desk found its own.
Rather than argue for the missing measurement, this desk built it. A census now runs over eleven repositories and 264 tracked files and reports what is written, what is free of sorry, what the kernel has audited under a pinned toolchain, and what is taken as an axiom — in two columns, raw and de-duplicated, with the convention printed beside the number. 1,963 declarations, 1,783 of them free of sorry, 173 kernel-audited, 53 axioms disclosed. The full table is on Page 2.
Its first run was against the corpus that built it, and that is the run worth reporting. A working document had put the clean core at 134 theorems. The census returned 86: three files — a working copy, a draft and a self-check — hold the same twenty-four, and each had been counted whole. The mathematics did not move. The denominator did.
Which is what an instrument is for, and the reason to run one before publishing rather than after. The script is committed in the repository it counts, so a reader who disagrees with the convention can recompute the answer under their own.
Alongside it, one new chapter went out this week: Book 4, Chapter 21, which puts the Gauss map back between the contact chapters and projective duality. It is the subject of Page 3, and the week’s reading list is at the foot of that page. Page 4 carries the arithmetic: Fermat’s 1657 challenge, and the answer Bhāskara had printed in 1150.
#print axioms outputsorry across the measured corpus — ninety-one per cent, de-duplicated, convention statedWhat a count owes. Two figures computed on different denominators can both be correct and still describe a corpus that does not exist. The rule this desk now works to: print the convention beside the number, or do not print the number.
A formalization corpus is usually described rather than measured. This one is now measured. The census runs over a declared list of repository roots, reads every tracked .lean file, and reports two columns — raw, and de-duplicated across version-suffixed copies — because those are two different questions and the difference is where most published formalization figures go wrong.
| Measured 4 September | raw | de-duplicated |
|---|---|---|
| Repositories in the census | — | 11 |
Tracked .lean files | — | 264 |
| Declarations written | 2,751 | 1,963 |
Free of sorry | 2,481 | 1,783 |
Admitted, carrying sorry | 270 | 180 |
| Kernel-audited under a pinned toolchain | — | 173 |
| Axiom declarations, disclosed | — | 53 |
De-duplication collapses version-suffixed copies of the same file; 41 such groups exist. Ninety-one per cent of the de-duplicated corpus carries no sorry. The convention is stated because a count without one is not a measurement.
| Delivered | Standing | Date |
|---|---|---|
| Volume I proofs released under licence — MIT for the code, CC BY for the prose | 86 theorems, 0 admitted, 0 added axioms, verified file by file | 4 Sept |
| Reflection file, Riemann arc, Book 4 | 11 theorems, 10 kernel-checked against the allowlist, 1 admitted — and the admitted one now carries its four hypotheses explicitly | 2 Sept |
| Chapter 21, the Gauss map and the conormal variety, with three constructed diagrams | Closes the gap between the contact chapters and projective duality. Page 3 | 5 Sept |
| Census instrument, run over all eleven roots | Committed beside the corpus it counts; a reader may disagree with the convention and recompute | 4 Sept |
| Two federal research elements in preparation, both under dual-anonymous review | Neither is described here, for that reason. A third notice of intent is on file and accepted | Sept |
| XIII LAW3M package lodged — abstract, technical brief, certification script, two posters, prototype schematics | Natal, 19–23 October | Aug |
Run against the corpus that built it, the census returned 86 theorems in the clean core where a working document had claimed 134. Three files — a working copy, a draft and a self-check — hold the same twenty-four theorems, and each had been counted whole. The mathematics did not move; the denominator did.
That is the case for the instrument, made at its own expense and worth more than a clean bill would have been. Every serious formalization effort has this failure mode. Almost none of them has run the check, and until this month, none of them published the number that comes back.
This month one did. The Fermat formalization announced on 4 September reports that roughly two in five theorem statements inside its proof files repeat, word for word, a statement already made in another proof file — disclosed by its authors, in the same document as the result. Thirteen million lines and a duplicate rate printed beside them. The convention this page argues for is not a house style: it is what the largest formalization ever produced had to state about itself before its counts could be read.
Corrections
Two pages of Book 4 and one section of the reflection note recorded chiLog_real_on_critical_line as admitted. It was proved and kernel-audited on 30 August. The file consulted was a retired snapshot in an evidence directory. Corrected 2 September; the live path is now the only path a claim is read from.
Three working documents reported a solicitation document as missing. It was on disk, one directory from where the search ran. Corrected 2 September.
A researcher identifier was transcribed from memory and was wrong in two digits. The correct value occurs 1,250 times in the corpus. Corrected 2 September.
The chapters run: a contact form on a three-dimensional space, Legendrian submanifolds, then — some pages later — a projective variety and its dual. Each step is defensible. The passage between them was a leap, and the missing rung has a name. The new chapter is Book 4, Chapter 21: The Gauss Map and the Conormal Variety, published this week.
Gauss, 1827. For a surface $X \subset \mathbb{R}^3$ the Gauss map $N : X \to S^2$ sends a point to its unit normal. Its derivative is the shape operator, and the theorem that made the subject is that
is intrinsic: computable from measurements made inside the surface, with no reference to the ambient space at all. That is the Theorema Egregium, and its content is that a map to an auxiliary space — the sphere of directions — recovers something that never mentioned the auxiliary space. Gauss–Bonnet then integrates it, $\int_X K\,dA = 2\pi\chi(X)$: a local differential quantity summing to a number that only counts holes.
A projective variety has no unit normal — there is no metric to take one from. What it has is a tangent space at each smooth point, and in $\mathbb{P}^n$ that tangent space spans an embedded tangent hyperplane. So the auxiliary space is not $S^2$ but the space of hyperplanes, $(\mathbb{P}^n)^\vee$, and the map
is the Gauss map of algebraic geometry, defined wherever $X$ is smooth. For a hypersurface it is written down directly: $\gamma = [\partial_0 F : \cdots : \partial_n F]$, the gradient of the defining equation, which is a morphism exactly off the singular locus.
This is the identity the series was missing. Inside $\mathbb{P}T^*\mathbb{P}^n$ — the projectivised cotangent bundle, whose points are pairs (point of $\mathbb{P}^n$, hyperplane through it) — sits
For a hypersurface the condition $\mathbb{T}_x X \subseteq H$ forces $H = \gamma(x)$, and $\mathrm{Con}(X)$ is literally the closure of the graph of the Gauss map. In general it is the conormal, and the graph statement holds after replacing $\gamma$ by the map to the relevant Grassmannian. Either way $\dim \mathrm{Con}(X) = n-1$, whatever the dimension of $X$ — which is the first sign that the right object is the graph and not either projection.
$\mathbb{P}T^*\mathbb{P}^n$ carries a canonical contact structure of dimension $2n-1$, and $\mathrm{Con}(X)$ is Legendrian in it — maximal isotropic, dimension $n-1$, exactly half of $2n-2$. The contact geometry of the earlier chapters is therefore not a motivating picture placed alongside the algebra. It is the ambient category the duality lives in, and the Legendrian condition is what makes the correspondence symmetric.
The canonical isomorphism $\mathbb{P}T^*\mathbb{P}^n \cong \mathbb{P}T^*(\mathbb{P}^n)^\vee$ exchanges the two projections. Under it $\mathrm{Con}(X) = \mathrm{Con}(X^\vee)$, and therefore
It would be easy to file that as a formality. It is not, and the way to see that it is not is that it fails in characteristic $p$. There the Gauss map can be inseparable — in characteristic two every tangent line of a smooth conic passes through a single point, so the dual degenerates and the second dual does not return. Biduality is a characteristic-zero theorem with a stated hypothesis and a known counterexample outside it, which is the only kind of statement worth putting at the top of a ladder.
Two consequences are checkable and were checked. The Gauss map has a degree, and for a smooth plane curve of degree $d$ the dual has degree $d(d-1)$ — the number of tangent lines through a general point. And the singularities of $\gamma$ are, generically, folds and cusps, which is why $X^\vee$ acquires cusps and nodes and why the Plücker formulas take the shape they do. The analogy with $\int K\,dA = 2\pi\chi$ is a heuristic, not a derivation, and the degree formula is the theorem; the paper says so in those words.
One row of the chapter’s inventory is marked open and stays that way. The contact form this corpus actually uses, $\alpha = dz - r^2\,d\theta$, is written on a real three-manifold. Whether it arises as the pullback of the canonical form on $\mathbb{P}T^*\mathbb{P}^2$ under any algebraic map is not established here, and until it is, the ladder connects two subjects rather than one. open
Fermat circulated the challenge through Digby to Wallis and Brouncker, naming two cases to try: N = 61 and N = 109. The choice was not innocent. For most small N the smallest solution is small; for 61 it is not. The answer is
and a reader can confirm it in a minute with a calculator, which is the whole point of the shape of the claim. Finding it is another matter. Fermat knew that, and chose 61 because he expected it to be out of reach.
It was not out of reach. It was in a book. Bhāskara II gives exactly these two numbers in the Bījagaṇita of 1150, obtained by the chakravala — the cyclic method — which drives a composition rule that Brahmagupta had written down in 628. Fermat set as a test of European mathematics a number that had been in print in India for five centuries, in a language he did not read.
Brahmagupta’s rule — he called it bhāvanā, production — is a single algebraic identity:
Read what it says. The quantity x² − Ny² is multiplicative: feed it two solutions and it returns a third. Two answers make a new answer, and a near-answer can be driven toward an exact one. That is the engine, and it is the reason a ten-digit solution is findable at all by hand.
In modern terms it is multiplicativity of the norm on the ring ℤ[√N], and the solutions of x² − Ny² = 1 form a group under it. Brahmagupta had the law in 628. The words norm, ring and group arrived twelve hundred years later. The identity did not need them — which is the observation worth keeping.
A file, Bhaskara.lean, states the identity, both of its sign variants, the composition as a closure property, conjugation as the group inverse, Bhāskara’s solution, one bhāvanā step applied to that solution and itself, and the second challenge case N = 109. Twelve declarations — eleven theorems and one definition. No sorry in code. It compiles in 202 seconds against Mathlib under Lean 4.32.0.
By this paper’s own three-tier rule that places it at tier three — kernel-audited. The audit appends #print axioms for every theorem in the file and reads back what each one rests on: eleven declarations, none trusting sorryAx or native_decide.
Two things about that sentence are worth saying exactly, because they are what this issue is about. Eleven, not twelve — the gate probes theorem and lemma, and IsPell is a definition, so the audited count and the declaration count are different numbers measuring different things. And the gate tests for the two axioms that break trust, not for the whole axiom set. What is established is that nothing here is admitted or decided by native evaluation. That is weaker than the claim the Fermat formalization makes about itself, where the build fails unless the axioms are exactly the standard three.
Not that Bhāskara proved Fermat’s theorem. Fermat asserted that x² − Ny² = 1 is solvable for every non-square N and gave no proof; the first European proof is Lagrange’s, 1768. Chakravala always terminates, but its termination was not established in the modern sense until much later, so Bhāskara did not have the general theorem either.
The sharp claim is the checkable one: the specific number Fermat used to test Europe was already published. That survives contact with the record, and the looser version does not.
On 4 September a second Fermat claim closed. The marginal note of about 1637 — the one with no room for the demonstration — now has an end-to-end machine proof, and the announcement makes its completeness claim in exactly the form Page 1 is about: the build fails unless the theorem rests on three axioms and no sorry.
Two Fermat claims, then, in one issue. One took three hundred and fifty-eight years to prove and eleven days to check. The other was never his to begin with. What they have in common is the thing this paper keeps returning to: for centuries the only justification either claim carried was that it could be checked — and a claim that can be checked, printed where strangers can reach it, outlives every argument that was never written down.
The serial on Page 6 is standing in the same year from the other side: Versailles, 1665, six weeks that became four days, and a man recalculating a plan that had already broken.
| 628 | Brahmagupta states the composition identity and solves several cases |
| 1150 | Bhāskara II gives x² − 61y² = 1 by chakravala |
| 1657 | Fermat poses N = 61 and N = 109 to England as a challenge |
| 1768 | Lagrange proves solvability for every non-square N |
Bhaskara.lean, and admitted ones. Eleven theorems, one definition; compiles in 202s under Lean 4.32.0#print axioms, and any trusting sorryAx or native_decide. Tier three, on this desk’s gateOne step of bhāvanā. Composing Bhāskara’s solution with itself gives
6 239 765 965 720 528 801
798 920 165 762 330 040
again a solution. The group is infinite, and the identity is the only thing needed to walk it.
Pablo Nogueira Grossi. Eleven years in banking — Banco do Brasil (2003–2014) and JPMorgan (2006–2009) — and, since, a decade in SEVP/F-1 education running the full ladder from classroom teaching through curriculum administration, programme director and school director.
Recently. Gold, Silver and Bronze medals, WorldQuant International Quant Championship 2026, and a consulting engagement with WorldQuant BRAIN signed 28 August. Forty-three open-access deposits. Presenting at the XIII LAW3M, Natal, 19–23 October 2026.
Three earned bachelor’s degrees. B.B.A. in Finance & Economics, Baruch College, CUNY (2015). B.A. in Economics & Computer Information Systems, Baruch College, CUNY (2013). Both completed on study leave granted by Banco do Brasil headquarters. Bacharelado em Turismo, UPIS, Brasília (1999–2003, Class President), with credit from the Universidade de Brasília, where the geology came from.
M.S. in Computer Science, University of the People — in progress.
Works in SQL, Python, Lean 4, retrieval-augmented generation, machine learning, and dashboards built from scratch in Excel. Reads and writes English, Portuguese and Spanish.
What he is looking for. Colleagues who are excellent at something he is not, and a problem worth being wrong about in public.
G6 LLC is a small research entity. This paper is unpaid and so is everything it reports on.
A weekly that states its results in a form that could have come out otherwise, and checks them before printing. That a k-fold symmetric ring on an even number of sites keeps exactly one non-constant mode, the folding frequency, precisely when N = 2k — twelve sites for the hexagon, twenty for the decagon — first swept numerically, now a theorem with six declarations through the kernel. That a growth constant used throughout this corpus is the Tribonacci root to sixteen decimal digits, and is not the LAW3M ratio it was nearly merged with; the two stand 5.23 per cent apart. That an operator chain written unbracketed for three years associates strictly at two levels of abstraction and only up to isomorphism at the third — kernel-checked, and invisible in prose.
Errors go dated into the corrections column, which is where they belong and where they stay. What is offered here is the other column: results, stated so that someone else can knock them down, by someone who tried first.
XIII LAW3M — Natal, Brazil, 19–23 October 2026. Submission package lodged: abstract, technical brief, the certification script for the inner basin boundary, two posters and prototype schematics. A month out at the time of writing.
Volume I proofs released. The Lean development is now licensed and public — MIT for the code, CC BY 4.0 for the accompanying prose. Eighty-six theorems, none admitted, no axioms beyond the three the standard library itself assumes. It is the part of this corpus a reader can check without taking anything on trust, and it is the part offered first.
The census is public too. theorem_census.py runs over a declared list of repository roots and prints the table on Page 2 in both columns. Every figure this paper quotes about its own corpus comes from it, and disagreement with a convention is settled by re-running it rather than by argument.
Corrections for this issue are on Page 2, dated, with the correction date beside each. Three items, all closed. This paper runs its corrections in every issue on the same page and in the same form, whether or not there is anything else to report that week.
She was not supposed to leave for another six weeks. Fermat had built the whole shape of it around that number — his commission granted, his affairs settled, his fever timed to a season when three parishes already had plague and no physician would look twice at a fourth quiet death. Six weeks was not arbitrary. Six weeks was the distance between two disappearances close enough to matter and far enough apart that no clerk, however clever, would think to draw a line between them.
She left in four days.
It was not a plan that failed. It was a king who would not wait.
He had summoned her twice in one week, which he had never done before, and the second time he had not asked her to sing, or to sit near him while he read dispatches, or to do any of the small ornamental things he usually wanted of her. He had simply looked at her for a long moment and said, “I am tired of admiring things from a distance, Marie,” in the particular tone he used when he had already decided something and was only informing the room of the decision, not asking its opinion.
She understood, walking back to her rooms that night, that the six weeks did not exist anymore. There was tonight, and there was tomorrow, and after that there might not be a version of her life she recognized well enough to plan inside of.
She did not send word to Toulouse. There wasn’t time, and worse, she wasn’t certain the roads were still safe for a letter that said what this one would have to say. She took what fit in a single case, left the rest exactly where it stood — a scattered detail was more convincing than a clean one, she had learned that much from watching Fermat build his own disappearance — and was gone before the palace had properly woken.
Fermat learned of it nine days later, from a merchant he half-trusted, in a letter that said almost nothing directly and meant everything.
The bird has left the garden ahead of the gardener’s schedule.
The garden does not yet know.
He read it twice, standing in his own study surrounded by the second set of books that existed only in his head, and felt, for the first time since he had begun any of this, something close to fear — not for himself, but for the arithmetic. His plan had never accounted for a version of events in which she moved first and he was left to catch up to a decision already made.
He did the only thing his training had ever taught him to do with an equation that no longer balanced: he solved for the new unknown.
If she was already gone, already unaccounted for, already the subject of whatever quiet, urgent search a king mounts for something he has decided he wants and finds missing — then Fermat’s own six weeks of careful invisibility were not a luxury anymore. They were a liability. A magistrate who died at Castres after a woman went missing from Versailles was a coincidence. A magistrate who died at Castres two months after was a pattern, and patterns were the one thing his entire life’s work had taught him to notice in other men’s mistakes.
He sent for his physician that same afternoon, and told him the fever had come early.
He did not know, yet, whether she had reached the coast. He did not know whether the ship still waited, or whether nine days was already too long a silence for a captain paid to be discreet, not loyal. He knew only that the careful shape of his plan — the one thing in his life he had built with the same precision he brought to a proof — had already broken before he’d had the chance to test it.
Some things could not be proven in advance, he had told her, the night before he left. They could only be attempted, and then lived.
He had meant it as comfort. He had not expected to be tested on it quite so soon, nor to find, turning the words over now with real fear behind them for the first time, how much less comforting they were when the proof in question was a person, and she had already gone ahead into the dark without him.
Part 4 of 18 · Fiction, drawn from the documented record; what is invented and what is not is set out in the series’ own note on fact and fiction. © 2026 Pablo Nogueira Grossi · G6 LLC.
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. Fermat was born in 1601 and sat thirty years on the bench of the Parlement of Toulouse. In May 1653 he caught bubonic plague and survived, weaker afterwards; Bernard Medon, a judicial colleague, wrote to the Dutch scholar Nicolas Heinsius the Elder announcing Fermat’s death — and withdrew it in his next letter. That accident is the seed of the whole premise, and it happened. He died at Castres on 12 January 1665. Clément-Samuel inherited his father’s offices that year and published the Diophantus with the marginal commentary in 1670.
Invented. That the death was arranged — the death itself is real and dated; the faking is the fiction. Marie. The six weeks, the four days, the merchant’s letter. The physician who is told the fever came early is Duval, invented, and is not Medon: Medon’s report was an accident in 1653 that a second letter undid, and Duval is what it looks like when someone reads that accident as a method.
Each issue, when it goes out. No list bought, harvested, or lifted from a conference roster. Unsubscribe by replying with the word stop.
[propext, Classical.choice, Quot.sound], no sorryAx.corpus_roots.txt beside it. Ten checkouts, git-tracked only, raw and grouped reported separately.
Vol. 9 · The Mathematics — the companion sheet to this issue: percolation and the cusp, with the figures at full size.