#project

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

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.

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.

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.

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.

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.

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.

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

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

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.

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

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

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.

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.

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

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

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

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

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.