Principia
A section for mathematics and physics. Chiefly a record of working on unsolved problems of mathematics — for each problem: what it is, how far the world has come, what was measured on this machine, and what remains.
This index falls into four parts. The articles by problem — each of them separating what the problem is / how far the world has come / what was done / what remains. Then spacetime and dimension — not unsolved problems, but the side of physics and geometry. Then what can be said across the problems, and how the work is done. Finally what remains, and machine checking — where the open items at the end of each article now stand, and the list of machine-checked claims.
Claims carry one of four labels. Leanmachine-checked paperproved, not yet machine-checked computationchecked on this machine, within the range stated knowna known theorem or a restatement. Nothing here is called a first — the most that is said is "not found in the literature searched".
The articles by problem
| The Collatz conjecture | 3n+1 is the only exactly critical map of this form. There are four articles on this problem, and this is the entrance
|
| The Riemann hypothesis | The explicit formula run both ways — building the staircase of primes from the zeros, and recovering the height of the zeros from the primes. And Λ = 0 exactly, which is to say no slack at all
|
| The Erdős conjecture on arithmetic progressions | The record 3.0085385 for k=3 and the record 4.4397535 for k=4 are each a single machine-checked theorem
|
| The BSD conjecture | |Ш| agreeing to thirteen decimal places across ranks 0–7, with the record of turning the verification of curve labels into a mechanism |
| The Lovász conjecture | Four exceptions. The search space for a fifth splits three ways by the deficiency def
|
| The Hadwiger–Nelson problem | f(α), the largest unit-distance graph with independence number at most α: f(3) = 10, and f(4) is 14 or 15 |
| Drawing unsolved problems at random | A record of the smaller problems — Sierpiński numbers, Riesel numbers, distinct distances |
Spacetime and dimension
| One sign is different | Time is not a fourth axis; it is one sign that differs in a quadratic form. Five measured consequences of that |
| The world is zero | Four pages of notes from 2002, written from E=mc² alone. The exponential formula agrees with the Schwarzschild solution to third order, and the places where it breaks can be named |
| What happens only in four dimensions | A casebook for Euclidean ℝ⁴. Not an unsolved problem, but a tool for seeing — and a different thing from the four dimensions of spacetime treated in the two articles above |
Across the problems, and how the work is done
| Problems remain only at the exact edge | The cross-cutting piece. Line up the long-unsolved problems and every one of them sits at strict criticality, which is not a coincidence but the result of selection. What can be proved is always only the "no slack" side |
| A map of the walls | For each problem, what is out of reach. Walls that closed are marked closed |
| Taking stock of novelty | The results sorted under four labels — closed in Lean, proved on paper, closed by computation, restatements of known facts. With theorem names |
What remains, and machine checking
| What remains | Where the open items at the end of each article now stand — closed / changed shape / open as first posed |
| The Lean verification bundle | The list of machine-checked claims. The bundle, the ledger of theorems, and how to check them |