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 Only 3n+1 is exactly critical — criticality as a whole, the distribution of the overshoot (five digits of agreement with measurement), the boundary that can be counted exactly, the lower bound on cycles What the sign of 1/3 decides — the sign of the asymmetry is fixed by 3³ < 2⁵ That constant is not yet a constant — the limit has a closed form; the value at each depth does not. The oscillation is a sawtooth built from the continued fraction of log₂3
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 How far the published logs alone reach — Λ ≤ 0.19 follows from Polymath15's public logs alone (no novelty). What remains is nine discrepancies in the manuscript Sunk eigenvalues of the Weil quadratic form — the Weil form with compactly supported test functions has about e^2L − 7/8 eigenvalues sunk almost to zero; their number gets a lower bound that does not assume the Riemann hypothesis. None of it can prove or disprove the hypothesis
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
Yang–Mills and the mass gap	A textbook-scale exposition (Parts 0–11 and appendices, 124 chapters). From reading the problem statement word by word, through the difference between two or three dimensions and four, the lattice, constructive field theory, the view from physics and a dictionary of the two languages, to where things stand and the study on this machine
The Hodge conjecture	On CM abelian varieties the Hodge classes reduce to finite combinatorics. At the smallest place where the exceptional classes leave the Weil classes, the problem comes down to a single Hodge class of codimension 2. Also the threshold t₃ of a model of the secant-sheaf type, and a reproduction of the walls on Fermat varieties. No algebraicity is proved
P versus NP	Where the ladder of negations stops — the price of 1 negation is half the correlation margin, the ceiling n^−1/2 is a matter of principle, and the window that cannot be reached has width log log N. No claim is machine-checked. Continued in Formula size as a function on truth tables
The Lovász conjecture	Four exceptions. The search space for a fifth splits three ways by the deficiency def Certificates: Hamilton cycles in HGL₄(F₄) and SGL₆(F₂) — the cycles themselves and verifiers that use only the Python standard library
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
Four points with distinct circumradii	Seven points in general position always contain four whose four circumradii are pairwise different; six do not. The whole chain is checked in Lean
Drawing unsolved problems at random	A record of the smaller problems — Sierpiński numbers, Riesel numbers, distinct distances, and five small records (#1087, #104, #99, #40, #30)

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
How the work is done	How problems are drawn, when to move on, the discipline of checking, and the bar for what is stated in public
The ledger of claims	What has been established, one line each — label, theorem name, whether it was known, and the article

What remains, and machine checking

The Lean verification bundle	The list of machine-checked claims. The bundle, the ledger of theorems, and how to check them
The Lean guide	What it means for a machine to check a proof. Where Lean comes from, how to start, how small examples are written, and “it passed — but does it say what you meant?” — 13 chapters
Papers	Where the drafts of the papers are kept. Six abstracts, grades, what each claims and does not claim, LaTeX sources
Archive	Pages removed from the index but kept — dated snapshots, and a line of argument that was withdrawn