M8: Exercise solver

[tamnd]

• Port taocp-solver's solver, prompt, result, textguard and adapt to the Bourbaki corpus adapter: solve/engine.go, prompt/solve.go with the solve_*.md templates, solve.Store plus report solutions, and textguard. pricing is deliberately not ported, since the fleet is ChatGPT web sessions and bills nobody; see the comment of 2026-08-19
• Context assembly: § text, sibling exercises, depth-2 transitive references via refs.json, out-of-corpus reference handling
• Candidate-blind reference call with obligations and falsification tests
• N-candidate generation from three distinct angles
• Obligation-wise selector
• Truth judge + reference-blind audit judge; both must pass
• Bounded correction loop
• Multi-part exercise decomposition with per-part status
• Outcome taxonomy: verified / partial / unverified / blocked / open
• solve run, solve review, report solutions
• 20-exercise hand-checked benchmark: benchmark/set.json, 10 accepts and 10 rejects over 20 distinct exercises, bodies in the corpus at benchmark/en/
• eval reports a false-accept and a false-reject rate on that set
• Pilot: solve Chapter VIII § 1 exercises 1–9 and read every one
• Long run: solve --all --status unattempted
• Every solution written in the delimiters this corpus reads. mathtex.Split recognises the dollar and the double dollar and nothing else, so a solution set in the other pair of TeX delimiters carries no math span at all, and eight solutions of Theory of Sets were written that way. 485 spans between them, invisible to M01, M04, P04 and the reference graph since the day they were generated (Set eight solutions in the delimiters this corpus reads bourbaki#145)
• The audit names a solution written on the free gateway. A solution is the only text in this corpus with no printed page behind it, so a wrong proof written fluently reads exactly like a right one and the judges are all there is between it and a reader. L15 asked this of a translation and nothing asked it of a solution, with 39 of the 44 solutions here written on the gateway and the audit silent on all of them. X06, soft, so the corpus does not go red for a solution that may well be right (quality: X06, a solution written on the free gateway #302, reports: X06 in the audit, 39 solutions written on the free gateway bourbaki#172)

Exit: every exercise in the corpus has a solution file with an honest status; eval reports a false-accept rate < 5 % on the benchmark; the scorecard is committed and the README coverage table shows solved %.

---

Every PR against this milestone ticks its boxes here and posts a comment with what was run, on what data, and the numbers.

[tamnd]

Context assembly is in, #84, with the refs fix it needed in #83.

bourbaki solve context builds what a model is shown for one exercise out of the committed Markdown and the reference graph: the exercise, every earlier exercise of its §, the whole of its §, the closure of its cross-references to depth 2 capped at 40 000 characters, and the citations that leave the corpus written out verbatim with the instruction to name the standard result rather than quote a statement it has not been shown. Nothing in it calls a model.

Run over both printings of chapter VIII. English, 317 exercises: median context 44.8k chars, mean 49.2k, p90 83.1k, largest 131.0k at alg-viii-s16-ex-17, smallest 8337; 306 in-corpus references carried, 169 leaving the corpus, 44 named as page citations that narrowed only to a §. French, 316 exercises: median 44.5k, mean 49.6k, p90 84.6k, largest 130.5k, smallest 8419; 0 carried, 73 leaving, 101 §-only.

Two things came out of running it that change what comes next.

No exercise in either printing reaches the 40 000 character cap on references, and none comes near it. The bulk of a context is the § plus the earlier siblings, so the number spec 07 §3.1 fixed is not the number that binds. What binds is the § itself: a context is 45k characters at the median and 131k at the top, and that is the token bill for every candidate, every judge call and every correction round, before anything is generated. Whether the whole § is the right thing to carry is the question worth asking before the pilot, not the cap.

The French carries no in-corpus references at all. That is not the assembler. Building the French graph needed the fix in #83 first, and once it built, 1020 of its 1555 edges resolve to a whole § and none to a statement, because the citation grammar reads English kind words and p. 21, prop. 4 therefore gives up its kind. 686 French citations name a kind the parser does not read: 246 prop., 135 cor., 116 th., 102 exerc., 38 remarque, 35 déf., 14 lemme. A French grammar is its own piece of work. Until it exists, a French context is the exercise, its siblings and its § and nothing else, which is worth knowing before anyone reads a French solution and wonders what the model was working from.

Also worth recording against this milestone: the audit only ever builds the reference graph over the English, which is why -lang fr was broken from the day the French was assembled and nothing said so. Building the French graph in CI is a separate question, since refs build -lang fr writes over the English manifests as things stand.

Next on this milestone is the port of taocp-solver's solver, prompt, result, textguard and pricing, which is the other box that does not need the fleet. Everything model-dependent stays parked while the fleet answers on gpt-5-6-mini.

[tamnd]

The outcome taxonomy and the solution file are in, #85, with the report update on the corpus side, tamnd/bourbaki#51.

Six statuses instead of three. blocked is the corpus's fault, open is nobody's, unverified is the model's, and folding those three into failed was what would have let a scorecard round them all up as tried and flunked. partial carries a part table, each part with its own status and, where it did not pass, the sentence saying what the judge did not believe about it. The front matter also carries uses, the tags the solution leaned on, which is what X03 has been reporting it could not run for want of. That rule is now written.

solve.Store reads and writes the files and refuses to write one that would be a lie on disk. The audit reports the same faults and the store refuses them, which is deliberate: the audit runs over what was committed, and a run that writes eight hundred files and then hears from the audit that all of them are malformed has spent the fleet for nothing.

Two faults fixed on the way. SolutionPath filed an appendix's solutions under sN, so the solution to Exercise 3 of Appendix 1 of chapter VIII would have been written over the solution to Exercise 3 of its § 1, with nothing left to say which one the survivor answered. And the standing note under a published solution said "it did not pass that judgement" for every status that was not verified, which under the new taxonomy would have reported an open question as marked wrong.

audit is unchanged at 51 rules, 7 could not run, 0 hard findings, 190 soft. publish -check unchanged at 1802 pages.

Left on this milestone that does not need the fleet: the prompts, the engine that runs the seven calls, and report solutions. Everything that calls a model stays parked while the fleet answers on gpt-5-6-mini.

[tamnd]

#86 lands the six prompts of spec 07 §2 and the reader for the decisions they ask back. No box is ticked by it, because every box on this milestone except the two already ticked describes a call rather than a prompt, and nothing here calls a model. What it does is fix the contract those calls will run under.

The six are solve_reference.md, solve_candidate.md, solve_select.md, solve_truth.md, solve_audit.md and solve_correct.md. The pipeline's shape is in them more than in the code that will run them: the reference is worked out without seeing any answer, the three candidates are written without seeing each other, the selector gets the obligations and not the reference's own derivation, and the audit judge never sees the reference at all. Each of those is a sentence in a file, and each one is there because the alternative collapses two independent readings into one.

textguard.Read is the only thing that reads a decision. It tolerates a model that bolds its verdict, bullets it, quotes it, heads it or ends it with a full stop, and refuses one that mentions a verdict inside a sentence. It tells a missing field from a negative one, which matters because those want different handling: read as a no, a formatting slip fails a correct solution, and read as a yes, silence passes anything. The truth judge is held to seven lines and a score of 6 or 7 out of 7 with the seven points named one by one; the audit judge is held to two lines, and there is a test that the audit block does not clear the truth judge's bar, which is what keeps them from becoming one judge asked twice.

The prompts and the parser are tested against each other rather than separately. prompt/solve_test.go pulls the example decision lines out of each built prompt and feeds them to the parser: the truth prompt's own example has to pass Passed(), the audit prompt's own has to pass Audited(), the selector's has to read as candidate 1, the reference's as PROOF and IN_CORPUS. Then a closure test requires every key any prompt asks for to be a key the parser knows. A prompt that starts asking for something nothing reads fails here instead of producing three hundred unparseable judgements.

Per-part judging is in. A judge asked for one verdict on a five part exercise gives the verdict the worst part deserves, and the corpus then prints nothing where four parts were right, so the judges are asked for PART b: FAIL, <reason> lines and the partial status is filled from them. Finding the parser dropped part lines was worth the test on its own: the decoration class held \s, so it ran past the end of the line and a four part answer read as two parts with each other's lines hanging off them.

Run against the real corpus rather than a fixture. Chapter VIII exercise 3 of § 1 builds a 32.6k character context and a 36.6k character reference prompt over it; exercise 11 of § 2 builds 42.7k and 46.7k. The selector is handed the exercise alone, since it checks coverage of a list and the whole context would be forty thousand characters it does not read, paid on every exercise. SolveSHA256 is one hash over all six prompts and the three angles, since a solution is the product of all six calls and is stale when any of them moved.

Left on this milestone that does not need the fleet: the engine that runs the six calls with its retry and its correction budget, the solution writer that turns a run into a file, and report solutions. Everything that calls a model stays parked while the fleet answers on gpt-5-6-mini.

[tamnd]

PR #87 landed the engine, which is the six boxes from the reference call down to the multi-part decomposition.

The pipeline is seven calls at most and one at least. The reference call goes first because it is the only call that has read the exercise and has not read an answer, and both blocked and open are read off it and stop the run there. An exercise that turns on a numbered result of a volume this corpus does not hold does not need three candidates written for it. After that it is three candidates, one to each angle, the selector over whatever survived the leak guard, then the truth judge and the reference-blind audit judge, and a correction loop bounded at two rounds that is sent only the judgement or judgements that failed, whole and unsummarised.

Both judges have to pass and they are not averaged. One reads the solution beside the worked reference, the other reads it with the reference taken away and tries to break it, and a solution that passes one and fails the other is either persuasive about a step it did not take or right in a way that cannot be seen from what is written.

Everything that touches a fleet is behind one interface method, so the whole thing runs end to end in a test against answers written by hand. That is the point rather than a convenience: the judging is the part that has to be right, and a harness that can only be exercised by spending a fleet is one nobody exercises.

The part detection is the box worth reporting numbers on, because it is what makes the partial status mean anything and because it was wrong twice before it was measured. A part marker is one the book set: it opens the exercise, opens a line, or follows a sentence that has ended. The back-references that fill the chapter all follow a word or a comma, "use a) to calculate", "deduce from c) that L is normal", "apply Exercise 23, d) of I, §6, p. 145", and reading them as markers gave forty of chapter VIII's exercises exactly five parts, a) through e), which is not a thing a book does forty times. It also hid the long exercises, because a false marker taken in place of a real one ends the letter walk early. The rule also has to allow "f )", which the printing sets as often as "f)", and the star this corpus writes as $*$ in front of a starred part.

Measured over the 317 English exercises of chapter VIII: 112 with no parts, 68 with two, 59 with three, 36 with four, 15 with five, 16 with six, 8 with seven, 3 with eight. No exercise stops its letters before a marker that appears further on in it. The same run over the 316 French exercises gives 112, 66, 60, 36, 15, 16, 8 and 3, which is two independent extractions of the same book counting the same parts.

Left on this milestone: the rest of the taocp-solver port, the solve and review and report solutions commands, the benchmark and eval, the pilot and the long run. Everything from the commands down spends a model, and no run starts while the fleet answers on gpt-5-6-mini.

[tamnd]

PR #88 landed bourbaki solve run and bourbaki report solutions. review is the box still open on that line.

The run plans the exercises, builds each context, runs the seven calls of the engine and writes one file through the store, which refuses a file that would be a lie on disk before the fleet is spent rather than after. One exercise to a lane and one host to a lane: the seven calls of an exercise are one line of reasoning billed to one account, and spreading them over three hosts to save minutes buys a run whose failures cannot be read.

Every question and every answer goes under work/solve/, which is not committed, and that includes the six calls an exercise throws away. A run log goes beside them with the call table and the whole reference reading, which is what a person reads when a judge said no and the reason is not obvious.

What was run, with no model called. -dry-run builds every context and asks nothing, which is the half of a run that can fail without a fleet. Over the English printing that is 317 exercises, mean context 49.2k characters, largest 131.0k, 15.6M in all, at most 2219 calls and as few as 317 if every one stops at the reference. Over the French, 316 exercises, mean 49.6k, largest 130.5k, 15.7M, at most 2212. The pilot set on the next box, chapter VIII § 1 exercises 1 to 9, comes to 296.0k characters, mean 32.9k, largest 34.9k, carrying 0, 2, 3, 2, 0, 5, 4, 0 and 0 parts.

report solutions on the corpus as it stands says 317 exercises, 317 unattempted, 0 answered, 0 believed. That is the number it has to print today, and it is why an exercise with no file is counted rather than left out: a scorecard over what was run says a hundred per cent verified on the first exercise anybody solves.

The dry run found two ordering faults worth naming. The exercises come out of the corpus in label order, so a pilot asked for the first nine of § 1 got 1, 10, 11, 12, 13, 14, 15, 2 and 3. And -section 1 matched the first appendix as well as § 1, which are different sections with the same number, so a run asking for § 1 would have reported on 43 exercises of the wrong one.

Nothing has called a model. The fleet answers on gpt-5-6-mini and no run starts until that is fixed.

[tamnd]

solve review is in, PR #89, and the commands line is ticked.

It is the judging half of the pipeline with the writing half taken out: the candidate-blind reference, the truth judge, the reference-blind audit judge, three calls to a solution rather than seven. Nothing is corrected and nothing is rewritten. The question it answers is whether what is committed stands, which is not the question a fresh run answers.

The single judging round came out of the correction loop as judgeOnce and the loop still calls it, so there is one implementation of what two judges add up to. Two would have drifted, and the one that drifted would have been the one the benchmark runs on.

Without -write it is a report: what the file says, what the judges say now, and the reason from whichever judge failed. With -write the front matter is brought up to what the judges said and the body is untouched, with the date in reviewed: rather than generated:. Both judgements go to work/review/<lang>/<label>/review.md whole, because the table says a verdict changed and that file is the only place that says why.

What is left on this milestone is the benchmark and eval, and the pilot, which is running now on server2 and server3.

[tamnd]

#91 is merged. The pilot was losing calls to a limit nobody had measured, so the limit was measured and every question now fits inside it.

The ceiling is not documented anywhere, so it was found on the live fleet with real material. Truth judge questions of 36 569 and 38 033 characters of Bourbaki were answered, one of 40 033 came back as the service's own error page, and one of 42 277 did so every time it was sent, on two hosts, over an hour. Filler prose of 59 456 characters was answered in about a minute, so the cap is not on characters: prose runs about 4.3 characters to the token and this material runs about 2.2 to 2.5, which puts every one of those observations on the right side of a limit near sixteen thousand tokens. bourbaki fleet ask is the command that did the measuring, one question to one host with -fill to pad it out, and it is also the only honest check that a host will answer at all, since fleet probe -deep speaks a different transport from the one the work goes over.

The shape of the problem that leaves is not a tail. Of the 317 exercises of this printing the median context is 44 780 characters, the largest is 130 961, and 250 of the 317 are over 32 000 before any instructions are added. Averaged over the printing the § is 40.1k characters of a 49.2k context, siblings 7.0k, references 1.1k and the exercise 0.9k, so dropping references and siblings alone could never have fitted anything and the cap has to be able to touch the §.

What goes is what nothing points at, before what something does, and the kind of the piece does not come into it. Everything droppable is ranked by how strongly something points at it: 0 for what nothing points at, 1 for what is reached through something else, 2 for what the exercise cites itself, 3 for what the work in front of the judge names. Least kept first, then least often pointed at, then longest first, re-rendering after each drop until it fits. The § is cut by the statement and not by the character, so a dropped proposition leaves its name where it stood rather than the § ending mid-proof. Whole pieces that go move into the block that already says what is in the corpus and is not in front of you, and the exercise itself is never dropped.

Exercise 17 of § 16 is the case that taught the rule. It is the largest context of the printing, sixteen earlier exercises and a § of forty statements, 130 961 characters, and its second line says "use Exercise 14". Trimmed it comes to 25 713: the exercise, Exercise 14, the § with 63 statements lifted out and each named where it stood, and the one reference it cites into another §. An earlier version of the ranking kept Exercise 1 and dropped Exercise 14, because both are cited at depth 1 and Exercise 14 is twenty characters longer, which is why the reach of a citation now carries how many times it was made and not only how far out it reached.

All 317 contexts fit after trimming, the largest at 28 000 characters. solve context reports it:

317 exercises
context  median 44.8k chars, mean 49.2k chars, largest 131.0k chars (alg-viii-s16-ex-17)
over ask 250 of 317 contexts are over 32.0k chars on their own, before the instructions
trimmed  median 27.3k chars, largest 28.0k chars, 0 still over the 28.0k chars a question leaves them

#92 makes solve run -dry-run print the same number, since it was printing the assembled size and a person reading 34.9k against a 32 000 cap cannot tell whether that means trimmed or refused.

One thing worth writing down before the pilot results arrive. Every host is answering on gpt-5-6-mini and has been for the last 26 jobs. chatgpt-tool accounts says the same thing from the other side: 31 slots, 11 verified, and every one of them a free account. Nobody picks the model here, the ask goes to a browser profile and whatever the account is being served comes back, so the pilot solutions will be written by a cut down model and quality.SmallModel will say so on every one of them. That is a fact about the fleet and not about the pipeline, and it is worth knowing before anyone reads the nine solutions and forms a view about how well the pipeline works.

The pilot is running now: § 1 exercises 1 to 9 over server2 and server3, nine contexts of 25.5k to 27.8k characters sent, up to 63 calls.

[tamnd]

The pilot is done and read

Nine exercises of Algebra VIII § 1 were put through the pipeline and every solution that came back has been read by hand against the exercise and against the §. The corpus side is tamnd/bourbaki#52, merged, and the box above is ticked.

What came back

Five of the nine returned. Four did not, and they did not fail on the mathematics: server3 filled its disk part way through the run and both mkdir and rsync came back No space left on device. Exercises 3, 7, 8 and 9 are worth running again once there is room, and nothing about them is known yet.

verified	3 (exercises 2, 4, 5)
partial	1 (exercise 6)
unverified	1 (exercise 1)
lost to the host	4 (exercises 3, 7, 8, 9)

Most calls landed on gpt-5-6-mini. None of the four pilot guards was in force for this run: they were written out of it and are #94, #95, #97, #98 and #99.

What the reading found

Two of the five ended with USES: 00QM, 00QN. Those tags are Theorem 1 and Corollary 2 of Appendix 3, which is Hilbert's Nullstellensatz, and neither exercise touches it. It was the sample line of the prompt, copied out of the instructions by a model with nothing better to write there, and three of the five answers to exercise 1 came back with exactly that line. Fixed in #98: the prompt prints XXXX and YYYY now and tags reserves both so no result can ever hold them.

Exercise 2's solution wrote its twenty displays as \[ ... \] where the four written beside it on the same prompt used $$ and where \[ occurs in no file of content/en. Fixed in #98 by normalising rather than by spending a call to say so.

Exercise 6 part d) is a false reject, and the interesting one. The proof is sound and argues from Definition 1 and Definition 2 of the §, and the judge failed it for relying on numbered definitions that were not in the section it was shown. That was true of the question and false of the solution: the trimming dropped both definitions because it ranked reachability by tag and by label while the prompt tells the model to cite the way the book does, by name and number. Fixed in #99 and checked on this exercise: both definitions now survive with 14,746 characters of room to spare.

Exercise 4 part b) is the one worth dwelling on. It rests on exercise 3 a) as the English prints it, and the English prints it wrong. It asks for K finite-dimensional over K' where the French of 1981 at A VIII.13 asks for infinite, and the right ideals of the ring in question are exactly the K'-subspaces of K, so the conclusion the exercise asks for holds in the infinite case and fails in the finite one. pdftotext on the Springer 2023 page confirms the English really says it, so the transcription is faithful and the book is what is wrong. The solver read it, wrote a solution on top of it, and both judges passed it, which is a verified solution whose second half rests on a hypothesis making its own conclusion false. Two judges will not catch a wrong premise they were handed as fact. The mechanism that came out of it is in #99 and #101: the correction lives in manifests/errata.yaml, the assembler stamps it into the exercise front matter, and the model is shown the printed words and the correction together.

Exercise 1's verdict of unverified is right. Its converse builds an injective hull and appeals to Baer's criterion, neither of which is anywhere in chapter VIII. It also gives the wrong address for a fact it uses, Example 3 of § 2 for what is Example 3 of § 1, no. 2.

Exercise 5 is right throughout and had left one of the results it cites off its tag line.

What the reading cost, and what it is worth

Four findings out of five solutions, three of them fixed in code and one of them a fault in the book. The verdicts themselves were mostly right: three of five statuses stand as the pipeline set them, one was a false reject, and one was a pass that should not have been. That is not a rate to conclude anything from at n=5, and it is the reason the twenty-exercise benchmark below exists.

A solution now records the reading on its face. hand_read and found went in with #100, and neither moves status: the status is what the pipeline decided, the corpus says so plainly, and a reader who disagrees writes down why rather than editing the verdict away. Exercise 6 part d) sits in the corpus as unverified with a found line saying the verdict is wrong and why, which is two facts, and neither of them should be allowed to swallow the other.

Next

• rerun exercises 3, 7, 8 and 9, and rerun 4 b) against the corrected exercise, once server3 has headroom
• the twenty-exercise benchmark, built out of these five hand readings plus deliberately flawed variants, then solve eval -write