What it cost, what the checks caught, and what is still wrong

Written by hand rather than generated, because the numbers in it come from six different commands and the point of it is the ones nobody would put in a summary on purpose. Every figure is from a command anybody can run, and the command is named next to the figure. It is true as of 20 August 2026 and it will go out of date, which is fine: reports/audit.md, reports/extraction-quality.md and reports/refs-unresolved.md are regenerated by CI and are the live numbers. This file is the part that needs a sentence around it.

What the transport cost

There is no invoice. Nothing here was billed per token. The pages went through chatgpt-tool on three small servers, driving signed in accounts rather than an API, so what was spent is wall clock, upload quota and cooldowns. bourbaki report usage counts it:

Forty three hours of wall clock, from 11 August 21:20 to 20 August 01:13, produced 745 pages. That is the number worth sitting with. Six thousand pages were sent and one page in eight came back. The other seven were not wrong, they were never answered.

Why the batches lost their pages, counted once per batch:

Five. Out of 5309 lost pages, five were the model failing to read the page. Everything else was the transport: an account banned, an account signed out, an account out of uploads for the day, or a batch that fell over and did not say why. The interesting engineering in this project turned out to be almost entirely about keeping a queue alive against a service that does not want to be driven this way, and almost not at all about reading mathematics off a page.

The 251 batches with no reason in the log are a hole in the instrumentation and they are counted here rather than rounded off. Nobody knows what happened to them.

As I write this every signed in profile on all three hosts is sitting out a cooldown and the first one is back in twenty six minutes. That is the ordinary state, not an outage. bourbaki fleet accounts says so.

What the checks caught

The rules are worth more than the corpus is, and this is the evidence for that. Each of these is a fault that was on main, that reads fine, and that a person would not have found by looking.

bourbaki refs build -check caught 51 reference manifests pointing at the wrong lines. The re-assembly in #159 rewrote the section files and every reference records the file and line it was read from. The text under them had not changed. Nothing looked wrong. Every one of those references would have sent a reader to the wrong paragraph. Fixed in #166.

S09, assembly is deterministic and what is committed is what it writes, caught 40 sections whose committed text no longer matched what the assembler produces from the same pages. The cause was ordinary: a change to the assembler in the solver merged while the content it produced sat in an unmerged corpus branch. Invisible in the files, invisible downstream, and it does not repair itself. Fixed in #159.

H06, the README coverage table is the one the corpus has, caught a coverage table twelve rows out of date. Fixed in #162, and the gate was tested by stashing the regenerated table and watching the build fail.

L05, a translation is not older than what it was made from, is holding 39 Vietnamese files that were made from English which has since been mended. This is the rule doing exactly its job. A stale translation is fluent Vietnamese that says what the older English said, and no amount of reading it will tell you. Tracked in #164.

M04, every math span parses, is the one that caught the checks themselves. It sits behind a flag, nothing had ever passed that flag, and the first time it ran over the whole corpus it reported 358 hard findings. Every single one was a formula that is right: it read the control space, a backslash followed by a space, as a command name that had been lost, and the corpus sets 448 of those. P04 parses the same spans with KaTeX and accepted all 358. Two rules disagreeing is what said which of the two was wrong, and the answer was the rule, not the text. Fixed in tamnd/bourbaki-solver#299 and it runs in CI now.

The extraction rules, run over what is on disk by bourbaki report extraction, accept 3303 of 3332 checked pages. The 29 rejections are 19 pages that are too short, 9 with a bad running head and 1 with prose leaking into a formula. That is 99.1 per cent on this machine and 98.9 on a clean checkout, where seven more pages count as short because the manifest that marks a page sparse lives under images/ and images/ is not in git. The report says which kind of run wrote it, so the two numbers do not have to be discovered twice.

The hard number to publish is this one. Of the 44 exercise solutions that have an answer, 22 have been read by a person, and 18 of those 22 readings found something the recorded status did not say. Eighty two per cent. bourbaki report solutions prints it as "disputed". The solver's own confidence about its own answers is wrong four times out of five when somebody checks, which is why the solutions are not being scaled up until the verifier is.

What is still wrong

The audit is not green. bourbaki audit -validate-tex over 64 rules that run and 2 that cannot:

The build is red on the 40 and will stay red until the fleet gives the accounts back. That is deliberate. The alternative is a threshold, and a threshold on a rule about whether a translation matches its source is a way of not knowing.

Two rules cannot run at all in the ordinary case. T05, tags is only ever appended to, needs a base commit. L09, the glossary version moves when the renderings do, needs a base revision. Both run in CI where there is one, and neither runs on a laptop. A rule that does not run is reported as not run rather than as a pass, which is the one thing this project has been consistent about.

253 references out of 5203 resolve to nothing, 4.9 per cent. Two thirds of those are numbered displays and loc. cit. that are supposed to resolve to nothing. The rest are real.

Three known faults have issues and no fix: #71, four volumes label their pages A where the book cites them LIE, TS and TA; #160, one page of Theory of Sets read with a line dropped; and tamnd/bourbaki-solver#266, a script in a stacked display measured against the wrong row.

The two historical note volumes have no chapter structure the table of contents parser recognises, because they do not have chapters. They are left alone rather than forced into a shape they do not have.

What has not been done at all

3398 of 14989 pages have been read, 22.7 per cent. Six volumes of 43 are read through, 14 are begun and 23 have never been opened. The percentage flatters it: it is not the library a fifth of the way through, it is six books done and 23 untouched.

78 of 325 sections are in the corpus, 24 per cent, carrying 1767 statements and 878 exercises, 2645 of them tagged.

Vietnamese is 269 of 968 files, 27.8 per cent, and the glossary is followed 98.5 per cent of the time. Chinese and Japanese have not been started. The milestone asks for all three.

44 exercises of 878 have an answer, 5.0 per cent, and 37 are believed, 4.2 per cent. The verifier has never been measured; bourbaki solve eval has not been run.

The whole pipeline has never been run from the PDFs on a clean checkout of both repositories. Until it has, the claim that the corpus is reproducible from the sources is a claim about the code and not a fact about the corpus.