Taking stock of novelty — the results sorted under four labels
A list of what the Principia articles claim, sorted by how far each claim has been verified. There are four labels, weakening from top to bottom. On "novelty against the world", no line says more than "not found in the literature searched".
closed in Lean14 groupsLean 4 + mathlib. Standard axioms only, no
sorryAx, no native_decidepaper proofs8proved, not yet machine-checked
closed by computation10checked on this machine, within the range stated. Not put forward as claims
known / restatementsmanyrediscoveries of known theorems, literature status, corrections to the articles
Contents
yardstick
The yardstick — four labels
| Lean | Machine-checked in Lean 4 + mathlib. #print axioms returns no more than the three standard axioms (propext / Classical.choice / Quot.sound), with no sorryAx (unproved hole) and no Lean.ofReduceBool (native_decide). The label is given only where the axiom output is in the ledger. Where the source exists but the output is not yet in the ledger, the entry says "axiom log pending" |
| paper | Proved, but not yet machine-checked. Whenever the word "theorem" is used, this label goes with it |
| computation | Closed by exhaustive enumeration, SAT or interval arithmetic. Written as "checked on this machine, within the range stated", and not put forward as a claim |
| known | A restatement or rediscovery of a known theorem, a check of the literature, or a correction to an article. Not new mathematics |
What a machine check does not guarantee
A machine check guarantees only that the conclusion follows from the proposition as written. Three things it does not guarantee: (1) that the proposition says what was intended — whether the definition of "contains no 3-AP" really says that is for a person to judge; (2) that the proposition is new — a matter of literature search, on which the machine says nothing; (3) that the object of comparison is read correctly — whether the "3.00849" of a 1984 paper is truncated or rounded, and for which set.
01
Statements closed in Lean
Theorem names are the names in the Lean sources. The column "axiom output" gives the state of the ledger.
| Problem | Statement | Theorem | Axiom output |
|---|---|---|---|
| Collatz | The multiplier 3 of 3n+1 is the only exactly critical one among maps of this form (the critical multiplier is an integer only for 3) | Shiori.qcrit_eq_three, qcrit_not_int_of_three_le | in the ledger (bundle) |
| Collatz | Sign conjugation of the Syracuse map, the minimum over six residue classes, the necessary rate, failure of the c=3 pattern | Shiori702.syracuse_sign_conjugation, Shiori737.min_over_six_classes, Shiori716.necessary_rate, Shiori751.c_three_pattern_fails | in the ledger (bundle) |
| Collatz | In the model ek+1 − ek = vk+1 − gk (assuming only v ≥ 1), three consecutive descents never occur (ek+3 − ek ≥ −2) and the asymmetry (3·log₂3 − 5)/4 is negative. Both from 3³ < 2⁵ | Collatz1139.no_three_consecutive_descents, eK_three_step_lower, asymmetry_negative, three_cA_lt_five | axiom log pending |
| #169 (k=3) | A finite set with no 3-term arithmetic progression whose reciprocal sum exceeds 3.0085385 (84 levels, window-separated Bellman). Exceeds the 1984 record 3.00849 | Shiori959.erdos169_lower_record_939, setA939_apfree_and_lower, Shiori939.setA939_lower | in the ledger (bundle) |
| #169 (k=3) | The 100-level set is 3-AP-free and beats the record; the union lemma for window separation; Wróblewski's Lemma 1 | Shiori844.setA_apfree_and_beats_record, Shiori712.apfree_iUnion_of_separated, Shiori730.lemma1_nonaveraging and the other headline theorems (20) | in the ledger (bundle) |
| #169 (k=4) | A finite set with no 4-term arithmetic progression whose reciprocal sum exceeds 4.439753369254541 (the reciprocal sum of Walker's 2025 record set, rounded up at 15 digits). Lower bound 4.439753474215620 | Shiori1112.setA4_apfree_and_beats_walker, setA4_apfree_and_lower | present (15 declarations); also in the certificate store |
| #169 (k=4) | The nesting lemma for k-AP-free sets (the general-k form of Wróblewski's Lemma 2); Walker's Theorem 1.2 (if the digit set contains no k-AP mod b then K(S,b)+1 is k-AP-free) | Shiori1109.core_strong, lemma2_four, Shiori1112.KSet55_apfree | present (15 declarations); also in the certificate store |
| Lovász (nearby) | Cubic bipartite graphs on 30 vertices that are connected, have a cycle of length 28, have no cycle longer than 28, and are not Hamiltonian (deficiency def = 2). Three isomorphism classes | Shiori1161.G30_def2 / Shiori1193.G30b_def2, G30c_def2 | present (14 and 20 declarations) |
| Lovász (nearby) | A connected cubic bipartite graph on 20 vertices with circumference 14, not Hamiltonian | Shiori1193.G20_def6 | present (20 declarations) |
| Lovász (nearby) | The number of Hamiltonian cycles of the generalised Petersen graph GP(n,3) is 7, 9, 11, 26, 75 for n = 7, 9, 11, 13, 15, and is divisible by n | Shiori1168.GP{7,9,11,13,15}_hc_card, card_dvd_of_perm_free, Shiori1173.GP{n}_dvd_rot, gp{7,13,15}_dvd_by_rotation | present (21 and 24 declarations) |
| Lovász (nearby) | For every odd n ≥ 7, the number of Hamiltonian cycles of GP(n,3) is divisible by n. No hypothesis. The parts: the rotation automorphism, winding numbers, block structure, the sign of a permutation, the local structure of the darts of a cycle, the first-return map | Shiori1202.gp3_dvd_hc_odd, Shiori1195.*, Shiori1197.*, Shiori1199.*, Shiori1202.* | present (41, 42, 30 and 30 declarations) |
| Hadwiger–Nelson | There is a unit-distance graph on 10 vertices with independence number ≤ 3, and one on 14 vertices with independence number ≤ 4 (Moser ⊔ K₃, Moser ⊔ Moser). In general f(2k) ≥ 7k and f(2k+1) ≥ 7k+3 | Shiori1183.fGe_10_3, fGe_14_4, Shiori1192.hn_lower_family, indepNum_sum, fGe_add | present (23 and 31 declarations) |
| Hadwiger–Nelson | The 117 candidate edge sets on 11 vertices and the 2,100 on 16 vertices are not realisable as unit-distance graphs in the plane (non-realisability certificates) | Shiori1178.hn11_no_realiz, Shiori1185.hn16_no_realiz | present (26 and 27 declarations) |
| Hadwiger–Nelson | The 296 + 103 ten-vertex subgraphs discarded by the 16-vertex enumeration are not realisable. The trilateration core (a linear identity in which the square root disappears) and the box bound | Shiori1189.hn10_no_realiz, hn10_no_realiz2, Shiori1178.trilat_core, lam_box | present (22 declarations) |
What stays outside Lean is fixed line by line — for k=4, the value of the reciprocal sum of Walker's set itself and the equality "head = truncation"; for def = 2, minimality and "exactly three classes"; for Hadwiger–Nelson, the completeness of the enumeration. These sit under computation or paper below.
02
Theorems with a paper proof
| Problem | Statement | Status |
|---|---|---|
| Collatz | The stopping-time tail theorem. For E(k) = #{r mod 2k : stopping time > k} (OEIS A076227) and uk = E(k)/2k: uk ρ−k k3/2 = A(θk) + o(1). A is 1-periodic with mean 10.892710 and relative amplitude 7.59 %; ρ = 0.9659065532. The Fourier coefficients have a closed form | paper Vatutin–Wachtel 2009, Theorem 6, with Cramér tilting; the Sparre Andersen identity checked in rationals for k ≤ 60. That the prefactor oscillates on a non-centred lattice is known in general; what is added is the closed form and the application to this sequence |
| Lovász | Truncation freezes after one generation. T(G) is Hamiltonian ⟺ G is. T²(G) is never vertex-transitive. A truncation-type fifth exception does not exist up to 3,840 vertices | paper |
| Lovász (nearby) | An edge-transitive d-regular graph has edge-connectivity d. If Aut has two vertex orbits, the deficiency graph of a def = 2 graph is spanning, regular, of size ≥ n/2. Corollary: a semisymmetric graph with def = 2 has n ≥ 50 if cubic and n ≥ 26 if tetravalent | paper Cubic semisymmetric graphs on fewer than 3,000 vertices are Hamiltonian (arXiv:2602.14388), so the cubic case is subsumed by the census |
| Lovász (nearby) | The 2-edge-cut decomposition of def = 2 graphs extends to all degrees d ≥ 3. Bipartite local lemma: n ≥ 4d, and n ≥ 6d − 4 if the girth is ≥ 6 (equality for Heawood) | paper |
| #169 | The prefix cut. If a Kempner-type set A = {1..J} ∪ (K(S,b)+J+1) has reciprocal sum at least the record 13.5332472, then |S ∩ [0,v₀]| ≥ mreq(v₀) for every v₀. The record enters only as a lower bound, so the conclusion survives any later improvement | paper |
| #169 | The inductive step of the cyclotomic proposition. If S is 3-AP-free, (1+xc) ∣ PS and 3c > D, then S = {0,c} ⊕ S′ with S′ 3-AP-free and PS′ cyclotomic. The escalation lemma EL implies the whole proposition | paper The local argument stops at c > D/3 (there are genuine direct sums with c ≤ D/3) |
| #563 | β(n,m) ≥ k ⟺ n < R(𝒢m,k). With Pα(m) := R(𝒢m,⌊αC(m,2)⌋+1), F(n,α) ~ cα log n ⟺ Pα(m)1/m → e1/cα. The case α = 0 is exactly #77. Supermultiplicativity fails; lexicographic products are ineffective for α ≥ 1/3; XOR-type products are ineffective | paper A restatement of the quasi-Ramsey numbers of Erdős–Pach 1983 |
| Hadwiger–Nelson | α ≤ 2 forces at most 7 vertices and α ≤ 3 at most 12 (comparison of the minimum edge count with u(m)) | paper Later sharpened to 11 and 10 in Lean |
03
Facts closed by computation
Checked on this machine, within the range stated. Not put forward as claims.
| Problem | Fact |
|---|---|
| Hadwiger–Nelson | Completeness of the candidate enumerations behind f(3) ≤ 10 and f(4) ≤ 15 (ω ≤ 3, K2,3-free, the u(m) test, minimum degree, isomorphism rejection) / f(5) ≤ 24 |
| Lovász (nearby) | The smallest connected cubic bipartite graph with def = 2 has 30 vertices, and there are exactly three classes on 30 / the smallest non-Hamiltonian connected cubic bipartite graph has 20 vertices and is unique up to isomorphism / no tetravalent bipartite graph with def = 2 on n ≤ 24 (all 4,623 tetravalent bipartite vertex-transitive graphs on n ≤ 40 are Hamiltonian) / the known non-Hamiltonian cubic bipartite graphs EH54, EH78 and Horton96 all have def = 2 |
| #169 | For k = 8, Kempner-type sets stay at or below the record 13.5332472 for every base b ≤ 200 except b = 121 / the record values for k = 5, 7, 8, 9: 7.8723049, 13.5905274, 13.5332472, 13.5637722 / the head for k = 4 is closed under product constructions with b ≤ 1000 / the cyclotomic proposition has no counterexample for deg ≤ 52 (67,236 sets) |
| Ramsey | ω(P₇₉₇) = 9 (the source of R(10,10) ≥ 798) / R(9,9) ≥ 565 cannot be improved with Paley graphs |
04
Known, restated, or settled elsewhere in the literature
| Problem | Content |
|---|---|
| Collatz | The model behind the sign of 1/3 is a restatement of standard ingredients (Terras's distribution, Sturmian words); what is added is only that the sign and the forbidden word come from the same inequality, and the flip point 25/3 / that the stopping-time prefactor oscillates is in the general theory of Vatutin–Wachtel and Mogulski–Rogozin / the closed form of C was already known; the description of the eigenstructure is added |
| Riemann | The first-order perturbation of the zeros in the Hurwitz family, dρ/da = ρζ(ρ+1)/ζ′(ρ), is elementary / Re ζ′(ρ) > 0 ⟺ |S(γ)| < 1/2 is a known identity (arXiv:2305.14253) / the 1/12 seen in statistics over the zeros is an identity unrelated to ζ — statistics over the zeros must first be tested against a point process that does not use ζ, or an identity is mistaken for a discovery |
| Lovász | The deficiency def has a name, the perimeter gap (Alspach 1981) / the conjecture "no vertex-transitive graph has def = 2" contains Grünbaum's 1974 conjecture / the three truncation theorems are known |
| #169 | The literature value 7.866 for k = 5 (as quoted from GR79) differs in the third decimal; H(G₅) = 7.8723049 / the route "replace the head of f(3)" is a restatement of improving the record / Elkin's factor is Θ(√log n) |
| #563 | The same quantity as the quasi-Ramsey numbers R̄c(k) of Erdős–Pach 1983 (c = 1 − α). The case α = 0 is #77 |
| Hadwiger–Nelson | Finite unit-distance graphs with n/α > 4 are known (Dúcz–Varga, arXiv:2606.28157); what is left is the exact value of f(α) / the unit vectors of the Moser spindle's field ℚ(√3,√11) span only 9 directions and are 4-colourable (de Grey's construction lies outside the rank-4 group) |
| Settled elsewhere | #138: Campos–Fox–Schildkraut (arXiv:2608.20824) prove w(k) ≥ (1−o(1))k2k−1 / #634: Beeson (arXiv:2607.23453) — dissection into a prime number of congruent pieces is impossible apart from listed exceptions / #165: DJPR (arXiv:1606.01043) Conjecture 2 ⟹ R(3,k) ≤ (1/2+o(1))k²/log k, with the lower bound of HHKP (arXiv:2510.19718) / #52: BSSZ (arXiv:2605.28781) construct real A with max(|A+A|,|AA|) ≤ |A|2−c / #143: KLL25 (arXiv:2502.09539) prove Σ1/x = o(log n) / #30: the reduction to prime gaps is formalised in Lean 4 (arXiv:2605.03274) |
05
What can be said about novelty
Every line stops at "not found in the literature searched". Here is what was searched.
| Statement | What was searched, and what was not found |
|---|---|
| The records for k=3 and k=4 (3.0085385, 4.4397535) | Nine lines of primary sources and Walker's 2025 table. No value above 3.00849 or above 4.43975 was found. Not yet examined by a third party |
| n odd, n ≥ 7 ⟹ n ∣ #HC(GP(n,3)) | OEIS has neither the sequence #HC(GP(n,3)) nor #HC/n. arXiv:2503.08326 gives the values by a linear recurrence, not the classification. Not confirmed in print. The use of Burnside's lemma is standard and may be obvious to specialists |
| Smallest cubic bipartite graph with def = 2 has 30 vertices | Twenty searches and the Web turned up no paper asking for the smallest order with def = 2. Not yet compared with the House of Graphs. Known values: smallest 3-connected is 50, smallest 2-connected planar is 26 |
| f(3) = 10, f(4) ∈ {14, 15} | Not found in print in the range searched. May be obvious to specialists |
| The closed form of the stopping-time tail | The general theory (oscillating prefactor) is known. The closed form and its application to A076227 were not found |
| The cyclotomic proposition (3-AP-free sets and direct-sum decomposition) | Closest: de Bruijn 1950/53, Billey–Swanson (arXiv:2305.07620), Filaseta–Kalogirou (arXiv:2508.12242). The same statement was not found. The proof is incomplete |
06
What this article can claim
| Content | |
|---|---|
| Claimed | Each line of §01: that the conclusion follows from the proposition as written, in the Lean kernel. The axiom outputs are in the ledger |
| Not claimed | No unsolved problem has moved. The records for k=3 and k=4 do not touch the conjecture itself |
| Not claimed | "New to the world" is not written of any line. Outside the range of §05 nothing was searched (MathSciNet, zbMATH, conference proceedings, non-English literature) |