Blog

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.

roundstorm’s desktop app now generates 32 random bytes on every launch, hands them to the daemon as ROUNDSTORM_TOKEN and injects them into its own page, and the daemon refuses /api and /ws without it — unset, the headless CLI and every script behave exactly as before. It is narrower than “auth”, and SECURITY.md now says so: it stops another process on the loopback socket and another user on a shared machine, and makes ROUNDSTORM_HOST=0.0.0.0 defensible, but not malware running as the user (17618e7).

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

deck-lovers’ /ws disconnect cleanup ran unshielded, so a cancelled task could skip telling the audience the projector had left and leave stale clients behind — Starlette’s TestClient cancels the app task right after sending the disconnect, which made the websocket tests hang about four runs in ten. The cleanup is now wrapped in a shielded anyio cancel scope, two test races are gone, and a regression test cancels the handler the way the client does (3c4e938).

cdclkit’s target-phase search copied the whole trail into the target at every new deepest trail. The comment said improvements become rare quickly, which is true once conflicts start and false before: a search that makes many decisions without one improves on every decision, so n decisions copied 1, 2, …, n entries — 65,536 declared variables and one unit clause took 144 s in Python, 131,072 took 4.2 s natively, and each 4× in variables cost about 13–19× (e43a4ac). A counter now records how much of the trail the target already holds, only the new suffix is copied, and the target still ends up byte-for-byte what the full copy produced.

caciarabot’s validator already caught a file over Telegram’s upload ceiling, but size is not the only way Telegram refuses a photo: width and height above 10000 px, or a longer side more than 20× the shorter, fails with PHOTO_INVALID_DIMENSIONS even at a few hundred KB — and a panorama or tall screenshot is exactly the file people drop in. A new telegram/imagesize.py reads the dimensions out of the header with the standard library alone — PNG (IHDR), JPEG (skip the APPn segments to the start-of-frame marker) and all three WebP variants — checked against macOS sips on all 142 real images in media/ with no false positives (b06e315).

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

A Dependabot pull request that failed one Ubuntu cell with “database is locked” was not the bump’s fault. Importing nearly anything under server/src imports db.ts, which opens a SQLite file at import, and ten test files never set ROUNDSTORM_DATA first — so they opened the default data directory, the real database on a developer’s machine, and on CI one file shared by every parallel test process racing to create and migrate it (44a5bd9). A second bug surfaced in the same empty-HOME experiment: gate.test.ts called /api/bootstrap, which probes every brain, so npm test executed the real agy and cursor-agent CLIs on any machine that had them. scripts/test-setup.mjs is now preloaded into every test process and hands each its own empty data directory rather than relying on the next author to remember, gate.test.ts hits /api/memory instead, and a re-run under an empty HOME passes 196 of 196 while creating nothing there.

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

roundstorm is now public at v0.1.0: a local-first app where persistent, heterogeneous AI researchers deliberate for a set number of rounds on a hard question — you write the question once, they do the arguing. The download is a macOS Apple Silicon image, with the daemon runnable on Linux and Windows; the app bundles no models and no keys, needs Node 22.16 or newer and at least one installed, signed-in CLI brain (claude, codex, agy or cursor-agent), and the release notes state the limits rather than let them be discovered — not notarised, no authentication (the daemon listens on loopback and refuses website origins, which is not auth), advisory capability tiers, and Windows never actually run. The release-day work was a pre-public tune: CI, a real CSP, and a Node floor corrected to a 22.16 that CI measured rather than guessed (4c98425, 73568f8), the daemon moved to Express 5, CSS imports declared so the project type-checks under TypeScript 7, dependency updates taken where safe with Tauri held at 2.11 on purpose, and one open advisory recorded with why it does not reach the shipped app.

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.

