lean4-explainer showcase

What lean4-explainer produces for the Lean projects below. Hosted annotations, when present, carry their provenance and source grounding beside the explanation. To write your own explanations, start with the Lean4 Domain Explanation Language (L4DEL) guide or the README.

This release includes Lean-backed trust results produced locally. A cached result is reused only for matching source, declarations, Lean toolchain, probe, and dependency pins. Each corpus's Trust page identifies checked declarations and every file that remained UNKNOWN. The corpus-card sorry count is still a separate textual source scan.

Annotation grounding audit (JSON): generated wording is checked against pinned source text; curated wording remains source-linked and unreviewed.

All corpora

1. Formal Conjectures (conjectures)
   Open and solved conjectures stated in Lean, one statement per problem.
   1725 files, 9845 declarations, 3790 contain sorry. commit 1646ca16afd6, toolchain leanprover/lean4:v4.33.1, mathlib 0df444a360ea. Source: google-deepmind/formal-conjectures at the pinned commit. License: Apache-2.0 (text).
   Software is Apache-2.0. Other material is CC-BY 4.0. Content taken from Wikipedia, MathOverflow and the OEIS is CC-BY-SA 4.0 (ShareAlike); material from bbchallenge.org is CC-BY 4.0; the source URL in each file names its origin. Doc comments and statements shown here are copies of that content.
   Selected declarations are explained with L4DEL from a hosted sidecar overlay; the upstream authors did not write these explanations and their sources are unchanged. Each explanation links back to its exact pinned Lean source. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.
   Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
   Primary project and mathematical sources: Pinned project documentation, Formal Conjectures paper, arXiv v1.
2. AlphaProof Nexus results (research results)
   Published Lean proof artifacts for AlphaProof Nexus across Erdős problems, OEIS, the Stacks Project, and mathematical collaborations.
   71 files, 3334 declarations, 72 contain sorry. commit 0647711a7118, toolchain leanprover/lean4:v4.27.0, mathlib a3a10db0e9d6. Source: google-deepmind/alphaproof-nexus-results at the pinned commit. License: Apache-2.0 (text).
   The pinned README licenses software under Apache-2.0 and other materials under CC-BY 4.0, with additional third-party-source notices for OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn.
   Selected declarations are explained with L4DEL from a hosted sidecar overlay; the upstream authors did not write these explanations and their sources are unchanged. Each explanation links back to its exact pinned Lean source. This overlay contains 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.
   Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.
   Primary project and mathematical sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions.
3. Carleson's theorem (formalization)
   The formalization of Carleson's theorem on the convergence of Fourier series.
   120 files, 3082 declarations, 6 contain sorry. commit 8972acdfd953, toolchain leanprover/lean4:v4.34.0-rc2, mathlib b63493a4746b. Source: fpvandoorn/carleson at the pinned commit. License: Apache-2.0 (text).
   Selected declarations are explained with L4DEL from a hosted sidecar overlay; the upstream authors did not write these explanations and their sources are unchanged. Each explanation links back to its exact pinned Lean source. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.
   Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
   Primary project and mathematical sources: Pinned project documentation, Pinned Carleson blueprint.
4. Fermat's Last Theorem (FLT) (formalization)
   The Imperial College project to formalize a proof of Fermat's Last Theorem.
   265 files, 3684 declarations, 50 contain sorry. commit f6c6a2fe9796, toolchain leanprover/lean4:v4.35.0-rc3, mathlib c0da404748dc. Source: ImperialCollegeLondon/FLT at the pinned commit. License: Apache-2.0 (text).
   Selected declarations are explained with L4DEL from a hosted sidecar overlay; the upstream authors did not write these explanations and their sources are unchanged. Each explanation links back to its exact pinned Lean source. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.
   Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
   Primary project and mathematical sources: Pinned project documentation, Pinned FLT blueprint introduction.
5. Polynomial Freiman-Ruzsa (PFR) (formalization)
   The formalization of the polynomial Freiman-Ruzsa conjecture over characteristic 2.
   76 files, 1083 declarations, 6 contain sorry. commit ce7ac95e620a, toolchain leanprover/lean4:v4.35.0-rc4, mathlib 1f414401f690. Source: teorth/pfr at the pinned commit. License: Apache-2.0 (text).
   Selected declarations are explained with L4DEL from a hosted sidecar overlay; the upstream authors did not write these explanations and their sources are unchanged. Each explanation links back to its exact pinned Lean source. This overlay contains 9 curated AI-written annotations and 485 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.
   Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
   Primary project and mathematical sources: Pinned project documentation, Polynomial Freiman-Ruzsa proof paper, arXiv v2.
6. Compfiles (competition)
   Formalized statements and solutions of olympiad-style problems.
   545 files, 8794 declarations, 5 contain sorry. commit 47b19bbfe5f3, toolchain leanprover/lean4:v4.34.0, mathlib 5ed296525643. Source: dwrensha/compfiles at the pinned commit. License: Apache-2.0 (text).
   Selected declarations are explained with L4DEL from a hosted sidecar overlay; the upstream authors did not write these explanations and their sources are unchanged. Each explanation links back to its exact pinned Lean source. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.
   Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
   Primary project and mathematical sources: Pinned compfiles documentation, Pinned compfiles corpus index.
