A map of the walls — for each problem, what is out of reach
One sheet showing, for each problem in Principia, where things stop now. A wall is the name of what cannot be reached. Walls that closed are marked closed, and next to them is written what it took to close them — the same tool sometimes works on the next wall.
Labels: Leanmachine-checked paperproved, not yet machine-checked computationchecked on this machine, within the range stated knownknown or restated.
Contents
01
Riemann — one part is missing
This section continues The Riemann hypothesis.
When Weil proved the analogue of the Riemann hypothesis for function fields (curves over finite fields), he used four parts. Trying the same over number fields, the only part genuinely missing is Frobenius.
| Part | Over number fields |
|---|---|
| The product C×C and intersection theory | knownGiven by Arakelov theory |
| The Hodge index theorem | knownFaltings–Hriljac–Moriwaki. The signature is exactly what Weil requires, and the arithmetic Weil positivity is itself a theorem. And it says nothing about the Riemann hypothesis |
| Frobenius (a single endomorphism) | The wall. Entirely absent. Among effective Hecke correspondences on X₀(N), the only ones satisfying ΓtΓ = (d₁d₂)Δ are c₁Δ paper — the route through Hecke correspondences is closed |
What is missing is not positivity but Frobenius. The Hecke route closed in three lines — ΓtΓ = (d₁d₂)Δ is equivalent to "all singular values equal √(d₁d₂)"; Eichler–Shimura and Hasse–Weil give |an| ≤ d(n)√n; and d(n)√n ≤ ψ(n) (equality only at n = 4) finishes it.
Wall: statistics over the zeros. When a quantity measured over the sequence of zeros looks like a discovery, whether it is specific to ζ cannot be known until the same quantity has been measured on a point process that does not use ζ. It happened once: a 1/12 that appeared in statistics over the zeros was an identity unrelated to ζ. known
02
Collatz — the quantity being chased is Tao's c
This section continues The Collatz conjecture.
| Wall | Status |
|---|---|
| The quantity chased around the overshoot constant | It is the same as the c of an open problem of Tao's. Both the sup and the inf sit at places nameable 3-adically. knownA restatement of the open problem, not a solution |
| Can a probabilistic argument conclude Collatz? | Closed (no). The same computation would conclude something false about 3n−1, so the line itself is closed. The cycles of 3n−1 (lengths 2 and 7) are the proof paper |
| That the constant C never becomes a constant | Closed. The limit has a closed form and the value at each depth does not — the oscillation is a sawtooth indexed by the convergent denominators of log₂3, and the transfer operator has largest eigenvalue exactly 1/2 with no gap paper |
| The prefactor of the stopping-time tail uk = E(k)/2k — there is no Δ-region of large deviations | Closed. What it took: the conditioned local limit theorem on a non-centred lattice (Vatutin–Wachtel 2009, Theorem 6) and Cramér tilting. uk ρ−k k3/2 = A(θk) + o(1), with A 1-periodic paper. Remaining holes: the order of the error term (only o(1); measured O(1/k)) and a closed form for the mean ascending ladder height |
| Does the sign of 1/3 explain the asymmetry? | Closed. In the 2-adic model the sign of the asymmetry is 3³ < 2⁵, and the forbidden word DDD comes from the same inequality. From the 3-adic limit measure it cannot come in principle (quantities on that side are invariant under the sign) |
03
Erdős #169 — a wall of scale, and the limit of local arguments
This section continues The Erdős conjecture on arithmetic progressions.
| Wall | Status |
|---|---|
| Room left inside the frame of the k = 3 and k = 4 records | Inside the window-separated Bellman frame the room left is roughly 5×10⁻⁶. Next is outside the frame — four or more windows, or block families other than Behrend |
| k = 8, b = 121. Among bases b ≤ 200, the only one where a Kempner-type set could beat the record 13.5332472 is 121 | A wall of scale. The prefix cut paper brought down b = 91 (SAT UNSAT after 1,918 conflicts), but for b = 121 39 pairs do not close after 5×10⁶ conflicts, and the extrapolation is 10⁹ years. For b = 49 the same tool closes in 4.3 seconds. Stopped here. The tantalising piece: the maximum size of 9 rows of ℤ₁₂₁ — if it is at most 26, 16 pairs fall |
| The cyclotomic proposition. For 3-AP-free S, "all roots of PS lie on the unit circle ⟺ S is a direct sum of two-element sets" | The local argument stops at c > D/3. The inductive step ((1+xc) ∣ PS, 3c > D ⟹ S = {0,c} ⊕ S′) goes through on paper paper, but there are genuine direct sums whose largest c is at most D/3 ({0,1} ⊕ {0,9} with c = 3), so the local argument cannot extend beyond that in principle. If the escalation lemma EL (an admissible but not fully involutive c yields an admissible pc for some prime p) is proved, the whole proposition closes. No counterexample for deg ≤ 52; EL holds in 14,304 instances computation |
| k ≥ 5 | Not yet on the footing of "the exponent of the logarithm" — the quantity to be measured from the lower-bound side is not even fixed |
04
Lovász — box III has no example
This section continues The Lovász conjecture.
| Wall | Status |
|---|---|
| Where a fifth exception could live. Splitting by the deficiency def = |V| − circumference: box I (def = 1), box II (truncations), box III (def ≥ 2, not a truncation) | Box III has no example at all. Whether a connected vertex-transitive graph with def = 2 exists is unknown. The conjecture that none does contains the vertex-transitive case of Grünbaum's 1974 conjecture (open) known. In bipartite graphs the standard longest-cycle lemmas (u⁺ ≁ v⁺ and the like) hold automatically and give nothing — exactly where it could happen, the tools do not bite |
| Box II (truncations) | Closed (empty up to 3,840 vertices). A truncation T(H) has 3|V(H)| vertices and is Hamiltonian whenever H is. Truncation freezes after one generation (T²(G) is not vertex-transitive) paper |
| def = 2 without vertex-transitivity | Cubic bipartite: three classes on 30 vertices LeanShiori1161.G30_def2, Shiori1193.G30b_def2, G30c_def2; none on ≤ 28 computation. Tetravalent bipartite: none on n ≤ 24 computation. Semisymmetric: n ≥ 50 if cubic, n ≥ 26 if tetravalent paper — the cubic case is subsumed by the census (Hamiltonian below 3,000 vertices) |
| Divisibility of #HC(GP(n,3)) by odd n — when 3 ∣ n, the local count on a fundamental domain does not kill it | Closed. It took two steps — the classification of spoke sets from the local winding identity (a domino block structure), and rephrasing Hamiltonicity as the permutation next₃∘θ being a single cycle, whose sign contradicts the number of inner strands always being odd. n = 7–15 in Lean LeanShiori1173.GP{n}_dvd_rot |
| The same theorem for general n — the step extracting, from a rotation-invariant Hamiltonian cycle, a window structure on the quotient (degree 2 at each vertex, oriented) was outstanding | Closed. What it took: never constructing the quotient graph — build an oriented 2-factor upstairs from the local structure of the darts of the cycle, descend to the quotient purely algebraically by periodicity, and rephrase "a single cycle" as the first-return map being conjugate to the permutation next₃∘θ. For every odd n ≥ 7, n ∣ #HC(GP(n,3)) LeanShiori1202.gp3_dvd_hc_odd (no hypothesis) |
05
Hadwiger–Nelson — one cell left
This section continues The Hadwiger–Nelson problem.
| Wall | Status |
|---|---|
| The goal was stated in words older than the literature. "Beat the Moser spindle's n/α = 3.5" | Closed (on the side of the words). Fractional chromatic number ≥ 4 and finite unit-distance graphs with independence ratio below 1/4 (Dúcz–Varga) are known, and the phrase has lost its meaning known. What is left is the exact value of f(α). Lesson: each time a goal is written, look its words up again in the ledger of what is known |
| A unit-distance graph with n = 12, α = 3 — it passes every combinatorial and density test | Closed (by geometry). All candidates rejected by interval arithmetic. Closing it needed geometry (the existence of real solutions to the coordinate equations) |
| n = 16, α = 4 — four classes admit no trilateration order, so the plain interval proof does not bite | Closed. It took the parallelogram step pv = px + py − pu (a vertex with no degree of freedom is solved by an equation). All 2,100 classes fall; the certificates are in Lean LeanShiori1185.hn16_no_realiz |
| n = 15, α = 4 (n/α = 3.75) | The one cell remaining. If it closes, f(4) = 14; if it hits, a witness for f(4) = 15 |
| Completeness of the enumeration | That the candidate enumeration is exhaustive (ω ≤ 3, K2,3-free, the u(m) test, minimum degree, isomorphism rejection) is computation computation. To put it into Lean, the enumeration of graphs itself would have to become a Lean object |
06
Walls seen in other problems
| Problem | Wall |
|---|---|
| The diagonal Ramsey numbers (around Erdős #161) | Colour exchange σ swaps the pair (threshold, exponent), so any quantity coming from a construction equivariant under colour exchange (Gaussian model, spherical model, polarity graphs) has second-order contact at C = 1. To beat √2 a first-order term in the sign representation of σ is needed — it cannot come from a colour-exchange-equivariant method in principle paper. Self-complementary graphs (fixed points of σ) have ω = α and cannot move off C = 1 — all 14 Paley graphs with q ≤ 113 have ω = α computation |
| Erdős #563 (the limit of the band for each α) | The existence of lim Pα(m)1/m is no easier for α > 0 than for α = 0 (#77). Supermultiplicativity fails (Pα(3)² > Pα(6)), lexicographic products are ineffective for α ≥ 1/3, XOR-type products are ineffective because monochromatic cliques multiply paper. No product construction can do it in principle. What is needed is a construction that multiplies the vertex count while keeping the level at m₁+m₂+O(1) and the density at α−O(α/m). Stopped here |
| Erdős #52 (sum–product with bounded degree) | Known lower bounds do not depend on the degree d, and no d-dependent lower bound exists in the literature. The route through boxes of units closes structurally at k = 2 (the rank dependence in ESS enters only the constant; the ℂ version of Chang's Theorem 1 is known) known. No gain specific to ℤ. Stopped here |
| Sierpiński numbers (around Erdős #1113) | The odd m for which algebraic factorisation is available are exactly cq and c⁴ (Capelli) paper. An Izotov-type t = 44745755 derived independently is identical to Theorem 10 of FFK 2008 known. Nothing new |
07
Walls on the side of method
| Wall | Remedy |
|---|---|
| A test that answers "none" breaks on the side of rejecting too much. A test that rejects every candidate returns the same "0" whether it works or is broken | Negative controls — mix in known examples that must pass, and trust the test only after seeing them pass. Four times this caught a bug (a false solution, "0 candidates", rounding in an integer square root, an idle loop) |
| The rejected side leaves no record. Filters tend to record only what passes, but the grounds for rejection later become the object of the machine check | Record the rejected side too. The non-realisability of the 296 + 103 ten-vertex subgraphs in Hadwiger–Nelson went into Lean from the record of what was discarded |
| Agreement of a count does not mean the same objects were counted. Totals can agree while the breakdown is wrong in two places at once | Compare the breakdown, not only the total. Check names against contents (assert group orders) before a sweep |
| The words of a goal fall behind the ledger of what is known. Knowing a development in the literature does not by itself update the wording of the goal | Each time a goal is written, look its words up again in the ledger |
| Putting an exhaustive enumeration into the kernel of the machine check is decided by memory. Kernel search costs about 0.5 ms and 50 KB per node; 12 GiB allows 10⁵–10⁶ nodes | Make certificates "the shape of a tree and integer bounds only" and let Lean compute the boxes. Without changing the structure of the enumeration itself, the minimality of def = 2 (150 GiB) does not fit |
08
What this article can claim
| Content | |
|---|---|
| Claimed | For every wall marked closed, what it took to close it is written. For every wall marked open, what is out of reach is named |
| Not claimed | No unsolved problem has moved. What has grown is the map |
| Not claimed | Walls marked "stopped" (b = 121, #563, #52) are judgements about computing resources or the state of the literature, not mathematical walls. Another machine or another tool might move them |
Basis for the labels: Lean is given where the ledger of the Lean verification bundle carries the axiom output. The results are sorted in Taking stock of novelty; the open items are in What remains.