dratify 0.1.6 fixed the README’s PySAT example — it loaded formulas with PySAT’s own parser, which stops at the % line every SATLIB file ends with — and closed a release path that let workflow_dispatch publish from a branch, with the pypi and crates environments now restricted to v* tags (108dd50, 5d0bb47). 0.1.7 is the security fix: three checker bugs found while tracing why PySAT’s CaDiCaL proofs do not verify, one of them a soundness hole where the pure-Python checker accepted refutations of satisfiable formulas when a list of steps held a negative literal — reachable through check_proof, though not from cdclkit’s own solver, and text proofs were never affected — alongside an unbounded literal that could size arrays for 10¹¹ variables and two false rejections, both checkers refusing valid proofs in which a lemma arrived unit at the root (61165f9). The PySAT failure itself is not the checker’s: the binding reads every CaDiCaL proof before flushing it, and with the documented workaround all four CaDiCaL versions verify 50 of 50, where glucose and Lingeling already did (2823854).

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

cdclkit 0.1.4 moves both halves onto dratify>=0.1.7, whose three fixed checker bugs include two that reach this package: --self-check could reject a valid proof, and the pure-Python checker could accept a refutation through check_proof (d33f84a). Publishing is now tag-only — the environment restricted to v* tags, the workflow_dispatch trigger gone, and the version check failing outright on any other ref — and make smoke, broken since the dratify split, now ties its module list to the source tree, with a packaging CI job that builds the wheel, installs it cleanly and runs it (b7b5426). Python 3.15 rc3 joins the test matrix (including a native-engine leg) and the README example is now executed by a test; the runbook’s recorded Sigstore gap was already covered, since every file on PyPI has carried a PEP 740 attestation since the first Trusted Publishing release.

The weekend digest swapped the tech feeds for a random Wikipedia article but kept the tech prompts, which tell the model it reads “computer-science-adjacent feeds” and must say something “technically true and not obvious” — handed a 150-character stub, that forces either an invented fact or a bolted-on code joke, and a county sheriff’s office had drawn a package.json comparison. A separate config/prompts/digest_weekend/ pool now holds three tones mirroring the tech one, confined to the excerpt and forbidden from asserting facts from memory or reaching for code-and-servers comparisons; the prompt is chosen by candidate.source rather than by re-checking the weekday, so it always matches its content, an empty weekend pool falls back to the tech pool instead of losing the day, and the validator requires the pool whenever the digest is enabled (932b0a6). A first pass still leaked — the Nagano article drew “visti i risultati complessivi”, implying an outcome the excerpt never stated — so the prompts now also forbid implying outcomes or quality the excerpt does not support.

forgepulse publishes two rankings of the same fleet — human attention, built from unique views, external referrers and new stars and forks, and raw clone volume — and they rarely agree, so a repository that reaches the top ten of both now carries an award badge beside its rank, in either view (55028f2). The condition lives in web/src/lib/rank.ts as inBothTopN, which is true only when the attention rank exists and both ranks are 10 or better; the badge is styled in styles.css and the rule is covered by rank.test.ts.

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

