Blog

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.

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.

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.