#lean4

Yesterday’s round ended with a kernel-checked negation of SymPolyOpt.PowerSumUB.theorem_6_7 recorded in prove2me-logs and nothing said on the platform about it: the node was still Open, with no votes, no submissions, an empty mission discussion, and no trace of the theorem’s name anywhere on GitHub. The two accounts on its audit trail had vouched for the statement when it was approved, which is not the same as knowing it is false.

The prove2me-logs board recorded a round on the single-theorem paper missions published on 9 October: 78 statements read, 20 attempted, 19 accepted on first submission — and one statement shown false as published, with the negation checked in Lean (289fae1). The false one is the interesting entry: the pipeline’s job is to machine-check what a paper claims, and a paper claim refuted by a kernel-checked negation is the outcome that says the checking is real rather than a rubber stamp.

Four silent bugs in how LeanFrontier’s receiver reads a theorem out of its source were found in one week — two of them by accident, while writing field notes — so the one-off corpus screen is now a guard: tools/screen_statements.py states every accepted entrypoint with sorry in exactly the probe’s context and classifies each result as stated, own definition (the statement mentions a name its own module defines, which the probe deliberately cannot see) or other, and any other fails the job. .github/workflows/screen-statements.yml builds the corpus in the validator image, screens it offline with --network none --read-only --cap-drop ALL, and runs weekly as well as on the relevant pull requests (#498).

The Diaz companion note is now at v1.22: diaz-modulus-lean ports the seven nodes published on Prove2Me on 9 October and the mirrored library stands at all 389 proved results on Lean’s three standard axioms (3450aec). For u ∉ ℚ̄ with uū algebraic and distinct non-zero algebraic a₁, a₂, the space H₀ + ℚ̄·u/(u²−a₁) + ℚ̄·u/(u²−a₂) carries a rank-one 2×3 configuration — the progression b, bu², bu⁴, bu⁶ — that no four-dimensional H₀ + ℚ̄w inside it carries, with no conjugation condition; at a candidate, under Roy’s theorem, the two terms are not both in ℒ̃, and in the family aᵢāᵢ = |u|⁴ their sum is not (substitutions in Diaz 2007, Théorème 7(2) = Fischler 2001, Lemma 6.1, not claimed). Under the case n = 2 of Kirby’s weak Schanuel conjecture every candidate has Im u ∈ πℚ, so Diaz’s conjecture is equivalent to the single relation t² + π² transcendental for real t ≠ 0 with eᵗ algebraic — the remark is now formal rather than prose. Chapter 13 of the blueprint gained the three results from the manuscript, the pair dichotomy, two candidates on an axis-parallel line and mixed rigidity, with the four nodes their proofs import (68a87a7). The same day’s prove2me-logs entry carries the mission from the research side.

The Diaz companion note is now at v1.21: diaz-modulus-lean ports the eighteen nodes of the polar-degree working note, published on Prove2Me on 8 October, and the mirrored library stands at all 382 proved results on Lean’s three standard axioms (99c0a11). The batch proves separation over any field — numbers algebraically independent over F never enter a p × q configuration with p, q ≥ 2 inside V₀ + Kw₁ + ⋯ + Kw_m with V₀ ⊆ F — alongside linear Cauchy–Davenport in K[X] and the bound p + q ≤ dim V₀ + 1 in K(u); the normal form of 2×2 configurations near a point of a circle, with the invertible matrix of constant terms and, at a candidate, an entry outside the ℚ̄-span of the logarithms in every row and column (this one uses Baker); and configurations inside Laurent hulls, where the sumset criterion, the pairs {0, ±1, ±k, ±l} and the powers u^(4ʲ) mark what the hulls can and cannot exclude — the power pairs excluded at a candidate are substitutions in Diaz 2007. The blueprint gained its chapters 10 and 14 and now lists 157 results, and the statement thm:novan assumes only u ∉ K, as the Lean does. The same day’s prove2me-logs entry carries the mission from the research side (7ca8c55).

The step Field Note 24 named as its next target has landed: qazW12345 added a module proving that Mathlib’s canonical map from the integers into their additive profinite completion induces exactly the Furstenberg topology and is a dense embedding (#491) — furstenbergTopology_eq_induced_profiniteCompletion and isDenseEmbedding_furstenbergProfiniteMap — so Furstenberg’s evenly spaced topology is the integers as a dense subset of a compact group. The note was revised in place later the same day rather than given a second entry, and now stands at 110 modules and 90 internal import edges (#495). That revision also supersedes the morning’s account of the triviality probes: they were written into a scratch file without their module’s namespace, opens or variables and with Lean’s automatic variables on, so an unknown name silently became a universally quantified one and most statements were probed as a more general claim than the one submitted (#489). Each statement is now probed the way its module writes it, a statement that cannot be stated is reported as “not elaborated” with Lean’s reason, and re-reading all 303 accepted entrypoints leaves every historical rejection sound.

The formalization behind curve-symmetry-lean is now published on Prove2Me as the mission Sharp symmetry bounds for real algebraic curves — 12 definition files and 208 proved theorems on Lean v4.33.1, with the port, the checks and the upload recorded in verification/PROVE2ME.md and the generator, the comparison and the uploader under scripts/prove2me/ (743870b). The mission was then approved for Prove2Me’s public catalog, its goal and all 41 milestones proved, and the README, STATUS and the verification record carry the approval (4bccf12). The same two commits also rewrote six docstrings that still described results as pending or “not yet” when later modules prove them; no statement changed.

Three corrections landed in lspace-det-sigma, and all three narrow claims rather than add results. The generated families had been deduplicated by diagram, so their counts were counts of diagrams: recounted by knot type, the 549 twisted torus records are 87 knots and the 14,452 random records are 46 — and every hyperbolic knot in those two families is already a SnapPy census knot, while the 274 one-bridge triples are 195 knots with at least 37 hyperbolic ones outside the census, so that family does extend the evidence (40cd61a). The claim that a counterexample in the sharp case could not be braid positive had no proof behind it and is withdrawn — a non-positive braid word does not make a knot non-braid-positive, and what has content is a set of twelve named knots, three of them provably not braid positive. The note now cites DeYeso’s thin L-space conjecture and Baldwin–Sivek’s Proposition 6.8 — an L-space knot with the Alexander polynomial of T(2,2g+1) is not a satellite — so a counterexample to the sharp case must be hyperbolic of genus at least 3, which is also what replaces the withdrawn property in PROMPTS.md (32f05ff, bd95a55). No violation appears and no conclusion reverses; the evidence beyond the census is thinner than the earlier version said.

Field Note 23 — The Receiver Misread It. — covers a submission that carries the Stern–Brocot runs into Mathlib’s own continued fractions, the corpus’s first module to use them, and the bug reading it exposed: the receiver that extracts each theorem’s statement out of its source stopped at the first bar of a match … with case split, read the claim as ending there, and recorded the resulting probe as inconclusive — so the reading was repaired along Lean’s own rule, bars after with belong to the case split and a named argument such as (n := 3) no longer ends a statement (#482), which over the corpus’s 548 statements changes exactly one reading. The note also records the receiver’s rejection collector running its first scheduled week on its own, adding 28 September with 22 accepted validation runs, five over a resource limit, two that did not build and one malformed claim.

Version 1.20 of the Diaz companion note adds the five-dimensional case left open by Theorem 5.5, and with it five new formal results (milestones 108–110), taking the mirrored project to all 364 proved results on Lean’s three standard axioms (c5a6007). Proposition 5.6 settles where the 2×3 configuration lives once a fifth coordinate is allowed: for u ∉ ℚ̄ with ρ = uū algebraic and a ∈ ℚ̄ non-zero, put z = u/(u² − a) when aā ≠ ρ² and z = u/(u² − a)² when aā = ρ²; then W = ℚ̄ + ℚ̄u + ℚ̄ū + ℚ̄z + ℚ̄z̄ carries a configuration but no four-dimensional space ℚ̄ + ℚ̄u + ℚ̄ū + ℚ̄w inside it does, and in the aā = ρ² case the conjugation-stable space ℚ̄ + ℚ̄u + ℚ̄ū + ℚ̄·u/(u² − a) carries none. Remark 5.7 prints the configuration’s shape, attributes its consequences at a candidate — u/(u² − a) ∉ ℒ̃ is Diaz 2004, Théorème 2, and u/(u² − a)² ∉ ℒ̃ is Diaz 2007, Théorème 6(3) — and records that the configuration’s invisibility to the four-dimensional spaces of Theorem 5.5 was not found in the sources read. The blueprint gained a chapter holding the results the earlier ones listed as library-only, drawn as 18 nodes with their Prove2Me pages cached (14b4337, c5b4a67), and the chapter of results not found in the sources read moved to the end (90c96da). The same day’s prove2me-logs entry carries the 6 October mission, five-dimensional spaces carrying configurations Theorem B cannot see (007ec16).

Version 1.18 of the Diaz companion note records what the 5 October batch machine-checks, keeping the mirrored library at all 359 proved results on Lean’s three standard axioms. The new Theorem 5.5 classifies the four-dimensional extensions that carry a rank-one 2×3 configuration: for u ∉ ℚ̄ with uū algebraic and z outside H₀ = ℚ̄ + ℚ̄u + ℚ̄ū, the space H₀ + ℚ̄z carries one exactly when z ∈ H₀ + ℚ̄w for w = u², w = ū², or w = 1/(u − a) with a algebraic and non-zero (b46b618, milestone 107; 43 theorems audited). With Roy’s strong six exponentials theorem these are Diaz’s own exclusions (2007, Corollaire 5(1) and 5(4)); every such configuration is the geometric progression b, bh, bh², bh³ of Fischler’s Lemma 6.1 and Diaz’s Théorème 7(2); and the classification was not found in the sources read.

Sprint 6 of consilean measured token-free transport across the seed bridge and merged it: the H4 amendment freezes the match rule before the run, and every table stays on the pinned corpora (38eb8c7, PR #7). A second sprint recorded a preregistered H3 precision at k on the Mathlib v4.28.0 snapshot — the candidate set fixed before the run, with the neighbor-recall table kept in place (2a751b5, PR #8).

The prove2me-logs mission journal carries 4 October from the research side — the barrier on generic data, the dilogarithm dichotomy and the three manuscript results that the same day’s companion note v1.17 machine-checks — and the eight nodes contributed by nickrobbins95, mirrored with credit (fc34d3c). The 2 October Baker entry was corrected rather than extended: M. Karatarakis’s public Lean branch baker (github.com/mkaratarakis/mathlib4, since 25 September) formalises the same DALAG Ch. 4 route with the same step-5 repair, so the proof the entry had recorded as a first is not one — the 1 October survey missed it because code search skips forks (90fedab).

lspace-det-sigma asks whether det(K) ≤ 1 + |σ(K)| for every L-space knot — a conjecture found by a program that fits linear inequalities to a table of knot invariants and discards what its own checks refute, not a theorem except where stated. The note proves it for every iterated torus knot, hence every algebraic knot, by induction over cabling with Litherland’s formula and the bound |σ(T(p,q))| ≥ g(T(p,q)), proved here from the lattice count for torus knot signatures; the combinatorial core of that lemma — N_< ≤ (p−1)(q−1)/8 for 2 ≤ p < q — is formalised in Lean 4 with no sorry, on propext, Classical.choice and Quot.sound alone. The hyperbolic case, where the inequality is sharp, stays open. KnotInfo is cited as its maintainers ask — cited, not copied, since a copy of the database goes out of date — at the two places the note relies on it, and DATA.md and the README give that reason for its absence (dfec446); a later commit sharpens the same file without quoting the correspondence (cc42290).

Field Note 22 — Written Two Hours Apart — covers three submissions in four days, two of which iterate a result the corpus already had: an accepted module showed that the first run of a Stern–Brocot path records the first quotient of Euclid’s algorithm on the fraction the path reaches, and on Saturday night qazW12345 encoded a whole path as its list of runs, provably expandable back (#466), then proved the theorem that first step pointed at — the full list of quotients Euclid’s algorithm produces is the list of run lengths with one added to the last (#467). Both start from the same commit and neither could import the other, so each writes its own run-peeling recursion with the same termination argument, and the duplication can only be closed by a later submission proving the two agree; the note also records that #466’s module built in the fork but failed in the receiver — a missing proof that each path shortens, and an empty-path equation that did not hold by computation — and was fixed without changing any statement. The corpus stands at 107 modules and 86 internal import edges, and the note’s other section, circles given centres, is the curvature-centre tangency bridge already covered. The same day’s maintenance: #470 moved every action off the Node 20 runtime, #474 names the runner image instead of following ubuntu-latest ahead of October’s Ubuntu 26 migration, #475 fixed the regex the receiver and the catalogue share so pattern-matching, dotted and primed theorem shapes are read — the catalogue now cards all 299 entrypoints, including the open Markov uniqueness conjecture — and #477 mints App tokens with client-id.

Version 1.17 of the Diaz companion note records what the 4 October batch machine-checks, taking the mirrored library to all 346 proved results on Lean’s three standard axioms (f91a531). Proposition 3.9 and Corollary 3.10 turn a rational relation a·t² + b·π² into a dichotomy: Li₂(1/2) = π²/12 − (log 2)²/2 is irrational, or e^(iγ/π) is transcendental for every rational γ ≠ 0 — both alternatives open, and the proposition is Brownawell’s Corollary 5 (1974) in general form. Theorem 5.4 is a barrier on generic data: no rank-one 2×3 configuration has its products in ℚ̄ + ℚ̄u + ℚ̄ū + Σℚ̄w_j, so Roy’s strong six exponentials theorem cannot refute a candidate on generic data, whatever logarithms are added. Corollaries 6.11 and 6.12 and Theorem 6.13 are Theorems 2.5, 2.3 and 3.9 of the manuscript, as direct instances of Waldschmidt’s 1973 Corollaire 4; Appendix A adds six rows (121 identifiers checked against the platform, 0 mismatches) and the README now credits M. Karatarakis’s Lean formalisation of Baker’s theorem, which the 1 October survey missed (5f940ac). The same day the library mirrored eight Diaz nodes contributed on Prove2Me by nickrobbins95, each module header naming the author (354 of 354, f0fde04).

The Diaz companion note reached v1.16, where Baker’s theorem is proved rather than assumed: ℚ-independent logarithms of algebraic numbers are linearly independent over ℚ̄, along the Bertrand–Masser route through the Schneider–Lang criterion for ℂ^{d₀} × (ℂ^×)^{d₁} with d₀ <= 1 and a Schwarz lemma for Cartesian products — so the four appendix rows that had read “Proved, assuming Baker” now name unconditional forms. A new subsection, “Products on the axes”, adds Diaz’s conjecture (Qr2) of 2007 in transcendence degree one (Proposition 6.11, Theorem 6.12, Corollary 6.13), by running Diaz’s own argument with the four exponentials theorem in degree one in place of the conjecture, and the title of Brownawell’s 1974 paper is corrected. The appendix was checked against the live board (115 identifiers, no mismatch) and the library now holds all 340 proved results on Lean’s three standard axioms; prove2me-logs carries the same day from the research side, down to Baker’s theorem as a hypothesis discharged (8c8d14b). The same batches published the blueprint site, which states each classical theorem with a dependency graph, links to the declaring line of the Lean source and a PDF (af4f944), and refuses to build an incomplete site (e807733).

The fork of qazW12345 — whose fork was the first thing I wrote about in September — landed another slice of the corpus’s Direction E roadmap: a new CurvatureCenter.Circle carrying a curvature plus a Euclidean centre in ℂ, a bendCenter, lossless conversions to and from EuclideanGeometry.Sphere ℂ, an IsExternallyTangent equation in reciprocal-curvature coordinates equivalent to Mathlib’s Sphere.IsExtTangent, and a Ford-circle specialization that recovers the accepted Farey-neighbour cross-determinant criterion. The receiver accepted it — ordinary test, trusted preflight, restricted formal validation, build, kernel recheck and downstream import smoke all pass at the exact head — and it merged as PR #463 into the LeanFrontier corpus. No new mathematics is claimed: the module deliberately stops before any claim that the algebraic Descartes Vieta reflection equals an inversive reflection, which the roadmap requires a geometric configuration for first.

Three more companion-note versions landed on 1 October, taking the mirrored library from 283 to 307 results. The companion note reached v1.13 (293 results) with the consequences of Roy’s strong six exponentials theorem that are now machine-checked — Diaz’s Corollaires 1, 2, 4 and 5 of the 2007 paper in general, and at a candidate the facts that u³ and axis multiples leave ℒ̃, so e^(βπu) is transcendental (f3c56f5). v1.14 (304) then takes all of Section 2 of Diaz 2007 under the same hypothesis, and pins down where that route stops: a strong six exponentials configuration fed with a candidate’s own data exists only for k = 2 and 3, so the theorem excludes u² and u³ from ℒ̃ and no higher power (2c75c4b). The day closes at v1.15 (307), where the strong four exponentials conjecture plus Baker’s theorem implies the sharp four and that implies Waldschmidt’s strong five, and Waldschmidt’s 1988 remark is corrected to compare the strong five with the sharp four rather than with Conjecture 1.2 (631d51f). No new mathematics is claimed, and prove2me-logs carries the same day from the research side, down to a note that Brownawell 1974 is “related by the exponential function” (d89c37f).

Field Note 20 — The Message Was the Fix — follows the Varignon perimeter submission that had been rejected six times: after the diagnostic was rewritten to say which term it measures, how large the statement is once expanded, and to suggest naming a large subexpression with a definition, the next attempt stated the perimeter as a named definition and was accepted. The note also corrects two published numbers (the pre-registered “imports something recent” column was computed over every module first seen that day, so 32 of 96 rows flip from true to false; the new weekly rejection count had mixed seven weeks of runs at once) and explains Monday’s stalled kernel re-check: asked for one module, the checker checks every module whose name begins with that name, and that one shares its name with a folder of nineteen others.

The Diaz companion note reached v1.12: Waldschmidt’s 1973 theorem in its algebraic-independence form is now machine-checked — if x₁, x₂ and y₁, y₂ are linearly independent over ℚ and e^(x₁y₂), e^(x₂y₂) are algebraic, then two of the eight numbers x_i, y_j, e^(x_iy_j) are algebraically independent (8b015b3) — formalised as a one-column extension of the four exponentials development rather than a new development of its own. That closes what the previous version had to carry as a hypothesis: the consequence added in v1.11 is unconditional, Section 4 no longer says the theorem is not formalised, and the status “Proved, assuming Waldschmidt 1973” is gone from Appendix A. It brings Schneider’s eighth problem — at least one of e^e and e^(e²) is transcendental — and the e^(π²) statement with it. No new mathematics is claimed, the mirrored library stands at 283 results, and prove2me-logs carries the same day from the research side (22c5195).

curve-symmetry-lean no longer carries ONBOARDING.md, the coding agents’ handoff and tracker, removed at the author’s request (d99bc17); it stays in the git history, last version at f618c4a, and the README says so for the older verification notes that cite it. The README now lists the repository’s tags through sprint-4-complete and sprint-7-complete, and STATUS records the Sprint 7 commit’s two CI runs. This is the follow-up to the 30 September publication, not a new result.

On 29 November 2024 Terence Tao conjectured on the Lean Zulip that the only nontrivial one-generated magma satisfying law 1518 of the Equational Theories Project, together with four target laws, is the three-element cyclic shift. I proved it in core Lean this month, in magma-1518-obstruction-lean. Since 30 September it is a registry record: PALOMAR-2026-09-30-000005.

LeanFrontier shipped v0.2.0, its first library release since v0.1.1’s two modules: 102 accepted modules on Lean and Mathlib v4.34.1 across 15 top-level areas, nine modules deep at its longest import chain, with the Markov uniqueness conjecture stated formally and one classical coprimality hypothesis resolved by a formal computation of two rings of integers. Admission is still mechanical and grew with what went wrong in practice — kernel re-check by leanchecker, no build- or import-time code, add-only submissions, and conjectures as a first-class quota-limited kind. The same day a batch of outside submissions from @qazW12345 landed: the eighth cyclotomic field’s Galois group identified as a Klein four group (#445), the missing Gaussian quadratic direction added (#446), and exactly three quadratic intermediate fields proved, which completes that thread (#456); topological transitivity for the full tent map, transported through the accepted Ulam homeomorphism to the parameter-four logistic map (#444); the first cofinality bridge between the corpus’s Furstenberg topology and Mathlib’s generic profinite-completion indexing category (#443); and Descartes curvature reflections bundled into an algebraic action layer (#457). The evidence ships beside the code, including the citable corpus-v1 dataset snapshot; the running record is at the field notes.

The Diaz companion note reached v1.11 with three corollaries on rational squared moduli, each machine-checked: if t^2 + pi^2 is rational for a real t != 0 with e^t algebraic, then e^(i*gamma/pi) is transcendental for every rational gamma != 0 (Corollary 3.8), so the two remaining open statements cannot both fail at rational data; logarithms of algebraic numbers that are algebraic over Q(pi) with rational squared moduli are rational multiples of one another up to conjugation (Corollary 6.9); and at most one pair ±t makes t^2 + pi^2 rational, so (log 2)^2 + pi^2 and (log 3)^2 + pi^2 are not both rational (Corollary 6.10). Section 4 adds a specialisation of Waldschmidt’s 1973 theorem, checked with that theorem as a hypothesis. The mirrored library stands at 268 results: the fifth size wave adds six second proofs and one node, closing at 268 of 268, and prove2me-logs carries the same day from the research side (9bed59e, 1c5714c).

curve-symmetry-lean went public on 30 September: the note Sharp symmetry bounds for real algebraic curves, as PDF and TeX, together with the Lean 4 port that checks every theorem, lemma and remark of it — 108 modules and about 900 theorems and lemmas, using only propext, Classical.choice and Quot.sound, with no sorry and no native_decide (f0b97b7). COVERAGE.md maps each claim to its declarations and to the reading it is checked at: for d >= 5 the note classifies the curves attaining the maximum max(d, 2d-4) rotations as Re(z^(d-2)(|z|^2 + a)) = 0 up to similarity, with their exact ambient Möbius groups, and the port reaches the genus from an explicit basis of holomorphic differentials rather than Riemann–Hurwitz. Theorem 1 alone is also published in sharp-symmetry-bounds-lean and registered with Palomar as PALOMAR-2026-09-18-000007. The last sprints before publication put the machine-checked halves into the prose — an Appendix A to the note saying where each statement is checked, by what, and who checked it — and added negative controls that make three mutated copies of the registry entry fail their own pre-checks for the intended reason. An e-mail to Alcázar, Lávička and Vršek went out on 30 September reporting that the note’s irreducible quintic is a counterexample to Lemma 9 of their arXiv:1801.09962v1; no novelty is claimed anywhere, and CHECKS.md records exactly what has and has not been checked.

sharp-symmetry-bounds-lean now carries the equality case in the README instead of only in the statement: a figure and its drawing script for Re(z^3(|z|^2 + i)) = 0, the d = 5 member of the extremal family, which has six rotations — the maximum 2d - 4 — plus a view of its complex points. The script pins numpy and matplotlib inline and runs with uv run figures/quintic.py. No Lean file, challenge, solution, comparator or registry configuration changed, so the registered commit is unaffected.

Field Note 19 — Aimed at the Number — opens with a submission that arrived ten hours after the previous note’s day saying, in writing, that it had been chosen to add an import edge: the thing the accumulation series counts had become something a producer aims at. The two facts are about Varignon’s parallelogram’s perimeter — adjacent sides half the diagonals, so the perimeter is their sum — and the import is genuinely used, calls the corpus’s Varignon theorem inside the proof. It was then rejected for RESOURCE_LIMIT_EXCEEDED: the statement, fully expanded, is larger than what the receiver will fingerprint and probe, and the mathematics was never in question. The agent answered with five pushes in thirty-five minutes, each smaller, each refused in the same words — because the diagnostic said the theorem “exceeds the normalized-term limit”, and term reads as the proof while the receiver only ever measured the statement (4c4210f now says which term it measures, how large it is, and that the proof is not counted). The same contributor closed the day with the first bridge between the corpus’s Stern–Brocot tree and the Euclidean algorithm — k identical turns along a path record a quotient k of the algorithm, or k + 1 if the path ends there — both theorems stated in terms of SternBrocot.pair, a corpus constant that now appears in the statements of six submissions, which is the catalogue measure that cannot be moved cheaply. The corpus stands at 96 modules and 74 internal import edges.

Roadmap item R01 in curve-symmetry-lean is closed: the quartic Re(z⁴) = 1 is now proved to have genus three, and the proof reaches it from an explicit basis of holomorphic differentials rather than from Riemann–Hurwitz. Three steps, each a clean check.sh run against mathlib-v4.34.0-reuse: first the chart at infinity for y⁴ = 2 − x⁴, where f = 2 − x⁴ and g = 2s⁴ − 1 are squarefree of degree four so R01c-2 applies to both Kummer fields, and F·dx is regular at the place pulled back from (0, ζ) with ζ⁴ = −1 exactly when φ(F)/s² lies in the local ring (fdc7192); then the isotypic split of the holomorphic differentials under y ↦ i·y, which recovers each aⱼ(x)·yʲ·dx/y³ from F, σF, σ²F, σ³F with coefficients ±1, ±i (2024297); then the degree bound deg aⱼ + j <= 1 at infinity, leaving dx/y³, x·dx/y³ and dx/y² to span the holomorphic space and forcing genus three (b8c207e). The same commit settles Remark 5 of the note as printed — Re(z⁴) = 1 has four rotations and genus three, every curve of the m = 2 family has genus two, and no direct or opposite similarity carries the quartic onto one of them — and the axiom audit climbed 1,991 → 2,034 → 2,058 across the three steps. The note and its Lean port went public in the same week, with the launch described here.

Contributed PalomarRegistry/PalomarSubmission#156: registration of an accepted submission had been “under way” for more than seven hours, the status page’s last event being 2026-09-28T08:09:00Z — The submitter asked for this result to be registered, with no palomar/… tag on the repository and no PalomarArchive copy created. The issue reports that this is not local to one submission: the newest repository in the PalomarArchive organisation was created at 06:50Z and none since, for anyone, while the rest of the pipeline looked healthy — 24 workflow runs started in PalomarSubmission since 09:00Z, 20 of them successful.

Palomar’s automated review declined registration of magma-1518-obstruction-lean on two grounds, and both are now answered. The first was an overstatement: the abstract, the source record and the Challenge account presented “no finiteness” and “one target law instead of four” as a strengthening of the cited conjecture, while the repository’s own prior-work account says the conjecture carried no finiteness hypothesis — the README and notes had been corrected on 13 September, the metadata and the Challenge docstring were missed, so the repository contradicted itself in the two places a reviewer reads first (5d521ea). The second was scope: the compared declarations included the F5 and F13 members of Theorem F, two concrete finite examples rather than the family, and the review did not find research interest established for that group. The package now compares Theorem A and Corollary A′ alone, Challenge.lean falls from 178 to 84 lines, the family facts stay audited under their library names, and gen_palomar.py grew a --with-family flag that reproduces the earlier ten-declaration package (af908bb).

The second automated Palomar review found no mathematical blocking issue in the selected statements of magma-1518-obstruction-lean and one presentation problem: the README’s Palomar section still described the ten-declaration package, F5 and F13 members of Theorem F included, while the submitted Comparator configuration checks only the four Theorem A declarations — and still said nothing had been submitted. The README now separates what the configuration checks from what else the repository holds and how each part is checked, and PALOMAR.md splits its check record by package so the earlier ten-declaration runs, including the 33-theorem audit and the rc3 Comparator run made before the narrowing, are no longer read as evidence about the narrowed one (1794778).

Two Field Notes landed in two days. Field Note 17 — “The Same Fact, Twice” — has the Srinivasan collision identity coming back after the previous note recorded it lost, and then two submissions opened forty-six seconds apart from the same fork, both proving that −1 is a square modulo every Markov number: the first in the integers modulo m via Mathlib’s primitive sums of two squares, the second as the existence of r with r² ≡ −1 (mod m) via a Bézout lemma the same contributor had landed that evening. The receiver accepted both, correctly by its own rules — it compares each statement with Mathlib and the corpus exactly, and two notations for one fact are two statements to it — so the corpus now holds a result twice, and the only reason anyone knows is that a person read both. The same note extends the deepest chain in the corpus to nine modules.

The companion note to diaz-modulus-lean reached version 1.10 to withdraw a claim the note should not have made: Section 6 called the transcendence degree two of two unrelated candidates of commensurable moduli “the first constraint of any kind on such families”, and Diaz 2007, Corollaire 4(2) — a consequence of Roy’s strong six exponentials theorem — already puts one of u/v, v/u outside the algebraic span of 1 and the logarithms for such a pair. The sentence now cites it, all 81 identifiers match the platform, and the mirror holds 262 results (c04cf7a).

consilean is a new public Python repository that scores pairs of formal statements in Lean corpora on two axes — how similar they are, and how far apart they sit in the dependency graph. Similar statements that sit near each other are duplicate candidates; similar statements that sit far apart are candidate hidden connections, and Lean’s kernel stays the authority on whether a connection holds: a similarity score is a pattern, not a claim.

LeanFrontier merged #385, a 160-line LeanFrontier/NumberTheory/MarkovEquation/SlopeScaleGCD.lean carrying three new declarations, submitted through the fork of qazW12345 — the outside contributor whose fork was the intake route for the Nesbitt submission, and whose resolution of the corpus’s only conjecture closed Field Note 16 the day before.

Sprint 2 of consilean — the scorer of Lean statement pairs by similarity and dependency-graph distance, with the kernel left as the authority on whether a candidate connection holds — recorded a second H2 ranking and a read-only replay of the H3 axis against Mathlib v4.28.0, with the run reports generated into docs/ (1592971). One negative result is recorded rather than buried: the frozen Mathlib deprecation pairs cannot serve as later H3 links, because every since date is already earlier than the Mathlib revision that was scored (39a5a75). The wider statement reader therefore stays on the frozen deprecation set, and the duplicate list stays empty — none of the recovered pairs closed on the later revision.

Field Note 16 — “The Only Open Question Closed” — reports that the corpus’s single conjecture, stated on 22 September as #243 claiming the coprime-differents hypothesis in the discriminant formula for linearly disjoint number fields is load-bearing, was resolved three days later by the project’s external contributor. The witness is the eighth cyclotomic field: its two quadratic subfields generated by ζ + ζ⁷ and ζ − ζ⁷ are the square roots of 2 and of −2, each of discriminant of absolute value 8 and ramified only at 2, so their different ideals share a prime and the formula predicts 8² · 8² = 4096 where the actual discriminant is 256. The resolution arrived twice — a first pull request carrying the field theory alone was closed as superseded by the second, whose 512-line module is mostly the two rings of integers — and six further submissions came with it, each importing an accepted module: Kochen–Stone from Chung–Erdős, two layers of the Furstenberg topology, Stedman’s plain changes closing into a cyclic Gray code, and two on the Markov tree, the Stern–Brocot embedding shown injective on whole triples and the branch that always turns the same way identified with the odd-indexed Fibonacci numbers.

The companion note to diaz-modulus-lean reached version 1.9, which checks Appendix A statement by statement against the Lean nodes: four rows whose proofs take Baker’s theorem on linear forms in logarithms as a hypothesis are now marked “Proved, assuming Baker” and Section 1 lists that theorem as a third input used without proof, Corollary 3.4 is marked Not formalised because no node states it, Proposition 3.2 is restated as Diaz.quantisation_orbit_iff_re_ne_zero proves it, and all 81 identifiers match the platform, the mirror holding 254 results.

Field Note 15 is out, and both submissions of its day were merged without anyone touching a button. #307 shows that the three oriented Markov branches the coverage theorem split out are one branch up to a cyclic permutation of the coordinates, and packages the permutation that carries the canonical branch onto each of the others — which puts the module at the end of the corpus’s deepest chain: Markov equation, descent step, path layer, orientation, Stern–Brocot bridge, coverage, symmetry, seven modules and six import hops, all six built since Monday. #308 finishes a result left five weeks earlier: the Ulam–von Neumann semiconjugacy between the tent map and the logistic map at parameter four, submitted on 18 August through the change of variables x ↦ sin (π x / 2)², was missing the structural fact that that change of variables is a homeomorphism on the unit interval, so supplying it upgrades the semiconjugacy to a topological conjugacy — the two maps are the same dynamical system seen through a change of coordinates.

Five more versions of the companion note to diaz-modulus-lean landed on 24 September, and the mirrored library grew with each. Version 1.4 machine-checks the three barrier statements version 1.3 had proved on paper: the period never enters (Theorem 5.6 — for u algebraically independent of π the only quadratic relation with algebraic coefficients among 1, u, ū, iπ is the norm X₁X₂ − ρX₀², so a configuration that could detect a candidate uses the constant term, u and ū and never iπ), and Proposition 5.7 gives the relations a non-generic candidate can carry. Version 1.5 then corrected 1.4’s own claim that nothing known excludes a relation such as Re(u²) = π²: Théorème 0.2 of Roy and Waldschmidt (1997), the quadric version of the 1973–74 theorem, excludes every rational quadratic relation among u, ū, iπ for a candidate algebraic over ℚ(π) with Im u ∉ ℚπ, and two more barrier results followed (Theorems 5.4(c) and 5.6(c)).

Field Note 14 is out, and its day is nine submissions that each import an accepted result rather than starting beside it: most build on results accepted the day before, one on a module accepted three hours earlier, and one on the Furstenberg topology another contributor landed on 18 August — so the note’s own answer does not need a second producer, only an accepted one. The named work includes explicit Thue–Morse cube sums via Prouhet and Nicomachus, the Markov tree path layer that makes the descent step iterable, the classical Turán bound derived from the Caro–Wei bound accepted the previous evening, the Horadam addition formula built on the companion matrix, Sylvester’s reciprocal series summed to infinity, and Markov root reachability — every positive Markov triple reached from (1,1,1) by Vieta moves, the third of three consecutive mornings whose results each became the next one’s substrate.

The receiver’s own day in LeanFrontier was governance rather than mathematics. A pull request whose every changed path is a Markdown file under docs/ is now a documentation proposal (#291): no claim, no Lean, no build, and the three stages that build or run candidate code are gated off, so a prose change costs one short job instead of a Docker build and a Mathlib fetch — decided from the changed paths and never from the branch name, with docs/catalogue/ and docs/website/ excluded because one is generated from the corpus and the other publishes under the project’s name. The friction it removes was real and twice theirs: #290 carries a contributor’s rewritten docs/CONTRIBUTION-DIRECTIONS.md with their authorship after the OWNER gate had refused it, leaving six open directions and marking the ones that have landed.

Three versions of the companion note to diaz-modulus-lean landed in twenty-four hours, and the mirrored library grew with each: 182 of 182 proved results at note-v1.1, 195 of 195 at note-v1.2, and 200 of 200 at note-v1.3, with lake build Diaz clean and nothing behind the headline theorems but propext, Classical.choice and Quot.sound.

Field Note 13 is out, and its day was nineteen submissions — eighteen of them from the outside contributor of the last two notes — which took the corpus from 33 to 53 modules at a speed where the only step the contributor could not perform was the maintainer’s merge click. Most of the new work formed two clusters: the rational trees (both path enumerations of the positive rationals, the Stern–Brocot interval invariants, and a bridge proving that a Calkin–Wilf path and a Stern–Brocot path reach the same pair exactly when one is the reverse of the other), and a new Probability/ directory opened with three versions of the Paley–Zygmund inequality plus Cantelli’s and the Chung–Erdős inequality. Six of the eleven targets in the contributor’s own contribution directions are now marked landed there. The last arrival sat outside both clusters: the Caro–Wei bound, an independent set at least as large as the sum of the reciprocals of one plus each degree, merged by hand as #259.

The Lean and Mathlib v4.34.0 bump in diaz-modulus-lean (a4f0779, the same weekly bump that moved the rest of the Lean portfolio, most of it written up on 21 September) left thirteen warnings behind, all of them in ported mirror modules: eleven tactic steps the unused-tactic linter now reports as doing nothing — four push_cast, five field_simp <;> ring whose ring never runs, a gcongr <;> positivity — and two haveI the linter asks to be have. Each is removed or respelled (0c7ef1b), and because the edits also live in the porter’s patch table, regenerating the mirror reproduces them instead of reintroducing them: the porter’s --verify reads 117 identical and 0 differing against this commit.

Field Note 12 is out, and its subject is the contributor from Field Note 11 — the account behind the fork covered earlier this month — returning with two theorems built on modules already in the corpus rather than two isolated results. #179 proves the local descent step of the Markov tree: for an ordered positive Markov triple other than (1,1,1), the Vieta jump in the largest coordinate is positive, at most the middle coordinate and so strictly smaller than the largest. #180 bridges the accepted Ford-circle criterion to Mathlib’s own geometry: two Ford circles with non-zero denominators are externally tangent in the sense of EuclideanGeometry.Sphere.IsExtTangent exactly when their cross determinant squares to one. The receiver accepted them in 111 and 79 seconds, with zero exact Mathlib matches, kernel replay, downstream import and all 118 and 119 entrypoints already in the corpus still passing.

The Lean toolchain and Mathlib moved to v4.34.0 across the portfolio in one pass. erdos-straus-offset-lean, magma-1518-obstruction-lean, moebius-transcendental-lean and sharp-symmetry-bounds-lean took the bump together with a new CI job that audits the axioms their headline theorems actually depend on, so a silently new dependency on Classical.choice or worse would fail the build rather than sit in the proof term. inversive-geometry-lean took the same bump and its README’s pinned version followed (d512c1f).

The committed density data in lean-corpus-density now names the corpora and revisions it was built from (550a97d), so a figure in the report can be traced back to a specific corpus state instead of to the tool that read it, and the reproduction check of 21 September is recorded alongside it (31558d4). The repository’s claim is that machine mathematics accumulates; the data has to be pinned before that claim is checkable by anyone else.

The companion note to diaz-modulus-lean is now fixed at stable version 1.0 (f4cca8b) — the point at which the formal case analysis stops rather than a point along it. Every branch of Diaz’s conjecture is either closed by a machine-checked proof or reduced, by a machine-checked reduction, to one of three statements: that e^{-iγ/π} is transcendental for real algebraic γ ≠ 0, that e^{β/π} is transcendental for real algebraic β ≠ 0, and that |u| is transcendental for a generic conjugate pair of logarithms, which is the conjecture itself. All three follow from the strong four exponentials conjecture, and the note says so, with the section the abstract had always promised and the body never contained; section 5 gains the two interpolation obstructions proved on 19 September.

The graded results for the SAIR Stage 2 challenge are in. My solver scored 181 of 200, the same figure on both tracks from the same file. Earlier I wrote about how it reached 200 on the organizer’s published sample set by removing things: six per-problem gates, a borrowed reference solver, two lookup tables. That post was right about what it described and incomplete about what it implied.

The two items diaz-modulus-lean still listed under “What is not proved” — real analysis and interpolation determinants, it said — are proved, and neither needed them (2bc0828). DiazModulus.no_first_order_arithmetic_operator shows why Schneider–Lang has no input here: for a candidate u and F(z,w) = exp(uz + conj u w), a first-order operator a ∂/∂z + b ∂/∂w with polynomial coefficients whose values on Z² are all algebraic must have a = b = 0, because the bracket a(m,n)u + b(m,n)conj u is algebraic — the exponential factor is a non-zero algebraic number — Baker (carried as an explicit hypothesis, since Mathlib has no form of it) kills it, and a polynomial vanishing on a product of infinite sets is zero; ∂/∂z ∂/∂w, by contrast, does take algebraic values and is not a derivation. DiazModulus.kronecker_factorisation closes the second: the matrix of values of exp(auz + b conj u w) on the lattice is the Kronecker product of two Vandermonde matrices, so its determinant is a product of powers of theirs and is non-zero — the nodes are distinct because |exp u| = exp(Re u) ≠ 1, and the candidate’s arithmetic does not appear in it. Both hypothesis classes are conjecturally empty, which the nodes say on their face, and neither claims novelty; the first is stated for polynomial coefficients where the note states it for rational functions regular on Z², since clearing denominators is not formalised. The library now holds 166 of 166 proved nodes, axioms clean, and the dead-branch table for the four superseded FourExp statements moved into refresh_prove2me_archive.py, because the file carrying it is generated and the refresh had been overwriting it.

carlok/sharp-symmetry-bounds-lean is now a registered entry in the Palomar registry — PALOMAR-2026-09-18-000007, version 1, status registered, trust level high, on the source of commit ced9fe2 (the record’s own copy of the entry is here). This is the first third-party verification of one of these formalizations, and what the registry actually did is the news: it rebuilt the project in a sandbox from the pinned dependencies (Lean v4.32.0), exported the proof terms with lean4export and replayed them on nanoda, an independent kernel implementation rather than the author’s own build, then used the Comparator to check that Solution.lean proves the Challenge.lean statements — five theorems of SharpSymmetryBounds — using only propext, Quot.sound and Classical.choice, verified at 2026-09-18T13:50:47Z.

The 1973 construction whose four children began to close in diaz-modulus-lean is finished, and with it the four exponentials theorem in transcendence degree one. The norm child went first: FourExp.norm_to_polynomial_alg is proved (a38d9db) by linear algebra rather than the paper’s conjugates — the value is presented as Π ∈ ℤ[X][Y] reduced modulo the monic Q, P = det M is the determinant of multiplication by Π in the basis 1, Y, …, Y^(d−1), non-vanishing comes from a kernel vector that would contradict the minimality of Q, and smallness from the adjugate identity M·adj M = (det M)I. That made the core, FourExp.construction_core_1973, a Proved node by cascade.

sharp-symmetry-bounds-lean is a new public Lean 4 repository formalizing Theorem 1 of the working note “Sharp symmetry bounds for real algebraic curves”: if an infinite real plane curve of degree d ≥ 2 is irreducible over the complex numbers and is not a circle, its Euclidean symmetry group is finite — the orientation-preserving part cyclic of order at most max(d, 2d − 4) and the full group of order at most 2d — both bounds are attained in every degree, and for d ≥ 5 the curves attaining the rotation bound are classified, up to orientation-preserving similarity, as Re(z^(d−2)(|z|² + a)) = 0 with |a| = 1 and a not real.

sharp-symmetry-bounds-lean now carries a document written for someone checking the formalization rather than reading it: docs/THEOREM1.md gives the informal statement of Theorem 1, a proof outline mapped step by step to the Lean declarations that carry it, fidelity notes on where the informal and formal statements diverge, and reproduction instructions (85ddda8). The addition makes the informal argument the declared source, since formalization.yaml now points its original-proof source at this document and records the passing mechanical preflight. A stale comment about sharpness in lean/DirectBound.lean was corrected in the same commit.

The restated 1973 construction split in four the day before has begun to close in diaz-modulus-lean, one archive-and-port step per child. The field came first: FourExp.trdeg_one_presentation makes ω = x₁y₁ transcendental by Hermite–Lindemann, everything else algebraic over Q(ω) from transcendence degree one, then a primitive element scaled to an integral generator with a monic minimal relation and a common denominator for the eight numbers (5f3ee4e). Two of the remaining children needed restating first, because auxiliary_function and norm_to_polynomial had omitted that the four exponentials are algebraic — without it the ω-degree of the powers (e^{x_i y_2})^{jb} is unbounded — so they came back as auxiliary_function_alg and norm_to_polynomial_alg with the old pair left as a dead branch (fced437).

With the transcendence criterion and the zero count closed, the last thing between the four exponentials theorem in transcendence degree one and a full proof is Waldschmidt’s 1973 construction — and re-deriving it against the published statement before splitting its core turned up a sign lost when the formula was read off a noisy text layer: the order of differentiation is S = ⌊N²(log N)^(−1/2)⌋, not the published S = ⌊N²√log N⌋. It matters — the construction’s polynomial has degree about r·S and log-height about S·log S, both of which must stay under a fixed multiple of N²/√log N and N²√log N; with the paper’s S the ratios stay bounded (1.00 and about 1.9 at every size checked), with the published one they grow to 27.6 and 56.9 at N = 10¹².

The Sep 14–15 entries in prove2me-logs open a subtree under four_exponentials_trdeg_one, the one Open leaf of the Diaz mission that is a theorem in the literature: six new nodes joined by three accepted reductions (b4002e2), routed through Waldschmidt 1973 with two tools from his 1971 paper after reading and rejecting the two Roy–Waldschmidt proofs. Transcribing the statements from page images rather than the text layer caught a missing hypothesis (σ₂ ≤ σ₁) and a wrong exponent, and the lattice step forced one classical fact out into a node of its own — an exponential polynomial with distinct frequencies does not vanish identically — which closed as the branch’s first leaf (f8f57d7).

The Sep 15 entries in prove2me-logs pick the Diaz mission up where the previous posting left it — the zero count split, with a hole in its source — and carry it to the end of the branch. Every FourExp leaf was given a reduction rather than a citation (e14a87b), the transcendence criterion was written out as a Lean argument (75ed372), and two of the classical leaves were proved from what Mathlib already has: Gel’fond’s height bound for a divisor, which is the Mahler-measure file plus the last inequality, and the resultant step that Mathlib reaches through the Bézout identity but has to finish with the Leibniz expansion instead of Hadamard (bed556a).

diaz-modulus-lean now holds the four-exponentials branch instead of citing it: the FourExp nodes are archived alongside the Diaz ones (3d5d9ce) with the reduction sketch and its pieces (57f3ec7, 6714dcb), the refresh script searches the FourExp namespace too (ab6aa90), and each Open node’s formal statement and write-up is now mirrored into archive/prove2me/open — rewritten when the board changes, deleted once the node stops being Open, and covered by --check (3eb78a7).

The four-exponentials branch of diaz-modulus-lean went from a tree of Open nodes to a closed criterion, in a sequence of archive-and-port steps: the transcendence criterion reductions and their children were mirrored (707c4d2), then the 1973 construction reduction and its four children (e79b003), and then the leaves were proved one at a time, each archived, ported and dropped from open/:

prove2me-logs records the Diaz mission being worked by a cloud agent with nothing but a Prove2Me key, a GitHub token and the public brief: the first run proved DiazModulus.candidate_no_real_algebraic_line, the second added candidate_distance_transcendental by polarization on top of the first run’s line exclusion — both accepted, both mirrored into diaz-modulus-lean. Offline the same day, the multiplier module determined what an extension of the three-dimensional hull could be ({z : u·z ∈ L̃} = Q̄ + Q̄/u, so no shifted reciprocal survives) and the one-log saturation node ruled out a candidate inside Q̄ + Q̄·l. The session’s most useful artifact is a curl-free helper: passing a JSON body through a double-quoted shell string let bash expand $u, $v and $$ inside the LaTeX before the request went out, which wrote mangled mathematics into 52 published nodes — repaired from a pre-damage snapshot — and tools/p2m.py now builds the multipart request itself and accepts any body as @file.

The credit corrections in magma-1518-obstruction-lean went a step further: every equivalence among the four 1518 targets was posted on the Lean Zulip in November 2024 — Tao relating 47 and 614 through law 359, Tencer tying 817 to S³x = x, Bolan noting with Prover9 that 3862 implies the other three, and Nielsen verifying with Vampire that all four agree under left cancellation — so 3862 is no longer presented as an improvement over Tao’s conjecture, which the earlier correction still called one, and what the repository adds is now stated as the proof rather than the reduction.

Field Note 11 — “A Stranger Ran the Same Machine” — records the corpus’s first contribution from a first-time outside author: qazW12345, whose fork was the previous day’s news, sent PR #175 formalizing Nesbitt’s inequality, 3/2 ≤ a/(b+c) + b/(c+a) + c/(a+b), by clearing a positive common denominator onto 2N - 3D = (a-b)²(a+b) + (b-c)²(b+c) + (c-a)²(c+a). The only human intervention was approving the paused first-time-fork workflow; the trusted receiver then accepted the submission in 107 seconds — 61 added lines, no exact Mathlib fingerprint match, a kernel replay pass and an allowed axiom closure of propext, Classical.choice and Quot.sound — and the theorem is now importable as LeanFrontier.Analysis.Nesbitt, with the report and observation persisted by the usual generated changes (PR #178). Nobody judged the proof’s elegance or importance, which is the point: an unfamiliar contributor reached the same boundary through the ordinary public route. The corpus is at carlok.github.io/LeanFrontier.

diaz-modulus-lean absorbed the Prove2Me work rather than citing it: diaz_of_sfe — strong four exponentials implies the conjecture — was ported first (fcf8130), then the rest: Hermite–Lindemann is now proved here instead of assumed, so #print axioms Diaz.diaz_of_sfe returns only propext, Classical.choice and Quot.sound, alongside the fibre bound, the quantisation batch, the six exponentials node and the candidate statements mirrored with their platform submission ids (0144e57, fcf8130, e4880ab, 8d02fd4, 7cb8b3a). The repository also gained a complete copy of the mission: archive/prove2me/ holds all 167 accepted submissions for its 132 Proved nodes plus a manifest, so no proof of this mission exists only on the platform (1f05ae7) — kept deliberately unbuilt, since the files target the platform’s Mathlib revision and nothing in CI reads them, with scripts/refresh_prove2me_archive.py refreshing the archive and --check failing when it goes stale (735f5b4). The companion note is published as tex/diaz_prove2me.tex and the CI build was fixed by dropping a says-verified simp list (e8265ae).

carlok/LeanFrontier was forked by qazW12345 on 2026-09-11. Forks are the corpus’s intake path rather than a copy: a submission arrives as a branch on somebody else’s fork and is judged there, which is what Field Note 10 — PR #167, the Tribonacci submission — was about. A new fork is worth recording for the same reason a new submission is: it is the only outward sign that someone intends to try. The corpus itself is at carlok.github.io/LeanFrontier.

Contributed to leanprover-community/mathlib4: PR #43660 was merged into master on Sep 10, weakening unused hypotheses in Mathlib/Data/Finset/Pairwise.lean, Mathlib/Order/Antichain.lean and Mathlib/Order/Monotone/Extension.lean — five one-line binder changes, five insertions and five deletions. It answers a request on the mathlib Zulip to slice the machine-found weakenings into smaller, reviewable PRs, and the unused-assumptions pipeline supplied the edits: replace one binder with a weaker class, keep the proof unchanged, let the compiler decide. The larger #43503 — 32 typeclass weakenings across 29 files — is still open.

The unused-assumptions repository now separates what is published from what is merely being worked on: outreach/ workshop text for upstream pull requests and messages — including other people’s contact details and prose that is not its author’s to publish — is ignored at the root rather than parked in a sibling repository (43e092a), since the drafts are about this project’s results and belong beside them. The same instinct ran through the leak-detector test, which had been asserting that no shipped tool names the private sibling project while spelling out exactly those names as literals — now assembled from fragments so the repository stops carrying the one string it exists to withhold (3e1cb9a, 78ce2c0). One weakening was also withdrawn as unwanted despite compiling (b0e1f4f): a patch surviving the compiler is not the same as a patch worth publishing.

The Sep 9 session in prove2me-logs closed DiazModulus.diaz_of_sfe: with x = (1, u) and y = (1, conj u) the four products are 1, conj u, u and the squared norm, all in the tilde space, and Hermite–Lindemann discharges from a node the mission had already proved — so strong four exponentials is the only hypothesis left standing. It came out of a design review that rejected its own design: three scoped reviewers returned REJECT on the alternative route via algebraic independence of logarithms, nothing was published from it, and the argument turned out to already exist verbatim in the accepted diaz_of_schanuel submission.

magma-1518-obstruction-lean grew a Palomar-ready package: Challenge.lean states Theorem A and the F_5 / F_13 members of Theorem F as coefficient matrices without imports, Solution.lean proves them from the core development and kernel decide, and a comparator pinned to Lean v4.33.0 accepts the pair locally — formalization.yaml, comparator.json and a PALOMAR.md readiness record are generated by scripts/gen_palomar.py.

A second Sep 8 session on the Diaz tree closed the free half: no admissible matrix exists there, and that is now proved, after which norm_free closes onto the published statement (S) and the frontier stands at four leaves. The log also publishes an SFE route the session’s other model proved and withheld, records the lesson that the relation you are using is the one that breaks your argument, and scopes the next target with a brief for the four-exponentials theorem at transcendence degree one.

carlok/prove2me-logs is the working log of my Prove2Me formalization activity — per-mission entries with theorem uuids, Lean environments, and what remains open — public since Sep 7 as a record of the work rather than an archive of the proofs. The first entries record dead ends beside progress: the free-ring no-go formalized with its prose proof intact, a six-exponentials no-go note with a Waldschmidt erratum, and a Diaz bridge node that turned out to attach to nothing. Day two records the Diaz tree and writes up the decompose–link–iterate rule behind it: by the fourth generation the main theorem’s difficulty sits in a single named leaf — pi transcendence — with both leaves of the second branch named.

carlok/unused-assumptions is a new public repository (visible since Sep 4; v1.0–v1.2 tagged Sep 6, archived at doi:10.5281/zenodo.22549525): theorems in Mathlib whose stated algebraic setting is stronger than their own proof requires. The method is one sentence — take a theorem, replace one binder with a weaker class, keep the proof byte for byte, compile it alone — and every row of data/survivors.jsonl carries what is needed to put the claim back in front of the compiler. A verifier rechecks each row at the Mathlib revision the manifest names, refuses to run against a different one, and requires #print axioms to rest on nothing beyond propext, Classical.choice and Quot.sound. Re-verifying the 36 candidate patches against a later Mathlib kept the 33 that still hold, and the README now answers the prior-art question explicitly rather than leaving it to the reader.

unstated-conclusions (public since Sep 6) is the dual of unused-assumptions: instead of weakening hypotheses, it asks which theorems in Mathlib prove a stronger conclusion than they state. It reads the root of the proof term — if the last step is a weakening lemma (le_of_lt, Or.inl, Exists.intro w _, And.left, …), the stronger statement is already there as a subterm with its own proof, so the finding typechecks by construction. A hand-written table of 22 weakening lemmas is the only judgement. The project runs in two parts with a statistical wall between them: Part 1 is a pilot at the fifty-candidate gate on unused-assumptions’ own survivors (a rate there is a rate among those theorems, and nothing more), and Part 2, the library-wide measurement, starts only after Part 1’s table is frozen.

First check-in on my Prove2Me profile: joined this month, rank Master, trust 33, six missions, 35 statements solved and 32 posted. Three proofs landed today with my name on them, all against Mathlib 0df444a (Lean v4.33.1).

Contributed to leanprover-community/mathlib4: PR #43503 weakens unused typeclass assumptions on section variables across 29 files — 32 one-line changes, 32 insertions and 32 deletions. Each was found by the unused-assumptions pipeline (LLM + Lean 4 propose, the compiler decides): replace one binder with a weaker class, keep the proof unchanged, compile it alone. Every change built against its unmodified file, with the whole library compiling locally at 633b366493. It is one PR rather than many by deliberate choice, citing mathlib’s own #42214 (813 files of the same kind of change) as precedent; the background is on the mathlib Zulip, where a reader spotted a further simplification in one refactored file.

Building a branch from all 36 weakenings in unused-assumptions applied only 28, and the eight that did not apply are not all failures: two patches for Indicator.lean and three for Untop0.lean rewrite the same variable line in different directions — one weakening the algebraic class, another the order — so they are alternatives rather than additions, and applied in sequence the first moves the context and the rest silently do not apply. patches/README.md now says so, with the further caveat that a file carrying two weakenings at once is a combination nothing here has compiled, since REPORT-master.json is per-patch and not per-combination, and three tests hold the line: alternatives must be documented wherever a pair rewrites one line, every patch touches exactly one file, and every changed line is a variable line.

magma-1518-obstruction-lean grew a third result overnight: Theorem F builds an explicit parametric family of finite magmas satisfying law 1518 that violate the four targets 47, 614, 817 and 3862 — the ETP’s known 15-element countermodels are the family’s two smallest members, which then continues with 27, 39, 51, 75, … elements. A companion classification shows the base-dependent extensions of the Z/3 shift come in exactly 8 classes for p ≡ 1 mod 4 and 4 for p ≡ 3 mod 4, with only the family and its conjugate refuting. The 15- and 39-element members are checked by the Lean kernel via decide with no axioms, and the classification rests on Gröbner bases over Q and over every F_p with p ≤ 257.

The results of magma-1518-obstruction-lean went out on the Lean Zulip, and the repository briefly carried a draft of that announcement before it was removed the same morning: an announcement lives in the thread it was posted to, not as a copy in the repository that announces it. The same pass repointed the markdown notes at repository paths, so a reader followed a link into the repository rather than into a working copy.

magma-1518-obstruction-lean is a new public Lean 4 repository about the Equational Theories Project law 1518, x = (y ◇ y) ◇ (x ◇ (y ◇ x)). It proves that every one-generated magma satisfying 1518 and 3862 is trivial or the Z/3 shift — Terence Tao’s conjecture from the November 2024 Lean Zulip, now without a finiteness assumption and with a single target law — where the core table-and-closure argument carries no axioms. A second result shows constant-coefficient magma cohomology cannot refute 1518 ⇒ 47, 614, 817, 3862 from any finite base: H² vanishes over the shift, so every such extension is a direct product. The README states the full theorem set (A–E) with a per-statement tally of confirming tools — core Lean, Vampire, Mace4, z3, brute force — and notes the repository claims no new implication, since the ETP has settled them all.

The write-up in magma-1518-obstruction-lean now says where Proposition A″ comes from: its equivalence of the four single-variable targets 47, 614, 817 and 3862 under 1518 together with left injectivity and left surjectivity — which hold in every finite 1518-magma — re-derives an observation of Bruno Le Floch posted on the Lean Zulip’s Equational stream in October 2025, that in a finite 1518-magma the squaring map and all left multiplications are bijective and the single-variable targets are then equivalent to each other and to S S S x = x. Naming the observation that was being re-derived is the difference between a proposition that stands on its own and one that stands on someone else’s step.

The release itself is already noted: parsimagma v1.0-stage2 settles all 200 problems of the SAIR Stage 2 sample set in one standard-library-only Python file, archived at doi:10.5281/zenodo.22237100 with a write-up at doi:10.5281/zenodo.22214743.

After parsimagma went public, someone read it properly.

moebius-transcendental-lean tagged v0.2.0, which classifies the conjugation-degree spectrum on the transcendental locus: conjDegree attains every value in ℕ∞ except 0, which it never attains. Every finite degree gets the same explicit witness, zₙ = sⁿ + i·s with s = liouvilleNumber 2, while the ⊤ stratum comes from an algebraically independent real pair. It compiles against Mathlib v4.32.0 with no sorry, and the permanent axiom-verification module confirms the ten new declarations close over exactly {propext, Classical.choice, Quot.sound}.

Field Note 10 — “The Fork Was the Test” — records the first submission to arrive from another person’s fork: PR #167 defines the Tribonacci sequence and proves that every term past zero is positive and that finite partial sums satisfy a telescoping identity — a genuine recurrence-sequence result, not a re-labelled Fibonacci or Padovan one. A Mathlib base bump moved underneath the PR mid-flight, a clean rebase put it back at the boundary, and the receiver — not a mathematical reviewer — decided whether it could cross. The corpus is at carlok.github.io/LeanFrontier.

Field Note 09 — “The Test Was a Submission” — records a deliberately ordinary theorem contribution exercising the freshly upgraded receiver end to end: local report, trusted validation, observation, catalogue, and automatic merge. The submission behind it is PR #169, adding natDegree_eq_zero_of_comp_X_add_C_eq_self, the natural-degree consequence of the existing polynomial translation-rigidity theorem, with the receiver report returning accepted (the note itself landed as PR #171). The corpus is at carlok.github.io/LeanFrontier.

moebius-transcendental-lean is a new Lean 4 + Mathlib formalization, now public, of the conjugation degree δ(z) = [Q̄(z, conj z) : Q̄(z)] on the transcendental locus ℂ ∖ Q̄, following the companion paper p19.tex. It is archived with a Zenodo DOI and shipped as v0.1.0 and v0.1.1 with CI and a permanent axiom-verification module. The δ = 1 stratum is the subject of the companion diaz-modulus-lean.

diaz-modulus-lean gained a Palomar submission surface on its palomar branch, parallel to the erdos-straus-offset-lean one: an axiom-free core, a Challenge.lean that imports full Mathlib so the statements match on the nose, and a companion note with attribution and search record. The repo also picked up an Apache-2.0 licence at the root.

erdos-straus-offset-lean now carries a Palomar submission surface on its palomar branch: a Challenge.lean statement surface, a Solution.lean with the proved counterparts, and a comparator that audits the pair, pinned to Lean/Mathlib v4.32.0. The Comparator result recorded in formalization.yaml passed on both kernels — Lean’s default kernel and the independent NanoDa kernel accept the four compared theorems, with the axiom closure limited to propext, Classical.choice, and Quot.sound. The metadata file also declares the automation method as an agent (Claude Opus 5 High via Claude Code).

LeanFrontier’s Field Note 08 records the corpus moving to Mathlib v4.33.1 on schedule, with the version chosen by nobody: the upgrade pipeline rebuilt the fingerprint index, re-audited all 114 entrypoints, replayed the kernel, and opened the pull request itself — a person only merged it. Getting there took three stacked defects, each invisible until the one before it was fixed, the best being a validator that refused the upgrade over bytecode it had compiled into its own working tree while running. A fourth outside contributor also sent in a submission, still open pending a rebase onto the new toolchain, and no acceptance was weakened by the upgrade.

carlok/LeanFrontier was forked by giacomoleonzi on 2026-08-24. In this corpus a fork is not a copy but the way in: a submission arrives as a branch on somebody else’s fork and is judged there, which is what Field Note 10 was about. This fork is the one the Tribonacci sequence submission later arrived through (PR #167). The corpus is at carlok.github.io/LeanFrontier.

Opened issue #3954 on TauCetiProject/TauCeti, the machine-generated Lean 4 library, to thank its maintainer and share a measurement: replaying its public history shows internal import density rising from 0.40 to 1.55 per module. The report is the courtesy side of the lean-corpus-density analysis, which used TauCeti’s history as evidence that machine mathematics accumulates.

LeanFrontier’s Field Note 07 documents the day the maintainer left the merge path: receiver-accepted submissions now merge themselves, with an allowlist read from the default branch so no submission can approve itself, and four have landed with leanfrontier-receiver[bot] as the merging identity — two of them four minutes after opening. Two new theorems entered the corpus under the unattended gate: translation rigidity for characteristic-zero polynomials (over a characteristic-zero integral domain, a polynomial invariant under translation by one nonzero element is constant) and the finite pairwise squared-difference identity (in any commutative ring, the sum of squared differences over all ordered pairs is twice the cardinality times the sum of squares, minus twice the square of the sum). The note also pre-registers the launcher A/B experiment — two launchers differing in exactly one paragraph, eighteen accepted submissions per arm, and a stopping rule fixed in advance — with the first three arm-carrying submissions already in.

LeanFrontier’s Field Note 06 measures the corpus against Tau Ceti, a second machine-generated Lean 4 library, and finds that machine mathematics does accumulate: Tau Ceti’s internal import density rose monotonically across its history, narrowing the open question to whether accumulation survives without a human-written roadmap. The day also took the human out of the merge path — receiver-accepted submissions now merge themselves, and the first unattended submission opened at 15:39 and merged at 15:56:56 — and admitted conjectures as Prop-valued definitions fingerprinted by value, so a conjecture restating known mathematics is rejected as a duplicate. Three new submissions landed (thue-morse-prouhet-power-sums, stern-brocot-coprime-enumeration, padovan-sequence-sum), taking the corpus to 27 modules, and running the pipeline unattended surfaced four defects that reading had missed. The measurement itself lives in the new lean-corpus-density repository.

lean-corpus-density is a new, reproducible measurement of dependency density in Lean 4 corpora, human and machine-generated. Replaying Tau Ceti’s commit history shows its internal import density rising monotonically as it grew — 0.40 edges per module at ten modules up to 1.55 at 2,314 — evidence that machine-generated mathematics builds on itself rather than merely piling up. The whole analysis is reproducible from file headers; no build is required.

diaz-modulus-lean is a new Lean 4 formalization of a negative result on Diaz’s 2004 modulus conjecture: for a candidate u with e^u and |u| both algebraic, the conjugate ū is a rational function of u with algebraic coefficients, so no statement about vanishing matrix coefficients over the algebraic hull can separate a candidate from an ordinary complex number. It machine-checks the conjecture’s question of method — how non-holomorphic maps like conjugation and modulus could enter a transcendence proof at all — in the negative direction.

LeanFrontier accepted its first batch of machine-generated theorem submissions: the Furstenberg topology on the integers, the tent map semiconjugate to the logistic map, Lucas numbers and their Fibonacci bridges, the Fibonacci Q-matrix, and a closed form for the Josephus problem’s survivor. Submitted modules are now replayed through the kernel before acceptance, and the whole corpus is rechecked whenever Mathlib is upgraded.

LeanFrontier accepted five more machine-generated submissions in a single day: a greatest sequence below a ceiling with bounded steps, how the greatest-step bounded minorant responds to its constraints, Stedman’s plain changes ringing a full extent, Hermite-Lindemann implying that exp is injective on algebraic numbers, and a generalization of finite-group character sum vanishing to noncommutative rings. The receiver was hardened along the way — submissions now authenticate as the LeanFrontier Receiver app, and the corpus dependency graph is published in the catalogue. The whole day is documented in Field Note 05.

LeanFrontier is a new Lean 4 library of machine-generated, kernel-verified mathematics. Every theorem it contains has been checked by Lean’s proof kernel rather than taken on faith, which means the machine-generated results carry the same formal guarantees as hand-written proofs.

carlok/LeanFrontier was forked by matteodesimone and rlacroce-rdi on 2026-08-18. A fork is this corpus’s intake path rather than a copy: a submission arrives as a branch on somebody else’s fork and is judged there, so a new fork is the outward sign that someone intends to try. Both used it that day — rlacroce-rdi for the Josephus survivor closed form for step two (PR #55, merged the same afternoon) and Matteo De Simone for a run of submissions from the Fibonacci Q-matrix to the Furstenberg topology on the integers (PR #56 onward). The corpus is at carlok.github.io/LeanFrontier.

inversive-geometry-lean is a new Lean 4 library for generalized circles — “circlines” — that treats circles and lines as a single object. Each circline is cut out by a Hermitian equation, giving a uniform treatment of inversive geometry inside a proof assistant.

euclean is a new research project asking whether a machine can recover mathematical structure from an anonymized formal theory armed only with a proof checker. The experiment strips away all the human-readable names and intuition, leaving just a formal theory and the kernel’s verdicts to work from.