3.0.0

A major version: a new deliverable and a new project layout.

• NEXT.md, the follow-up papers. A private file that answers what paper you could write next, following the one you formalized. It keeps only directions that would make a paper of their own: an answer to a question someone has posed, a new idea where the paper's method stops, a sharpness result, a new setting. It leaves out remarks such as an unused hypothesis or a variant the same proof covers. The best two to four candidates are explored in depth: the target and a fallback, a search for the target itself, the step where the paper's argument fails (followed in a scratch Lean file), attempts past it, computed evidence and partial results. Every claim is marked as proved, checked numerically or conjectured, and a second reader checks each candidate. NEXT.md is ignored by git and never published unless you ask. The report's "What's next" section stays as it was.
• Three libraries. Each layer imports only Mathlib and the layers below it: Basic holds general mathematics, External the results the paper cites from other works, and the paper's library its own results. External is now a library beside Basic instead of a directory inside the paper's library. It states each cited result in its source's own terms, and the paper's library proves the bridge from its objects to the source's, so other formalizations that cite the same source can reuse it. The lakefile template, the audit script, CI and the link script all treat External as one of the roots.

Projects laid out with PaperName/External/ can move it in one cleanup round (references/cleanup.md).

2.5.1

The last version of the 2.x series.

What the 2.x series added to 1.4.0:

• 2.0.0: the report ends with "What's next", built from a dated search for later work, later versions and errata. Later work that corrects the paper becomes one of the audit's findings. The documents are reworded in plain language, and CREDITS.md records how each formalization was made, round by round.
• 2.1: simpler proofs found during the work are recorded in "What's next". Also a pitfall: hypotheses that section variables silently drop from statements.
• 2.2: the paper's place in the literature (before it, concurrent with it, since it, and other formalizations) gets its own section of the report.
• 2.3: the route check extracts, from the TeX source, the results each of the paper's proofs cites, following where papers put their proofs.
• 2.4–2.5: general mathematics lives in Basic, a library of its own beside the paper's, filed by field under Mathlib's names, so it can be contributed later.

1.4.0

The last version of the 1.x series: the skill as it first settled, before the report gained its sections on what comes next.

What the 1.x series built up:

• The workflow from the paper to a Lean project with no sorry and no axiom: inventory, statements first, the paper's own results (Stage 1), then the results it cites (Stage 2), verification, cleanup, the audit report and packaging.
• Palomar packaging by default (Challenge/Solution, Comparator, formalization.yaml), and a run log of how the formalization was made.
• Cited results out of reach become named hypotheses, so a formalization that depends on them says plainly that it is conditional. Libraries beyond Mathlib are allowed, and the Challenge's scope is defined.
• 1.4.0: every proof follows the paper's argument. A proof departs from it only when it must, and every departure is reported with its reason.