Mathematical plates that draw themselves — prime counts, orbits and lattices rendered live rather than shipped as pictures. It runs continuously while on screen, and it pauses on its own whenever it scrolls out of view.
We measured it rather than guessing: the largest frame-to-frame change in average brightness is 0.26%, and it produces zero flashes per second against the threshold of three set by WCAG 2.3.1. That is well under the limit, and it is not a promise about any individual: if moving images are a problem for you, you should not have to assess ours.
Everything animated on this site honours your system’s reduce motion setting — turn it on in your operating system or browser and these pages stop moving, with nothing else lost. All the mathematics is in the text and the still figures.
Everything we have put on the public record, with the DOI or the archive record that resolves to it. The list of record is the ORCID entry 0009-0005-4048-1237, not this page: if the two ever disagree, ORCID is right and this has gone stale.
None of these has been peer-reviewed. A Zenodo deposit is a public, dated, citable record of what was claimed and when. A Lax Lean Archive record adds one thing a deposit lacks — the archive rebuilt every proof with Lean’s kernel before registering it — but it is still not a referee. A pull request to Mathlib is under review and accepted only when it is merged. None of the three is a second opinion, and we would rather say so at the top than have it inferred from the absence of a journal name.
Version 2, deposited the same day, corrects how many seeds the census evolves: the 51,472 whose bounding box is exactly 4×4, not every one of the 65,535 patterns of the box as the first version said. The code, the data and the Lean proofs are open at github.com/joelcanary/life-like-rule-b37s2378.
A corrected version follows: the first release described its five Lean 4 theorems as “kernel-checked” when they are closed by native_decide, which trusts the compiler rather than the proof kernel.
The landscape in the strip at the foot of every page on this site is M(n), the Mertens function this paper is about.
The Kodama Observable for Collatz Dynamics: Exact Decomposition, Residual Dynamics and Experimental Evidence up to 10^8 (10.5281/zenodo.21087140) was deposited and then retracted by its author on 6 July 2026. The DOI now resolves to a Zenodo tombstone rather than a paper.
It is still on the ORCID record, so it is on this page too. A withdrawal only the person who made it can see is not a withdrawal, it is a deletion — and pulling a preprint you no longer stand behind is the system working rather than a blemish to tidy away. The same reasoning puts our refuted findings in the registry instead of the bin.
A preprint is a claim with a date. These are something else: each is a set of statements in Lean 4, with the natural-language meaning beside the formal one, whose proofs the archive rebuilt on its own machines against a pinned Mathlib before recording them. The counts below are read from the archive’s own build output, not typed. A record is immutable once registered; a correction would be a new record that supersedes it.
AnnotatorCeiling 2/2 · Candidate 4/4 · Duplication 3/3 · Matching 3/3 · Removal 4/4 · WeightedFamily 6/6
EulerCharacteristic 1/1 · GeometricGenus 4/4 · LinearSubspaceClass 1/1 · NoetherLefschetzWindow 4/4 · Parity 4/4
Involution 1/1 · QuadraticTwist 1/1 · TunnellParity 1/1
LcmDeterminant 3/3
How the second record started. For a smooth surface of degree d in P³ the codimension of a Noether–Lefschetz component lies between d − 3 and pg = C(d−1, 3). Someone computed the gap for d up to 200 and noticed it was the OEIS sequence A005581 shifted by three. The figure redoes that computation in exact integers: the two bounds on a log scale, the gap as dots, A005581(d−3) as the thin line through them, and the count of agreements. What the computation could never say is “for every d”; the record says it, as the identity (d−1)(d−2)(d−3) − 6(d−3) = (d−4)(d−3)(d+1), checked by the Lean kernel.
For the congruent-number curve En : y² = x³ − n²x and a prime p, the trace of Frobenius ap measures how far the number of points over the field with p elements strays from p + 1. Each dot below is one prime up to 1500, and its ap is summed in your browser from Legendre symbols when the figure starts — there is no table behind it.
Proved: every prime p ≡ 3 (mod 4) that does not divide 2n lands exactly on zero, for every n — the dark dots on the axis. That is Deuring’s theorem for these curves, checked by the Lean 4 kernel with Mathlib, with no hypothesis left unproved; the reason fits in a line (x ↦ −x permutes the field, x³ − n²x is odd, and −1 is not a square there, so the sum equals its own negative). Switching n flips the other dots by the Legendre symbol (n/p): the quadratic twist, also proved in Lean. The general step, for any odd function over any finite field where −1 is not a square, is under review as a pull request to Mathlib, listed below.
Shown, not proved here: the grey dots, the primes p ≡ 1 (mod 4), never land on zero, and none leaves the shaded band |ap| ≤ 2√p. Both are classical theorems (Hasse’s bound, and the complex multiplication of these curves); the figure displays them and the site’s tests check them for every prime drawn, but they are not among the results proved in Lean. Primes that divide n are left out: there the curve is singular, and the sum vanishes for a trivial reason that has nothing to do with the theorem. And the picture looks the same whether or not n is a congruent number (5, 6 and 7 are; 1, 2 and 3 are not): this is local information, prime by prime, and whether n is congruent is a global question that it cannot settle.
Mathlib is the community library that the Lax records above are checked against. Getting a result into it is the opposite of depositing a preprint: other people decide, and they decide slowly and in public. These five are open on GitHub, two of them stacked, each building on the one before, and every one carries Mathlib’s LLM-generated label because an AI tool wrote the Lean under our direction and we said so. An open pull request is a submission under review, not a result the community has taken in. The state, labels and CI on each line are read from GitHub a few times a day by a scheduled job, not typed here; the badge turns green only when the pull request is merged. If the job stops, the line says when it last looked, and the pull request itself is the truth.
For a multiplicative f, the product over the prime factors of n of (1 − f(p)) equals the Möbius-weighted sum of f over the divisors of n — for every n ≠ 0, dropping the squarefree hypothesis Mathlib had.
The Redheffer matrix over any commutative ring: its determinant is the Mertens function M(n) — the identity behind the landscape at the foot of every page here.
The zeta matrix (aij = 1 if i divides j) is invertible over any commutative ring, and its inverse is the Möbius matrix.
Smith’s determinant: det[gcd(i, j)] over the first n integers equals the product of φ(1)…φ(n), again over any commutative ring.
Over a finite field in which −1 is not a square, the quadratic character summed along an odd function is zero — the step at the heart of Deuring’s theorem that the congruent-number curves have trace zero at every prime p ≡ 3 (mod 4).
A publications page lists what went on the record, which invites you to assume that is the whole picture. Here it is not: most of what has been proved has never been written up. The list below is generated from the same registry that feeds /challenges, not typed here, and it will get shorter or longer on its own.
Loading the registry…
For a machine-checked statement, cite its Lax record (\cite{lax-303562} and so on): the archive resolves the id to the exact statement and proof, and the record cannot change under the citation. For everything else, cite the DOI rather than this page — it resolves whatever happens to our hosting. If you are citing a specific result rather than a whole paper, the findings registry gives each one an identifier and an evidence level, and the level is part of the claim: P-Lean, P, V, H and X are five different strengths of statement and quoting one without the other loses the half that matters.
Author: Joel Cruz Cabrera, ORCID 0009-0005-4048-1237. Work carried out at KodamaSEC Labs Ltd.