The ledger of claims
A list, one line each, of what the Principia articles have been able to say. Each line carries how far it has been checked (the label), the theorem name for anything closed in Lean, its relation to the literature, and the article where it is written up in detail. When the status of a claim changes, its line is rewritten.
Leanmachine-checked (Lean 4 + mathlib, within the three standard axioms, no sorryAx or native_decide)
paperproved, not yet machine-checked
computationchecked on this machine, within the range stated. Not made a claim that is put forward
knowna known theorem, a restatement, or a confirmation of outside literature
The literature column takes three values. Known = in the literature (or a restatement of a known result). Not found = no statement of the same form was found in the literature searched (the range searched is given in each article). Weaker = weaker than a known result. "—" marks lines not yet compared against the literature. In the theorem name column, "part" means that only some steps of the paper proof are closed in Lean — not the claim as a whole. The criteria for the labels, and the thinking behind which claims are put forward, are in How the work is done.
By problem
01
The Collatz conjecture
| Claim | Label | Theorem name | Literature | Article |
|---|---|---|---|---|
| The multiplier 3 of 3n+1 is the only "exactly critical" one among maps of this form (3 is the only multiplier whose critical value is an integer) | Lean | Collatz.CriticalMultiplier.qcrit_eq_three, Collatz.CriticalMultiplier.qcrit_not_int_of_three_le | — | Only 3n+1 is exactly critical |
| Sign conjugation of the Syracuse map: if 3m − 1 = 2ar then 3(−m) + 1 = 2a(−r). The two maps are conjugate by n ↦ −n | Lean | Collatz.LadderHeight.syracuse_sign_conjugation | Known | The Collatz conjecture |
| Among the six unit classes, the 3-adic limit measure has its minimum at class 7 mod 9 (the minimum is at the point that doubles to the maximum) | Lean | Collatz.LambdaMeasure.lam_seven_min, Collatz.SubtractionSteps.min_over_six_classes (under the doubling relations among the six classes and the assumption m₇ ≤ m₄) | Known (the mod 9 level is in a primary source) | The Collatz conjecture |
| The probabilistic supermartingale line is closed by the cycles of 3n−1 (of lengths 2 and 7): the same computation reaches a false conclusion for 3n−1 | paper | — | Only 3n+1 is exactly critical | |
| In the model ek+1 − ek = vk+1 − gk (assuming only v ≥ 1), there are never three descents in a row, and the asymmetry A = (3·log₂3 − 5)/4 is negative. Both follow from 3³ < 2⁵ | Lean | Collatz.no_three_consecutive_descents, Collatz.eK_three_step_lower, Collatz.asymmetry_negative, Collatz.three_cA_lt_five | The parts (Terras's distribution, Sturmian words) are known. That the sign and the forbidden word come from the same inequality was not found | What the sign of 1/3 decides |
| The tail of the stopping time: ukρ−kk3/2 = A({ak}) + o(1). A has period 1, mean 10.892710 and amplitude 7.59%, and its Fourier coefficients have a closed form | paper | Oscillation of the prefactor is known in general. The closed form, and its application to this sequence, were not found | The Collatz conjecture | |
| The constant C = q²p/(ln2·(log₂3 − 4/3)) = 0.4215205965. The limit has a closed form; the value at each depth does not | paper | Known (the closed form has appeared before. A description of the eigenstructure was added) | That constant is not yet a constant | |
| The oscillation of C is a superposition of sawtooth modes indexed by the convergent denominators of log₂3. The transfer operator has largest eigenvalue exactly 1/2, and no spectral gap | paper | — | That constant is not yet a constant |
02
The Riemann hypothesis
No line here says anything about the Riemann hypothesis itself.
| Claim | Label | Theorem name | Literature | Article |
|---|---|---|---|---|
| The explicit formula run both ways — the staircase of primes from the zeros, and the height of the zeros from the primes. Λ = 0 exactly, which is to say no slack at all | known | Known | The Riemann hypothesis | |
| Λ ≤ 0.19 follows from Polymath15's public logs alone | computation | Known | How far the published logs alone reach | |
| The coefficients λn of Li's criterion are reproduced to within 0.75% at n = 199 even by a synthetic sequence of zeros built from the zero-counting function alone (the margin does not test the arithmetic) | computation | Not found | Sunk eigenvalues of the Weil quadratic form | |
| The Weil quadratic form passes the same test: merely rearranging the values of Λ(k) onto other prime powers, keeping their multiset, drops the smallest eigenvalue to ≈ −20 (L = 2, 3, 4; 12 out of 12 randomisations) | computation | Not found | Sunk eigenvalues of the Weil quadratic form | |
| Theorem A: a lower bound on the number of eigenvalues sunk below ε in the Weil form with truncated support, n(WL; ε) ≥ Sh(T) − N(T) − 1 − 𝔇(ε/κ). Does not assume the Riemann hypothesis | paper | part: SunkCount.card_le_of_form_le, SunkCount.card_eigenvalues_le (the finite-dimensional linear algebra step) | That the number grows like e2L is known. The lower bound in the form of a theorem was not found | Sunk eigenvalues of the Weil quadratic form |
| An estimate of the number sunk, n(L) = e2L − 7/8 − S(T*) (T* = 2πe2L). Over 9 cells the difference from measurement is 0.39 to 1.46 | computation | Not found | Sunk eigenvalues of the Weil quadratic form | |
| In place of Landau's dimension theorem: tr Q − tr Q² = (1/2π²) log(4LT) + O(1) | paper | part: TimeBand.compress_sub_sq, TimeBand.trace_compress_sub_sq, TimeBand.card_gt_ge_trace_sub | Not found | Sunk eigenvalues of the Weil quadratic form |
| The 1/k law for the traces: ak = Λ/(π²k) (Λ = log(4LT) + γE + 1) | paper | part: TimeBand.cluster_identity (individual versions for k ≤ 12) | Not found | Sunk eigenvalues of the Weil quadratic form |
| The combinatorial identity Σn≥1 C(k, 2n) On = 2k−2 Hk−1 (for all k ≥ 1) | Lean | TimeBand.binom_oddH_identity | Not found (elementary, and quite possibly known) | Sunk eigenvalues of the Weil quadratic form |
| Theorem T (transfer): tailδ(f) ≤ 2e2L|δ|u(1+ω)/2‖f‖², ω = (2/π)arctan(σ/|δ|) | paper | part: TimeBand.transfer_of_ratio, TimeBand.harmonic_measure_ge | Not found | Sunk eigenvalues of the Weil quadratic form |
| This road does not reach the Riemann hypothesis: the results above hold without assuming the Riemann hypothesis, and can be used neither to prove it nor to disprove it | paper | Known (that the positivity road does not reach it on its own is also stated explicitly by Zhu, arXiv:2608.24827) | Sunk eigenvalues of the Weil quadratic form |
03
The Erdős conjecture on arithmetic progressions (#169)
| Claim | Label | Theorem name | Literature | Article |
|---|---|---|---|---|
| There is a finite set containing no 3-term arithmetic progression whose sum of reciprocals exceeds 3.0085385 (above the 1984 record 3.00849) | Lean | APFree.BellmanRecord.erdos169_lower_record_939, APFree.BellmanRecord.setA939_apfree_and_lower | Not found (compared against 9 lines of primary sources) | The Erdős conjecture on arithmetic progressions |
| There is a finite set containing no 4-term arithmetic progression whose sum of reciprocals exceeds 4.439753369254541 (Walker's 2025 record rounded up at 15 digits). Lower bound 4.439753474215620 | Lean | APFree.FourTermRecord.setA4_apfree_and_beats_walker, APFree.FourTermRecord.setA4_lower_full | Not found (compared against Walker's 2025 table) | The Erdős conjecture on arithmetic progressions |
| A nesting lemma for sets containing no k-term arithmetic progression (Wróblewski's Lemma 2 in its general-k form) | Lean | APFree.Nesting.core_strong, APFree.Nesting.lemma2_four | Known (the form of the lemma is Wróblewski 1984) | The Erdős conjecture on arithmetic progressions |
| An instance of Walker's Theorem 1.2: if a digit set contains no 4-term arithmetic progression mod b, then neither does K(S, b)+1 | Lean | APFree.FourTermRecord.KSet55_apfree | Known (Walker 2025) | The Erdős conjecture on arithmetic progressions |
| If A contains no 3-term arithmetic progression and A ⊆ [x, ∞), then Σ1/n ≪ (log x)−c | known | Known (two lines from Bloom–Sisask) | The Erdős conjecture on arithmetic progressions | |
| Prefix cut: if the sum of reciprocals of a Kempner-type set is at least the record 13.5332472, then |S ∩ [0, v₀]| ≥ mreq(v₀) for each v₀ | paper | — | The Erdős conjecture on arithmetic progressions | |
| One inductive step for the cyclotomic proposition: if S contains no 3-term arithmetic progression, (1+xc) ∣ PS and 3c > D, then S = {0, c} ⊕ S′ with S′ having the same property | paper | Not found (closest are de Bruijn 1950/53, Billey–Swanson, Filaseta–Kalogirou) | The Erdős conjecture on arithmetic progressions | |
| No counterexample to the cyclotomic proposition for deg ≤ 52 (67,236 sets) | computation | — | The Erdős conjecture on arithmetic progressions |
04
The Lovász conjecture
| Claim | Label | Theorem name | Literature | Article |
|---|---|---|---|---|
| The 4 known exceptions (excluding K₂) all have "no cycle, but a path". No counterexample among 9,805 Cayley cases | computation | The list of exceptions is known | The Lovász conjecture | |
| The Cayley graphs of HGL₄(F₄) and SGL₆(F₂) have Hamilton cycles (with certificates) | computation | — | Certificates | |
| Among cubic bipartite graphs on 30 vertices, those that are connected, non-Hamiltonian and of deficiency def = 2 fall into 3 classes up to isomorphism | Lean | CubicBipartite.ClassI.G30_def2, CubicBipartite.Search.G30b_def2, CubicBipartite.Search.G30c_def2 | Not found | The Lovász conjecture |
| The smallest order of a connected cubic bipartite graph with def = 2 is 30 (there is none on 28 vertices or fewer) | computation | Not found | The Lovász conjecture | |
| There is a connected cubic bipartite graph on 20 vertices with circumference 14 that is non-Hamiltonian | Lean | CubicBipartite.Search.G20_def6 | — | The Lovász conjecture |
| The number of Hamilton cycles of the generalized Petersen graph GP(n, 3) is a multiple of n for every odd n ≥ 7 | Lean | GeneralizedPetersen.Descent.gp3_dvd_hc_odd | Not found (this sequence is not in the OEIS) | The Lovász conjecture |
| The number of Hamilton cycles of GP(n, 3) for n = 7, 9, 11, 13, 15 is 7, 9, 11, 26, 75 | Lean | GeneralizedPetersen.Small.GP7_hc_card and others (GP9, GP11, GP13, GP15) | — | The Lovász conjecture |
| Truncation freezes after one generation (T(G) is Hamiltonian ⟺ G is Hamiltonian, and T²(G) is not vertex-transitive). There is no fifth of truncated type up to 3,840 vertices | known | Known (the search up to 3,840 vertices is computation) | The Lovász conjecture | |
| The edge connectivity of an edge-transitive d-regular graph is d. Corollary: if semisymmetric with def = 2, then n ≥ 50 for cubic and n ≥ 26 for quartic | paper | — | The Lovász conjecture | |
| The conjecture "there is no connected vertex-transitive graph with def = 2" contains the vertex-transitive version of Grünbaum's 1974 conjecture | known | Known | The Lovász conjecture |
05
The Hadwiger–Nelson problem
f(α) is the largest number of points of a unit-distance graph with independence number at most α.
| Claim | Label | Theorem name | Literature | Article |
|---|---|---|---|---|
| f(3) ≥ 10, f(4) ≥ 14 (Moser spindle ⊔ K₃, Moser spindle ⊔ Moser spindle) | Lean | HadwigerNelson.Witness.fGe_10_3, HadwigerNelson.Witness.fGe_14_4 | Not found (may be obvious to specialists) | The Hadwiger–Nelson problem |
| f(2k) ≥ 7k, f(2k+1) ≥ 7k+3 | Lean | HadwigerNelson.Family.hn_lower_family | — | The Hadwiger–Nelson problem |
| The 117 classes of 11-point candidates and the 2,100 classes of 16-point candidates cannot be realised in the plane with unit distances (certificates of non-realisability). Hence f(3) = 10 and 14 ≤ f(4) ≤ 15 | Lean | UnitDistance.Order11.no_realization, UnitDistance.Order16.no_realization | Not found (may be obvious to specialists) | The Hadwiger–Nelson problem |
| That the enumeration of the candidates above is exhaustive (including the isomorphism tests) / f(5) ≤ 24 | computation | — | The Hadwiger–Nelson problem | |
| The form of the generator that "adds the point which increases α least" is settled. If α = 2, then n ≤ 7 | paper | — | The Hadwiger–Nelson problem | |
| The fractional chromatic number route hits a ceiling at 4.36 (from the best density 0.22936 of a measurable set avoiding unit distances) | known | Known | The Hadwiger–Nelson problem | |
| Finite unit-distance graphs with n/α > 4 exist | known | Known (Dúcz–Varga, arXiv:2606.28157) | The Hadwiger–Nelson problem |
06
The Hodge conjecture
No line here says anything about the algebraicity of Hodge classes.
| Claim | Label | Theorem name | Literature | Article |
|---|---|---|---|---|
| The Hodge classes of a CM abelian variety reduce to combinatorics of the CM type (admissible set T ⟺ |T ∩ σΦ| = |T|/2 for every σ) | known | Known (Pohlmann 1968, Kubota 1965, Ribet 1980) | The Hodge conjecture | |
| The smallest dimension at which "the exceptional classes are generated by divisors and Weil classes" breaks in this combinatorial model is 8 (no counterexample in an exhaustive check for g ≤ 7). That row is realised over Q | computation | Not found | The Hodge conjecture | |
| The smallest odd dimension at which exceptional classes appear is g = 9: of the 512 CM types of Q(ζ19), 54 are degenerate and primitive, forming just 1 class up to automorphisms | Lean | CMHodge.card_deg_prim | Not found | The Hodge conjecture |
| On that variety, the weight of degeneracy d(A) is at least 3 (the ℓ¹ norm of an element of the annihilating ideal is at least 6). The equality d(A) = 3 is on paper | Lean | CMHodge.weight_ge_three | Not found | The Hodge conjecture |
| There are exactly 6 exceptional Hodge classes of codimension 3 (the admissible sets with |T| = 6 number 90 = 84 products of divisors + 6 exceptional) | Lean | CMHodge.Texc_card | Not found | The Hodge conjecture |
| WF(1) ≅ H¹(E)⊕3: ΦW = {0, 2, 4} is induced from Q(√−19) | Lean | CMHodge.PhiW_eq, CMHodge.level1_breakdown | Not found | The Hodge conjecture |
| The Hodge classes of H⁴(A×E) have dimension 51 = 36 + 9 + 6. Products of divisors span 45 dimensions | Lean | CMHodge.count31_eq | Not found | The Hodge conjecture |
| The position of the exceptional class ξ is settled by known theorems (the pull-back of a split Weil class; absolutely Hodge unconditionally; algebraic if the Lefschetz standard conjecture holds) | known | Known (André 1992, Deligne 1982, Abdulali) | The Hodge conjecture | |
| The roads that build a divisor supporting ξ from theta divisors, isolated singularities, complete intersections (c = 2, 3), single curves, or Jacobians of cyclic covers are all closed | paper | part: CMHodge.places_nonneg_of_mult, CMHodge.not_gorenstein, CMHodge.T0_not_generated_by_divisors | Not found | The Hodge conjecture |
| The algebraicity of ξ is exactly equivalent to the WF part of the generalized Hodge conjecture GHC(1, 3) | paper | That GHC is open in the CM case is known (Vial) | The Hodge conjecture |
07
P versus NP
No claim in this section is machine-checked.
| Claim | Label | Theorem name | Literature | Article |
|---|---|---|---|---|
| The only existing technique that avoids all three barriers (relativization, natural proofs, algebrization) at once is, in substance, Williams's method | known | Known | P versus NP | |
| The ceiling n−1/2 on correlation lower bounds on the monotone side is a matter of principle, and the road of narrowing the band cannot enter the window | paper | The ceiling itself is known (Rossman) | P versus NP | |
| The monotone blocks before and after a negation gain by sharing (they do not decompose, exhaustively at n = 4) | computation | — | P versus NP | |
| Under a weight-neutral planted measure, the floor does not drop | paper | — | P versus NP | |
| Formula size seen as a function on truth tables: V₂(XORn) = L(XORn), with ceiling n² (confirmed for all 65,536 functions) | computation | — | Formula size as a function on truth tables | |
| The number of leaves in the smallest tree-like resolution refutation of the pigeonhole principle PHPn+1n is 3, 11, 43, 189 for n = 1..4 (two independent implementations agree) | computation | Not found (not in the OEIS) | — |
08
Smaller problems
Numbers are those of the Erdős problems collection (erdosproblems.com).
| Claim | Label | Theorem name | Literature | Article |
|---|---|---|---|---|
| #827: seven points in general position always contain four points whose four triangles have pairwise different circumradii. For six points there are configurations where this fails (n₄ = 7) | Lean | DistinctCircumradii.sInf_isGood_eq_seven | Known (the value has an earlier record. This is a proof by another route, machine-checked along the whole chain) | Four points with distinct circumradii |
| #827: a configuration of six points in general position with integer coordinates in which every 4-point subset has a pair of triangles with equal circumradii. And n₄ ≤ 9 | Lean | DistinctCircumradii.seven_le_sInf_isGood_and_sInf_isGood_le_nine | Known (n₄ ≤ 9 is Martínez–Roldán-Pensado 2015) | Four points with distinct circumradii |
| There is no odd k below 78557 with a covering set. On the Riesel side, there is none below 509203 either | computation | Known | Drawing unsolved problems at random | |
| For the number D of distinct distances in an m×m grid, the ratio to n/√log n settles around 1.11, while the ratio to n/log n keeps growing (m ≤ 2048) | computation | — | Drawing unsolved problems at random | |
| #1087: a vertex-transitive finite planar point set lies on a single circle. No factor of log n comes out of this family | paper | — | — | |
| #104: the 3-rich circles of a grid number n1+o(1). Behrend-type transfer from a single grid does not work | paper | — | — | |
| #99: under assumption (J), an optimal configuration has at least c√n − 3 diameter pairs | paper | — (puts side by side the two bounds of Eppstein 2018) | — | |
| #40: g(N) = Nε is not the answer. From the Erdős–Rényi construction for #39, 1 ≪ g(N) ≤ No(1) | paper | — | — | |
| #30: the error term for Sidon sets, b∞ ≤ 1.89715 (fixing the breakpoints makes it a convex program, and the certificate is a single tangent plane) | paper | Weaker (Hou–Zhao, arXiv:2607.01169. Not reached even at the ceiling of this method) | — | |
| #563: β(n, m) ≥ k ⟺ n < R(𝒢m, k). The existence of the limit is equivalent to the convergence of Pα(m)1/m, and does not come out of product-type constructions | paper | Known (a restatement of the pseudo-Ramsey numbers of Erdős–Pach 1983) | — |
09
Questions that remain
Beyond the claims above, these are the questions not yet answered. None of them is an unsolved problem itself; each is one step short of it.
| Problem | Question that remains |
|---|---|
| The Collatz conjecture | Machine checking of the theorem on the tail of the stopping time, and the order of the error term |
| The Erdős conjecture on arithmetic progressions | Bringing k ≥ 5 onto the ground of "the exponent of the logarithm" / the general case of the cyclotomic proposition (the inductive step stops at c > D/3) |
| The Lovász conjecture | Whether there is a vertex-transitive graph with def ≥ 2 that is not a truncation (restricted to cubic graphs, the only examples up to 1,280 vertices are the 4 known ones) / machine checking of 30 as the smallest order of a cubic bipartite graph with def = 2 |
| The Hadwiger–Nelson problem | The single cell n = 15, α = 4 (closing it gives f(4) = 14; a hit gives f(4) = 15) / machine checking of the completeness of the candidate enumeration |
| The Hodge conjecture | A non-normal divisor whose singular locus is not a complete intersection, and a 6-dimensional locus whose normal bundle does not split. These two places alone remain as candidates for a divisor supporting ξ |
| P versus NP | A tool that enters the window of width log log N where the ladder of the number of negations stops |
| #827 | The values for k ≥ 5 |
| Sierpiński numbers | Is there a Sierpiński number with no covering set? (#1113) |
Related: How the work is done (the criteria for the labels, and the thinking behind which claims are put forward) · The Lean verification bundle (the bundle and how to check it) · Archive (the dated lists that preceded this ledger)
Revised 2026-10-02: new page.