Blog

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

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

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

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

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

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

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.

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.

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

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.

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.

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.