#research

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.

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).

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.

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.

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).

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).

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).

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).

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.

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).

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).

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).

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.

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)).

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.

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.

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.

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.

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¹².

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/:

quadratula is a new public repository that asks how much of the implication structure of Schröder’s 990 quasigroup equational laws is already visible in small quasigroups. It enumerates every quasigroup of order 1 to 6 up to isomorphism — 1,131,984 classes, in Rust on a pinned toolchain — computes which laws each one satisfies, and measures that exhaustive floor against Bruno Le Floch’s arXiv:2603.29909: quasigroups of order at most 4 already witness 95.34% of the 726,207 law-level non-implications (91.68% of the 1,958 between the 47 classes), and going to order 6 reaches 96.70%, realising 94 of the 114 varieties and separating 42 of the 47 classes.

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.

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).

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.

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.

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).

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.

parsimagma now enumerates, pair by pair, every implication that is false in general but holds for every finite magma: 820 ordered pairs — 610 from the unresolved hard core and 210 from the saturation-refuted set — decoded from the ETP’s closed implication graphs into data/etp/infinite-only.tsv. The exact split answers the question left open in the project’s #1474, and it makes the corpus’s coverage readable honestly: 610 of the 1062 hard-core pairs can never be refuted by a finite construction, so the real figure is 411 of the 450 finitely refutable (91%), with the remaining 39 listed. A differential test against the ETP’s Lean-verified finite graph agrees on all 797 finite claims.

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 certificates README in parsimagma had the origin of its three permitted axioms wrong — they enter through the finOpTable encoding, not through what decide invokes — and the correction credits Wenlin Zhang, who settled it by re-emitting 44 affine models as plain arithmetic operations: same goal, same tactic, no axioms, 44/44 at carriers 2–9. The same README now also records that the judge’s default policy admits no axioms at all, so the false column of the table fails under it while the true column does not — which is the difference between a certificate that is checked and one that is merely re-runnable.

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.

parsimagma is tagged v1.0-stage2: one standard-library-only Python file — no database, no lookup table, no LLM call — reaches 200/200 on the organizer’s 200-problem sample set, confirmed by two independent runs agreeing problem for problem and explicitly not the private graded set. Three search mechanisms split the work: finite model search refutes false implications cell by cell, critical-pair completion proves most of the true ones, and ordered superposition under a Knuth–Bendix ordering takes the rest. Every derived equation carries its replayable derivation, paths are double-checked before any Lean is written, and certificates are emitted from the inference DAG rather than flattened — 13,728 bytes against 3,634,949 on the hardest problem.

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}.

parsimagma’s citation surface was settled deliberately: the README badge and posts cite the concept DOI 10.5281/zenodo.22237100, which always resolves to the newest release, while the paper’s bibliography keeps the version DOI, because a report of measurements should pin the artifact it measured — and the write-up DOI was repointed at the current version rather than the one carrying a superseded-version banner (16d60e0). The same pass took the working directory out of the published Vampire logs: the proofs are worth publishing, the absolute temp path they were produced under is not (2f9bf2d).

parsimagma is a new public signature and coverage engine over the 4,694 equational laws of the Equational Theories Project, asking which ETP constructions cover which separations. Its central finding is that the residual is not uniformly hard: at least 411 of the 1,062 Vampire-unresolved implications have finite countermodels on 9 to 32 elements, found in seconds by a structured algebraic sweep where three SAT/SMT-style solvers all fail from carrier 11 upward. The repo also argues the published count of unresolved implications sits below a provable floor and independently reproduces corrected figures for the paper’s section 5.1.

The Equational Theories Project’s completed implication graph turns out to be fetchable: finite_graph.json and graph.json are build artifacts the site serves and the repository does not track, and decoding them reproduces the project dashboard exactly, recovering its two remaining open cells, (677, 255) and its dual, without being told. That splits the 1,062 Vampire-unresolved implications precisely — 610 require an infinite model, 450 have a finite counterexample, 2 are still open — which settles the question parsimagma had filed as unanswerable in issue #1474, and corrects its own headline: 610 of those 1,062 admit no finite counterexample at all, so the corpus reaches 411 of 450, not 411 of 1,062. Same measurement, 39% or 91% depending on which denominator you bother to compute. The earlier claim that the circulating figure of 310 sits below a provable floor is withdrawn: counted up to duality the same set is 316, so 310 looks like a dual-class count against an earlier snapshot rather than an error. The graph is also Lean-verified, so it can contradict the engine, and does not: 790 of 790 finite witnesses agree, and 19,392 order-5 laws extracted from a fork’s branch agree too.

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.

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.

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.