Weekend days — in the bot’s own timezone, default Europe/Rome — now pull the daily digest’s candidate from Wikipedia under a non-technical topic filter instead of the configured tech sources, and the daily-thought Wikipedia rabbit hole uses the same filter on those days; weekdays are unchanged, and weekday Wikipedia draws stay unfiltered (00e467f, PR #1). is_weekend_in_bot_timezone() in llm/scheduler.py is the shared check, looks_technical() in llm/wikipedia.py the heuristic, and weekend Wikipedia picks skip the English-only page fetch so Italian reads come through. The same day’s second change fixes how updates land: deploy/update.sh now rebuilds, then does podman compose down and up -d, because up -d followed by restart could leave the old container running the previous image; the script deliberately keeps -v off down, so the bind-mounted config, media and data/ trees survive (bbaa82c, PR #2). The test suite stands at 174 passing.

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.

A scheduled notify pass in topshift-trend can now fail halfway without repeating itself: per-chat deliveries are recorded as they succeed, so the next run skips the links a chat already received and retries only the ones that never went out, and the global cooldown baseline advances only after a clean pass (0ce1688, PR #9). Before this, one transient Telegram error in the middle of a batch could resend everything that had already arrived. A ruff UP035 fix — Mapping imported from collections.abc — rode along.

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.

pickmydegree had been committing the HTML output of its test-coverage run, and CodeQL flagged the Istanbul report’s sorter.js assets as js/xss-through-dom inside that generated output (11e72fc). Those files are test artifacts rather than application code, so coverage/ is now ignored and the committed reports left the tree — roughly 22,800 lines of generated HTML and CSS removed and three added, merged as PR #2. The app source is untouched; only the repository stops carrying a copy of its own coverage run.

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.

pacenotch notices that Claude Code has refreshed its OAuth token by fingerprinting the credentials it reads, and that fingerprint used to be a SHA-256 of the access token — which CodeQL flagged as go/weak-sensitive-data-hashing (a63ee1f). The hash never left memory, but hashing the secret was never needed to detect a refresh: the fingerprint is now claudeAiOauth.expiresAt, a value every refresh moves and which is not secret at all, while a PACENOTCH_TOKEN cannot change while the program runs and gets a fixed fingerprint. It is the second CodeQL-driven correction in pacenotch’s credential layer after the recovery path stopped re-reading the token.

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.

forgepulse can now answer “who starred what, and when” across the whole fleet: a new /stars page lists every star across every tracked repository in one chronological feed — avatar, who, which repository, when — which GitHub only offers per repository and never across an account (af4a8ea). The backend adds a star_events table populated from each repository’s /stargazers endpoint requested with the star+json media type, which carries the true starred_at per user and so needs no backfill wait, unlike the human-attention baselines; it syncs alongside the existing star count.

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

deck-lovers’ /login handler set the proj_auth cookie to the projector password itself, so the plaintext password lived in every presenter’s browser — which CodeQL reports as py/clear-text-storage-sensitive-data. The server now issues a random per-process session token and compares password and cookie in constant time, which also means a server restart invalidates existing projector cookies; two converter test assertions that matched the bare fonts.googleapis.com hostname (py/incomplete-url-substring-sanitization) now check the exact stylesheet URL built by google_fonts_css_url() (fa4dfce).

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.

portcullis replaced paramiko’s AutoAddPolicy — which accepts whatever key a host presents — with an explicit trust-on-first-use policy (25da71b). Phase 1 is the first contact with a VM created seconds earlier by the same process, so there is no prior key to compare against and Hetzner does not publish the fingerprint through its API: the new policy accepts that first key once, logs its type and fingerprint, and Phase 2 still connects with that exact key pinned, so a later substitution is detected. The change addresses CodeQL’s py/paramiko-missing-host-key-validation alert, and the test that asserted the blanket policy now asserts the new one. The secret-handling pass of 21 September had already pinned the key Phase 2 connects with; the first contact was still an unconditional accept.

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.

The window columns in forgepulse were mostly empty at their recent end: GitHub’s traffic API lags a day or more, so counting back from the wall clock left the newest days without rows and the 1d column read zero for nearly every repository (7f5acb4). The windows now count back from the newest day that at least half of all repositories have a row for, and each window is capped at that day, so a stray early same-day row cannot leak in as a partial day or move the anchor — a plain MAX(day) would let one early reporter blank out everyone else. It also makes 1d genuinely one day: the old >= now − 1 day spanned up to two. It is the same lag the per-repository clone baselines were added for, now fixed at the window itself rather than at the comparison.

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

The segreto feature in caciarabot keeps a roster of who has posted — display names only, no message content, because the Bot API cannot list a group’s membership — but its dry-run log line wrote those names out in full. It now logs a count instead (db905db), and the README’s Privacy section says so explicitly: the events say how many people a secret was about, never which ones. The change also cleared CodeQL alert py/clear-text-logging-sensitive-data, whose “sensitive data” label was firing on the word “secret” rather than on a credential — the dataflow was real even where the rule’s name was not, and the count is all the operator needs to see the feature working.

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.

Podman only reports a host-port clash after the images are built, and only as an opaque “proxy already running” error that never names the port. The deploy script in deck-lovers now runs a pre-flight check in local serve mode before the build, naming the container or host process that is actually holding the port — 80 and 443 included when Caddy is started — while skipping this compose project’s own containers, so re-running over a live deck-lovers server still attaches instead of failing (5c07394).

portcullis hardened its own handling of the secrets it moves around during provisioning (f41693f): it no longer logs the first and last four characters of HCLOUD_TOKEN, keys/id_rsa is created 0600 from the start rather than being written and then narrowed, and the smtp.env values are shell-quoted before Phase 2 sources them as root — passwords containing $, spaces, quotes or backticks had been mangled or executed, and the file is now chmod 0600 on the VM before credentials are written into it. Phase 1’s SSH host key is pinned and Phase 2 rejects a different one immediately, so a swapped host cannot receive the second phase’s credentials, and preflight validation now runs before any Hetzner resource exists.

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

An MIT licence was added to repositories that had been public without one: cold-path-server-podman, llm-source-security-review, spriter, lifechess, eclipse-3d-sim — whose README was rewritten in the same commit — plus book and daily-drift-run. solids-hunter had a licence file whose text had drifted from canonical MIT; the canonical text is restored and the third-party carve-out it had absorbed lives in THIRD-PARTY.md, where it belonged.

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 echarts 5 → 6 bump in forgepulse changed the default legend position from top to bottom, so on both charts the legend collided with the x-axis date labels while the 48px the grid reserves at the top sat empty — legend.top is now set explicitly, so the layout stops depending on a library default (94fb8c1). The same release draws a filled marker on every data point, which on a hundred-day series is clutter; the dots are hidden on all eight series through one shared base while the axis tooltip still marks the hovered point (1f70b65). Both rode in with the vitest 4.1.11 / echarts 6.1.0 security bump.

fleetlens is now public: for a handful of Debian/Ubuntu VMs it logs in over SSH with Ansible, collects a fixed set of read-only facts and turns them into a JSON report, a Markdown report, a terminal summary and an optional email — nothing installed on the targets and nothing on them changed. It sits between “I SSH in and look around every few weeks” and a full monitoring stack: disk usage, pending updates, reboot-required, failed units and journal errors, with each host marked OK, WARNING or CRITICAL and the fleet taking the worst of them.

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.

A pass over open dependency advisories bumped the affected packages in every repository that carried them. On the JavaScript side: pickmydegree (vitest, happy-dom, vite, surge), storygen (vitest 4, vite 6, react-router 7), solids-hunter (vitest 4, vite 6.4.3), eclipse-3d-sim, lifechess, agility-trainer and they-live-agent (vitest 4.1.11), platosdf (vitest and its coverage package, 5.0.1), with lockfile refreshes in deck-lovers and express updates in neon-bumper-cars and collective-starship-game.

Seven repositories that had no continuous integration now run their own tests on every push: topshift-trend (running ruff and pytest), caciarabot and python-hosts-checker (pytest), euclean (pytest together with its Lean build), and quadratula, unstated-conclusions and prove2me-logs with smoke tests — in prove2me-logs’ case covering the p2m helper, the piece the mission journal is actually read through.

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.

vitthorio started following this account — a follow says someone is watching, the same way a fork says someone intends to try, so it is worth naming rather than counting. The login is not a stranger to the repositories here: their own fork of jalhund/cold-path-server is the other copy of the Cold Path game server that cold-path-server-podman containerises.

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.

The digest in caciarabot now skips candidate links whose target page is in another language (7fd451b), because GitHub trending routinely surfaces repositories documented entirely in Chinese — two of the fifty candidates in that day’s live fetch were exactly that, and posting one of them as the link of the day wastes the slot. The check runs in two stages, cheapest first: the pool is filtered on the title and description the source already returned, no extra request; only the picked candidate is fetched and checked, because verifying fifty to post one would be fifty requests a day, and a rejection drops that link and draws again, up to five times. For a GitHub repo the check reads the raw README rather than the repo page, since github.com serves <html lang="en"> on every page it renders, including for repos written entirely in Chinese; elsewhere the declared lang decides, falling back to an English-stopword ratio over the visible text. Two deliberate non-rejections: Latin-script languages pass the metadata stage (ten words of French cannot be told from English reliably), and a page yielding no usable evidence is accepted rather than quietly thinning the pool — and Greek is left out of the non-Latin script set on purpose, since a lone alpha here is more likely to be mathematics than prose.

slop-audit spent the rest of the week being made presentable rather than more capable. A brush-up design split the work into Phase 1 (docs and packaging) and Phase 2 (hygiene), and Phase 1 followed: an MIT license, a changelog and pyproject.toml metadata (e7bc0a3) with the README polished and GitHub publication marked done (9b6a418), merged as PR #1.

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.

portcullis is a new public Python repository: one command creates a hardened Ubuntu 26.04 VM on Hetzner Cloud, and it drops the gate first — an unprivileged user with key-only SSH on a random high port, root locked, UFW default-deny and sysctl hardening, all inside about 30 seconds and using only what the stock image already ships — then switches the Hetzner firewall to the new port and deletes the temporary API key before the full CIS-style pass (package upgrades, AppArmor, auditd, AIDE, PAM policy, fail2ban, rkhunter, msmtp alerts, Docker and Podman) runs behind both firewalls. verify.sh then runs 58 checks on the finished host. Everything runs inside a Podman container so nothing is installed locally, and teardown deletes a half-provisioned server together with the keys and firewalls it created. The README was rebranded as the repository went public, with a GitHub Actions test workflow on actions/checkout@v5 and a logo.

The rank-trend arrows in forgepulse’s Repository signal table cost every row its bottom border alignment: display: flex on .rank-share, added to stack the arrow, pulled that <td> out of table layout, so it stopped growing to the row’s real height and stayed clipped to its own content while the Name column stretched normally for longer descriptions. Dropping the flex display and keeping the existing block-span stacking restores the alignment — two lines of CSS, which is what a change made to fit a two-character indicator should have cost in the first place.

The clone-trend arrows added to forgepulse two days ago were reading “stable” almost everywhere, and the cause was GitHub’s traffic API rather than the repositories: it reports a day’s row inconsistently per repository, so at any moment only a handful have a same-day daily_traffic entry while most lag behind, and a single fleet-wide “yesterday” cutoff therefore compares most repositories against data already included in their current total (762ea7b). The fix is to compare each repository’s clone total against one day before that repository’s own most recent row, computed in one query through a per-repository MAX(day), so the comparison never depends on a shared calendar date — verified live, the trends now show real up and down movement instead of universal stability.

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

pacenotch’s GUI grew the controls a .app cannot be handed on the command line: a Settings window (footer button, tray menu, pacenotch → Settings… on macOS) for the on-pace band, the refresh interval, notifications, compact mode, appearance and Dock behaviour, applied and saved as they change (13dc75f). Because a MacBook’s camera notch can hide the menu bar icon and with it the only Quit, the app can now switch to the Regular activation policy and live in the Dock and Cmd-Tab with a Quit in the window and a Settings window that is not hidden by the notch (b6f4031).

forgepulse’s Repository signal table now carries a Billboard-chart-style up / down / stable indicator on every row, in both ranking modes, showing whether a repository moved since yesterday (9306fec). It tracks rank rather than the raw figure on purpose: clone volume ranks by total_clones, a cumulative counter that only ever grows, so diffing the value would read “up” almost every day regardless of real trend, while rank stays relative and keeps meaning.

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

slop-audit is now public: a Python harness that scores a piece of prose for AI-slop and formulaic style, general writing issues and descriptive stats, and — kept strictly separate from all of it — local AI-authorship detector signals. Nothing leaves the machine: there are no hosted detector APIs and no remote LLM touching the target text, with the network used only for installs and optional model-weight downloads. A run produces a Slop Index (0–100 plus band) from the slop tools and linters (05e1527), deterministic edit suggestions quoted from the tools that would lower it — no LLM rewrite of the prose (7bcdcc3) — and a per-tool matrix reporting OK / NOT_RUN / ERROR with the exact reason, so a tool that failed never invents a score.

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.

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.

forgepulse grew the two controls its dashboard was missing: Refresh re-fetches the stored dashboard and detail data without touching GitHub at all, while Sync now performs a real pull through the existing POST /api/v1/sync endpoint outside the hourly schedule and now surfaces the server’s error inline — an expired token says so immediately instead of failing silently until the next scheduled attempt (87cfe54). On-demand sync then exposed a contention bug worth fixing properly: the scheduled tick and the new endpoint shared one GitHub collector with no coordination, so a click landing during the hourly run let multiple full 84-repo syncs proceed at once, each with its own bounded per-repo fetch — enough load to trip secondary rate limiting and queue on SQLite’s single writer, turning overlap into a crawl rather than an error. A single-flight guard now rejects the second sync instead of letting the two contend (47b2e73).

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

pacenotch is a new public Go repository: a CLI, tray icon and window for macOS, Windows and Linux that reports Claude’s usage windows (5-hour session, 7-day all models, and the 7-day Sonnet/Opus windows when the plan reports them) with a thin vertical notch drawn at the elapsed fraction of each window — the fill is past the notch when you are ahead of an even pace, short of it when there is room left, and the tray icon turns red on that side of the line (d7d6da6, 371aefc). The first day of commits also landed the usage/pace packages and terminal renderer with a compact mode below 60 columns, parity and coverage tooling, and a CI matrix with packaging and the README (b8f822a, b6c6151). The macOS build learned to raise its window in front of other apps and to reopen it when the running app is launched again (9f9aa5e, 6ca1263). MIT-licensed and unofficial — not affiliated with Anthropic.

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.

topshift-trend, the Telegram bot that watches GitHub’s monthly trending list, learned to suppress repositories it recently notified: a repo that drops out of the top-N and comes back used to announce itself to every subscriber again. The bot now keeps a notification_history.json alongside its state and subscribers, and the scheduled check filters out keys seen inside a configurable window — NOTIFICATION_COOLDOWN_DAYS, default 30 days, 0 disables the suppression. The commit touches the config, store and main loop plus three test files, and the check’s log line now reports how many entries were suppressed next to how many notifications actually went out.

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.

forgepulse shows the age of its own data: the homepage now reads the most recent successful sync run — already recorded in the sync_runs table but never surfaced — and renders it next to the git-ref pill as Updated <UTC> · <local> (Xh Ym ago), ticking every minute (d4c5e85). Traffic history is only as useful as the moment it was collected, and until now the dashboard gave no way to tell a stale snapshot from a fresh one. The change touches two new frontend modules plus tests for the relative-time formatter and the API field behind it.

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

portcullis hardens a fresh Ubuntu host, and hardening has to leave the machine pleasant to actually use: Ubuntu’s Vim defaults enable xterm mouse reporting, so on a remote terminal Vim captures the selection and ordinary copy/paste stops working. A new Phase 2 section, 1.6a — Terminal editor defaults, now ships /etc/vim/vimrc.local with set mouse= (and a note in the README’s Phase 2 list), leaving selection to the terminal emulator while anyone who wants Vim’s mouse support can opt back in.

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.

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.

dratify tagged v0.1.4 and v0.1.5 after an audit of its published numbers: the README’s speed table came from CNF files that are not in the repository, and its “~18x” was the top of a range quoted as the typical value. A committed benchmark script (bench/repro.py) now produces figures anyone can reproduce — a second run held the geometric mean at ~15x while individual ratios moved between 11x and 22x, so the release quotes the mean and states the spread as a spread. The same pass (c34c31b) added a fuzz workflow and stopped error messages from reporting version skew in the vocabulary of an unrelated project’s module.

cdclkit tagged v0.1.3: the release leads with the bug that mattered — --adaptive --self-check printed s UNSATISFIABLE while verifying nothing. Both engines now require dratify 0.1.4, with a test that fails if they ever ask for different versions again. The same pass rewrote the docs to describe the program (a fresh make test failed with 24 import errors while the Makefile still claimed no dependencies), and BENCHMARKS.md now says what the published 20.1x figure is a sample of: one run per instance, with individual ratios seen moving by a third between runs while the geometric mean held.

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.

dratify is tagged v0.1.3: the docs said the Python checker and the Rust checker were compared against DRATChecker on acceptances and rejections, but the only two tests that did so had silently skipped on every run — an import-time guard — so that claim had never once been exercised. The new differential suite (2889df3) sweeps 150 random instances plus hand-written accept/reject cases, and CI installs the native checker and fails if the tests skip. The same release hardens the untrusted-input paths: header counts like p cnf 99999999999 0 that would have asked for hundreds of gigabytes are rejected outright, register_native validates the checker it is handed instead of unpacking a fixed tuple, and proof parsing reports the offending line and token. Tests go from 87 to 96 and coverage 84% to 87%, with each new guard confirmed to fail when its fix is reverted.

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

forgepulse merged its first pull request, PR #1: human attention is now the default explainable ranking alongside clone volume. The dashboard persists fork history, collects release/tag and Actions-checkout signals, and shows each traffic diagnosis with its evidence inline. Clone-volume mode also gained sortable Stars/Views/Clones column headers (c69739b).

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

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.

kiwifarmit/cra-lab is now public — a small lab in the Kiwifarm org that builds the pipeline half of a Cyber Resilience Act story instead of describing it. Pull requests go through Semgrep SAST plus SCA and IaC scanning (Semgrep rather than CodeQL, which needs GitHub Advanced Security on private repos, and it runs entirely on the runner so the code never leaves it); a v* tag generates a CycloneDX SBOM with Syft, hashes it, hands the digest to the SLSA generic generator for provenance, and runs Trivy over the release SBOM at CRITICAL/HIGH before attaching it to the release (pr-security.yml, release-security.yml). A weekly Trivy and Semgrep sweep covers vulnerability, misconfiguration and licence scanning on a timer, and Dependabot keeps the actions the workflows themselves depend on pinned, with each workflow’s comments citing the CRA Annex I Part II clause it answers.

dratify’s release pipeline could report a successful release that published nothing: ci.yml triggers on branches and pull requests and never on tags, so no test ever ran against the ref being published, and combined with skip-existing a tag that forgot to bump the version built the old one, had PyPI skip it as already present, and exited green. The suite now runs on the tag, and the build fails when the tag does not name the version it produced — skip-existing should absorb a re-run of the same release, not disguise a forgotten bump.

caciarabot word-trigger responses now ship videos and GIFs alongside images, so the bot can reply with moving media instead of only stills. The update script also always restarts the bot now, so config-only changes actually land on the next deploy.

forgepulse hit its first tagged release, v0.1.0: the self-hosted GitHub traffic dashboard with retained clone and view history, repository analytics, charts, referrer and path snapshots, and JSONL export. The release note frames it explicitly as the baseline before the next feature — human attention ranking, which is already landing on the develop branch.

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.

forgepulse now highlights repositories whose clone counts sit above the fleet’s median, and the comparison was fixed to use each repo’s own daily median against the fleet’s rather than its raw total, so a busy repo can no longer skew its own marker.

Contributed to teorth/equational_theories a pull request correcting the paper’s section 5.1 brute-force counts: the two stated addends, 13,345,053 and 415,293, sum to 13,760,346 rather than the printed 13,632,566, and the “96.3% of the false ones” figure describes the first addend, not the total. The corrected numbers come from the project’s own All4x4Tables README, fixed earlier in #1335; the analysis is disclosed as AI-produced under human direction and reproducible from parsimagma.

dratify is a new public DRAT/DRUP proof checker that runs inside your Python process: zero dependencies, no subprocess, no compiler. It replays a solver’s derived-clause log to confirm the empty clause really follows, sharing no code with the solver that wrote the proof, and the same checker is published as a Rust crate. A register_native() seam lets the Rust engine (~18x faster) be supplied without shipping a toolchain, publishing is tokenless via Trusted Publishing, and the checker’s own tests went from 12 to 71 with a coverage gate.

cdclkit is a new public CDCL SAT solver, preprocessor and encoding library, written from scratch in readable Python with an optional Rust engine (roughly 18x faster) shipped as cdclkit-native. Every answer comes with a certificate: a satisfying model is re-evaluated clause by clause, and an UNSAT answer emits a DRAT proof that an independent checker replays. It publishes on PyPI with no third-party code, and the tutorial walks one problem end to end, from DIMACS through the files between stages.

parsimagma-greedy-cover is now public on the SAIR Contributor Network, entered into the Mathematics Distillation Challenge Stage 2. It is a deterministic refuter with no LLM calls: given two equational laws it finds a finite magma satisfying the first and violating the second, and emits a Lean 4 certificate the organisers’ judge accepts under plain decide. The point of publishing is the ordering rather than the score — four instances of Z/2 refute 11,871,871 of the ETP’s 13,855,357 false implications, twenty-five refute 97.2%, and x ◇ y = 7x + 7y over Z/13 alone refutes 268 pairs that Vampire’s fmb, Mace4 and z3 on a ground encoding all fail to find. The honest number is on the item: 55 of 200 on the graded distribution, zero on the true half by design, and zero on the extra_hard category, which is selected against exactly this method.

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.

Contributed to teorth/equational_theories an issue reporting that the 1,062 Vampire-unresolved implications are not uniformly hard: at least 411 of them have finite countermodels on 9 to 32 elements. The analysis is reproducible from parsimagma and disclosed in the issue as AI-produced under human direction.

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

caciarabot stopped tracking its live config: the working bot.jsonc is no longer in the repo, and a bot.jsonc.example ships instead, so local state can’t be clobbered by updates or leak into history. The daily thought generator also gained a real mood range and occasionally follows a Wikipedia rabbit hole instead of picking a templated topic.

forgepulse fixed two web-UI bugs: opening a repository detail page directly, or in a new tab, no longer 404s, and modifier-clicking a link now opens it in a new tab instead of swallowing the click. CI was retriggered after a GitHub Actions outage stalled the pipeline.

The pull request adding selectable daily clone statistics to hrodrig/gghstats was merged upstream: the “Unique” line on the clones-over-time chart and the compact daily clone panel are now part of the project.

forgepulse’s repository detail page now links its title, top referrers, and popular paths straight to GitHub (paths always, referrers only when they look like real hostnames), and the JSONL export filename embeds a UTC timestamp so re-downloads stop silently overwriting the previous file. A cross-check against the issues opened on hrodrig/gghstats found that three of them applied to forgepulse too — the export filename, the stats-panel jargon, and the rank column header — and were fixed here; the locale-formatting issue does not apply in the same shape yet.

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.

forgepulse got its launch-week pass: the repository table is paginated, a favicon landed, and the static “LOCAL” badge now shows the running git ref. On the ops side, a scheduled sync that was silently failing (the /data volume was never chowned to the app user) and a repository detail page that replayed every historical referrer day are fixed, and the production container now restarts itself after a crash or reboot.

solids-hunter, the first-person Babylon.js game where you hunt solids defined by boolean rules, is in pre-release polish: full gamepad menu control, a working HUD speaker, spawn facing derived from the room, and rule complexity that ramps with each clear. A pre-release review surfaced five launch blockers, now fixed, gameplay screenshots landed in the README, and the shadow-pass watchdog now halves its cadence and can shed shadows entirely when quality is at risk.

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.

forgepulse is now public: a self-hosted GitHub traffic-history analytics app built with Rust, a Svelte frontend, SQLite for storage, and Podman for deployment. It keeps a running history of GitHub traffic metrics so trends accumulate instead of vanishing after GitHub’s rolling window.

caciarabot grew a Phase 3 admin surface: /sleep, /wake, /categories, /stats, and /reload let moderators pause the bot, inspect its categories, and reload state without touching the container. Two reply bugs were also fixed — a cited reply and a word-trigger image can now fire together, and the LLM prompt no longer drifts into recurring ants/insects imagery.

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.

Contributed to hrodrig/gghstats with a pull request that adds selectable daily clone statistics to the repository index: a second “Unique” line on the clones-over-time chart with its legend enabled, plus a compact daily clone panel. The change makes unique cloners visible alongside total clone events.

dash parses DMARC aggregate reports in a serverless setup for Gmail: it extracts and parses incoming reports, enriches the failing sources, and emails a summary of which senders are failing DMARC and why. The repo is public and actively developed.

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.

cross-tetris is a new game: four standard Tetris wells arranged in a cross, sharing a single piece stream. You — or a greedy rule-based AI — pick which well each piece falls into, the wells play out as ordinary real-time Tetris, and the game ends when any well tops out. The engine is Rust compiled to WASM with a React UI, and it is playable live.

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.

cold-path-server-podman is a new repository that runs the Cold Path multiplayer game server inside a Podman container, so no LuaJIT, LuaSocket, or LuaSec install is needed on the host. The upstream sources aren’t vendored — the image build pulls them from GitHub, and make build / make run / make logs handle the rest.

spriter is a new browser-only tool that turns a raster image into a pixel-art sprite. There’s no upload, no build step, and no dependencies — the whole conversion happens locally in the browser.

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.

caciarabot is a new self-hosted, reactive Telegram group bot designed Italian-first. It runs on your own infrastructure rather than a hosted service, and it reacts to group activity rather than only to explicit commands.

This blog is a running, public log of activity across my GitHub repositories.