7. Mathematics in Lean (tutorial)
   The tutorial that teaches Lean 4 and mathlib through mathematics. Exercises and solutions share names.
   88 files, 1646 declarations, 246 contain sorry. commit dd6d752fedb1, toolchain leanprover/lean4:v4.30.0, mathlib c5ea00351c28. Source: leanprover-community/mathematics_in_lean at the pinned commit. License: Apache-2.0 (text).
   Selected declarations are explained with L4DEL from a hosted sidecar overlay; the upstream authors did not write these explanations and their sources are unchanged. Each explanation links back to its exact pinned Lean source. This overlay contains 9 curated AI-written annotations and 7 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.
   Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
   Primary project and mathematical sources: Pinned Mathematics in Lean documentation, Pinned Mathematics in Lean textbook.
8. Theorem Proving in Lean 4 (tutorial)
   The book on Lean 4 itself: dependent types, tactics, inductive types.
   35 files, 1258 declarations, 64 contain sorry. commit 4e28129fdd58. Source: leanprover/theorem_proving_in_lean4 at the pinned commit. License: Apache-2.0 (text).
   Selected declarations are explained with L4DEL from a hosted sidecar overlay; the upstream authors did not write these explanations and their sources are unchanged. Each explanation links back to its exact pinned Lean source. This overlay contains 8 curated AI-written annotations and 26 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.
   Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
   Primary project and mathematical sources: Pinned Theorem Proving in Lean documentation, Pinned Theorem Proving in Lean 4 book index.
9. openai/math (oai)
   Lean formalizations that accompany the openai/math manuscripts.
   122875 files, 3572375 declarations, 539 contain sorry. commit fd4aeeb2ee4f. Source: openai/math at the pinned commit. License: Apache-2.0 (text).
   Selected declarations are explained with L4DEL from a hosted sidecar overlay; the upstream authors did not write these explanations and their sources are unchanged. Each explanation links back to its exact pinned Lean source. This overlay contains 120 curated AI-written annotations and 1273 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 9 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. Those 9 annotations were revised on 2026-10-14 to bind all of them to exact page-one quotations from 6 pinned OpenAI manuscripts, the matching pinned formalization notes, and named historical primary sources; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. The 3 manuscript-grounded matrix-multiplication annotations were composed from pinned OpenAI manuscripts and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Six additional target-specific annotations for Catalan's constant, the irrationality exponent of pi, dyadic Erdos similarity, Unique Games, quintic Lienard systems, and Yau nodal growth were composed from pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for Seymour's second-neighborhood conjecture, Cannon's conjecture, Koebe circle-domain uniformization, and circle-domain rigidity were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for simple Lebesgue spectrum on the three-torus, Rokhlin multiple mixing, the nine-dimensional Borsuk counterexample, and Tingley's sphere-isometry problem were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the Abhyankar-Sathaye counterexample, the circulant Hadamard conjecture, the Eilenberg-Ganea counterexample, and short Egyptian fractions were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and quotations from Sathaye, Turyn with Storer, Eilenberg with Ganea, and Erdos in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the complete Crouzeix inequality, unrestricted Euclidean five-coloring, the general Mahler conjecture, and Thompson F nonamenability were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, the matching formalization notes, and linked historical sources by Crouzeix, de Grey, Mahler, Cannon, Floyd, and Parry; no human review is claimed. Four additional target-specific annotations for algorithmic strong thin trees, Barnette's Hamiltonian-cycle conjecture, the explicit Artin CAT(0) counterexample, and generalized amplitude-damping capacity were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, matching formalization notes, and linked historical sources by Anari with Goddyn, Arts with Hopman and Timmermans, Charney, and Khatri with Sharma and Wilde; no human review is claimed. Fourteen solution-level annotations for Seymour's second-neighborhood theorem were added on 2026-10-14 from the pinned 15-page manuscript, covering the exact-neighborhood model, minimal-counterexample reduction, subset deficit, transitive blowup, pruning, extremal contradiction, and proof-bearing final theorem. The subset and blowup annotations also bind exact quotations from Tyler Seacrest (2019) and Brantner, Brockman, Kay, and Snively (2009); no human review is claimed. Thirty-seven declaration-level annotations were added on 2026-10-14 for the rest of ComparatorChallenges/AlgorithmicThinTrees.lean, covering its multigraph semantics, stack-machine cost model, explicit and binary-multiplicity encodings, output certificate, and complete algorithmic proposition. They are bound to the pinned OpenAI manuscript and linked earlier thin-tree sources by Luis Goddyn, Nima Anari, and Shayan Oveis Gharan; the annotation explicitly preserves that the concluding comparator theorem still has body by sorry, and no human review is claimed. Thirty-one supporting declarations in ComparatorChallenges/UniqueGamesTheorem.lean were upgraded or added on 2026-10-14, completing curated coverage of all thirty-two declarations in that file. The annotations cover the finite game model, Boolean formula and parser, binary-vector translations, explicit output serialization, finite-alphabet machine contract, and gap theorem; they distinguish manuscript-backed mathematics from Lean-specific canonical parsing and unary game output encoding, bind exact OpenAI manuscript quotations, and credit Subhash Khot through his 2010 survey. The comparator theorem remains explicitly labeled as having body by sorry; no human review is claimed. The source-derived generator was hardened on 2026-10-14 so a formalization note covering multiple comparator results no longer copies its combined Scope prose onto each declaration; those targets now use declaration-specific source comments when available and otherwise remain explicitly bounded to the exact Lean statement. The remaining source-derived annotations were generated mechanically from pinned formalization notes and source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.
   Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.
   Primary project and mathematical sources: Pinned openai/math documentation, Pinned formalization catalogue.
   Implication edges: curated claims about what one result could establish about another, each with its contract and how far it is checked; kept in lean4-explainer, not by the upstream authors.