Papers
Where the drafts of the papers are kept. They are set apart from the articles. The originals are in English; this page carries their abstracts, shortened. Each entry opens with a short guide to the problem the paper is about and where to read about it in full. The abstracts themselves are written in the language of the field, so the guide alone is enough for a first reading.
Four labels. Leanmachine-checked (no sorry, no native_decide, only the three standard axioms)
Paperproved on paper, not yet machine-checked
Computedchecked by computation on this machine
Knowna known theorem or a restatement. Each entry ends with one line on what it claims and what it does not.
- Lattice Yang–Mills — near the Millennium Prize problem on the mass gap
- p-adic height pairings — near the Millennium Prize problem of Birch and Swinnerton-Dyer
- Counting Hamiltonian cycles of the generalized Petersen graph GP(n,3)
- The smallest cubic bipartite graphs with circumference deficit 2
- Erdős problem #827 — n₄ = 7
English — the five abstracts
Each entry carries the same four links: PDF, LaTeX source, the Lean files with their axiom logs, and the ledger of machine-checked statements.
One-link integration before Bakry–Émery for SU(2) lattice Yang–Mills
The problem this paper is about. One of the Millennium Prize problems of the Clay Mathematics Institute is "Yang–Mills theory and the mass gap" (the problem page at the Clay Mathematics Institute): construct, with mathematical rigour, the Yang–Mills theory that describes the forces between elementary particles, and show that its lightest particle has positive mass (the mass gap). This paper does not touch that problem itself. It works inside a finite model, "lattice gauge theory", where space is replaced by a grid, and improves one constant that appears in an existing method, the Bakry–Émery criterion. That is the whole of what it claims.
For SU(2) Wilson lattice gauge theory on (Z/L)⁴ we integrate out one quarter of the links exactly — a complete family I*, a set of links (edges of the grid) meeting every plaquette (smallest square of the grid) exactly once — and apply the Bakry–Émery criterion to the marginal, whose density is exp(−Φ) with Φ = −Σ log F₀(β²‖M‖²/4). The second derivative of Φ along U ↦ U e^{τX} is at least −27β² Σ‖X‖², for every β and every configuration; with Ric = 2 for the unit S³ this is a Bakry–Émery curvature 2 − 27β² and a threshold β < √(2/27) = 0.2722, against β < 1/12 = 0.0833 from counting. The chain from the Wilson action to that bound is a theorem of Lean 4 with Mathlib; the step to a log-Sobolev inequality and a mass gap is on paper and in outline only. A second machine-checked statement: a complete family exists on Z^d exactly for d ≤ 4 (restricted to a unit cube it is a binary code of length d−1, size 2^{d−3}, minimum distance 3, and the Hamming bound reads d ≤ 4); with the period included, for k-cells (density exactly 1/(2(k+1)), forcing d ≤ 3k+1), and packings of density at most 1/d for d ≥ 5. The constant 27 cannot be improved past 21.
Leanthe Hessian bound and the combinatorics of complete families Paperthe mass gap, LSI and uniqueness (outline) Computedsearches and numerics
What is claimed and what is not. The claim is an improvement by a constant factor inside the Bakry–Émery method. Nothing is claimed about the continuum limit, and nothing about the Clay problem. The mass gap itself is not a Lean theorem.
PDF ym-onelink-bakry-emery.pdf · LaTeX source ym-onelink-bakry-emery.tex · Lean LatticeGaugeOneLink.lean (StarInequality, StapleCurve, OneLinkSeries, CompleteFamilyLattice, StaplePerturbation, WilsonOneLink), PerfectFamily*.lean, PlaquetteCounting.lean. The main theorems are WilsonOneLink.SW_eq, IsHaarS3.one_link, StaplePerturbation.hess_gauge, PerfectFamily.no_perfectZ_of_five and PlaquetteCounting.perfect_torus_d_le_four. The axiom logs are the axioms-*.txt files of the same names (sorry 0, no native_decide, only propext, Classical.choice and Quot.sound) (the ledger of machine-checked statements)
Integrality of the p-adic height pairing at an anomalous prime is equivalent to a point of order p in E(Q_p)
The problem this paper is about. An elliptic curve is a curve given by an equation of the form y² = x³ + ax + b, and how many points with rational coordinates it has is a central question of number theory. The Millennium Prize problem "the Birch and Swinnerton-Dyer conjecture" (the problem page at the Clay Mathematics Institute) predicts that this abundance (the rank) can be read off an analytic quantity, the L-function. This paper does not touch the conjecture itself. It studies a quantity that appears around it, the p-adic regulator, and asks how large a denominator it can have at certain special primes p (the anomalous primes).
Let E/Q be an elliptic curve, p ≥ 5 of good ordinary reduction and Reg_p the cyclotomic p-adic regulator. At an anomalous prime (p ∣ #E(F_p)) the regulator need not be p-integral, and counting indices gives the baseline v_p(Reg_p) ≥ r − 2 (Theorem A, elementary and known). What this note contributes is the local mechanism governing the deficit: if #E(F_p) = p and Λ = E(Q)/tors surjects onto E(F_p), then every entry of the height matrix lies in Z_p if and only if E(Q_p)[p] ≠ 0; in rank one v_p(Reg_p) ≥ 0 ⟺ split, the non-split value being −1 exactly. The proof is local and runs through one element λ ∈ F_p, the Fermat quotient of the p-th division polynomial: Vélu's factorisation kills λ in the split case, and conversely λ = 0 forces splitting — a known criterion, proved here independently through the Euler identity for the weighted-homogeneous division polynomial and a residue computation at the cusp. CM curves split at every anomalous prime of good reduction. The arithmetic steps are theorems of Lean 4 with Mathlib; the geometric inputs enter as hypotheses.
Paperthe frame of the proof Leanthe arithmetic steps Knownthe baseline (Theorem A) and the local criterion (Proposition 6) Computed§5, PARI/GP
What is claimed and what is not. Nothing here bears on the conjecture of Birch and Swinnerton-Dyer, nor on Ш (the Tate–Shafarevich group), L-functions or the rank. In rank ≥ 2 the theorem is a lower bound, and in the split case nothing predicts the value.
PDF padic-regulator-valuation.pdf · LaTeX source padic-regulator-valuation.tex · Lean PadicHeightValuation4–8.lean (the linear-algebra step of the main theorem is regulator_valuation_of_split_anomalous, the equivalence is regulator_valuation_of_split_anomalous_iff_split, the criterion is lambda_eq_zero_iff_split). The axiom log is axioms-PadicHeightValuation4–8.txt. The correspondence table is §6 of the paper and statements-and-dependencies.md (the ledger of machine-checked statements)
The number of Hamiltonian cycles of the generalized Petersen graph GP(n,3) is divisible by n for odd n
The problem this paper is about. The generalized Petersen graph GP(n,k) is made of an outer n-gon and an inner star that joins n points in steps of k, with the corresponding vertices of the two joined by n further edges (Wikipedia: Generalized Petersen graph). A Hamiltonian cycle is a closed walk that visits every vertex of the graph exactly once and returns to its start. This paper proves, for k = 3, that the number of Hamiltonian cycles is divisible by n whenever n is odd. The numbers themselves were already known.
Let #HC(GP(n,3)) be the number of Hamiltonian cycles of the generalized Petersen graph GP(n,3), counted as edge sets. For every odd n ≥ 7, n divides #HC(GP(n,3)); more precisely no Hamiltonian cycle is invariant under a non-trivial rotation, so Z/n acts freely on the set of Hamiltonian cycles. The proof is elementary — a conservation identity for the oriented cycle, a winding number forced into {0, ±2} when the quotient length is odd, a block structure for the missing edges that exists only when 2 is invertible in Z/d, and a permutation-sign obstruction — and it is carried out entirely in Lean 4 with Mathlib, with no kernel enumeration in the proof for general n. For even n the statement fails and rotation-invariant cycles exist. The values themselves are known (Haugland gave a linear recurrence); the divisibility and the freeness of the action are what this note adds.
Leanthe main theorem and the values for n = 7…15 Computedenumeration up to n = 23 Knownthe values themselves
What is claimed and what is not. Only the main theorem and five values are formalised. On whether it was known, we say only "we did not find it in the literature we searched"; the references not read in the original are marked as such.
PDF gp3-hamiltonian-count.pdf · LaTeX source gp3-hamiltonian-count.tex · Lean GeneralizedPetersenBase / Blocks / Count / Descent / Small / FreeAction.lean (6,947 lines in all) and ChkGeneralizedPetersen.lean. The main theorem is GeneralizedPetersen.Descent.gp3_dvd_hc_odd. The axiom logs are axioms-GeneralizedPetersen*.txt (the ledger of machine-checked statements)
The smallest cubic bipartite graphs with perimeter gap 2
The problem this paper is about. A cubic (3-regular) graph is one in which exactly three edges leave every vertex. A bipartite graph is one whose vertices can be split into two groups so that every edge runs between the groups. The length of the longest cycle in a graph is its circumference, and how far it falls short of the number of vertices is the deficit; deficit 0 means a cycle passes through every vertex (the graph is Hamiltonian). This paper asks how few vertices a connected cubic bipartite graph with deficit exactly 2 can have, and answers 30.
For a connected cubic bipartite graph put def(G) := |V(G)| − circ(G), the number of vertices minus the length of the longest cycle. Since def is even here, def = 2 is the smallest possible failure of Hamiltonicity. The smallest order of a connected cubic bipartite graph with def = 2 is 30, and on 30 vertices there are exactly three such graphs (in the adjacent case). That the three graphs are cubic, bipartite, connected, contain a cycle of length 28 and no longer cycle is a theorem of Lean 4 with Mathlib: the completeness of the search is proved by structural induction on walks and the search trees are run by the kernel. The non-existence below 30 and the classification at 30 are exhaustive computations, not formalised; an independent second route through a 2-edge cut confirms n ≥ 30.
LeanTheorem A (the three graphs on 30 vertices) ComputedTheorem B (non-existence below 30, classification at 30) Knownthe neighbouring minima
What is claimed and what is not. Theorem B is not formalised, the count of classes leaves four leaves of the non-adjacent side without an isomorphism test; on whether it was known, we say only that we did not find it in what we searched.
PDF def2-cubic-bipartite.pdf · LaTeX source def2-cubic-bipartite.tex · Lean CubicBipartiteGap2.lean (1,385 lines) and ChkCubicBipartite.lean. The theorems are CubicBipartite.ClassI.G30_def2, CubicBipartite.Search.G30b_def2 and CubicBipartite.Search.G30c_def2. The axiom log is axioms-CubicBipartiteGap2.txt (the ledger of machine-checked statements)
A machine-checked proof that n₄ = 7 for Erdős problem #827
The problem this paper is about. The Erdős problems site (erdosproblems.com) collects, under numbers, the problems left by the mathematician Paul Erdős; this paper is about its problem 827 (erdosproblems.com/827). Place points in the plane: how many are needed before they must contain four points whose four triangles all have different circumradii (the radius of the circle through three points)? That least number is n₄, and the answer is 7. The problem was already solved — the value was recorded on the site's discussion forum on 22 September 2026 — and this paper comes after it: an independent verification, by a different route, run through Lean's check from end to end. The earlier record itself asked for verification by others.
Let nk be the least N such that every N points of the plane in general position (pairwise distinct, no three collinear, no four concyclic) contain k points all of whose C(k,3) triples have pairwise different circumradii (Erdős #827). A proof of n₄ = 7 is written in Lean 4 and passes its check. The lower bound is the six-point set {±(1,0), ±(1,1), ±(2,3)}, in which every one of the fifteen four-point subsets contains two triangles of equal circumradius. For the upper bound we classify the witness structures of six-point configurations: four points {u,v,c,d} with the shared edge u v form a cell, six points have 90 of them, a cell is a witness when the two circumradii agree, and a configuration is bad when every four-point subset carries a witness. The witness set of a bad six-point configuration falls, up to relabelling, into exactly 35 classes (a search of 204,890 nodes, run by the Lean kernel as 1,820 subtree theorems); 34 of them are not realizable in general position; and the survivor forces the six points to be octahedral — three pairs whose eight transversal triangles share one circumradius. An octahedral six-point set is symmetric about a point, and seven points cannot have all seven of their six-point subsets symmetric about a point, whence n₄ ≤ 7. The whole chain is one Lean 4 statement, sInf {N | IsGood N} = 7, with no hypotheses, no sorry, no native_decide and only the three standard axioms. The earlier record (22 September 2026, on the problem's forum) rests on a different computer-assisted proof — a SAT refutation and ideal saturation in Singular — and is a separate route from this one.
Leanboth bounds, the census, the 34 classes, and the bridge — the whole chain Computedthe search for the certificates, branch counts, timings Knownn₄ ≤ 9 (Martínez–Roldán-Pensado) and the prior record of the value
What is claimed and what is not. One value, for k = 4 and the plane. Nothing is claimed about k ≥ 5 or about the asymptotics. The value depends on the convention for general position (dropping "no four concyclic" leaves only 7 ≤ n₄ ≤ 9). The census is a machine computation, verified rather than surveyable. The computations of the earlier record were not checked here.
PDF erdos827-distinct-circumradii.pdf · LaTeX source erdos827-distinct-circumradii.tex · Lean the 100 modules Principia.DistinctCircumradii.* of principia-src.tar.gz: the foundation Basic, the 73 search-tree modules Census.Tree301–Tree373, Census.Statement / SixPoints / SevenPoints, 22 class modules and Final. The main theorem is DistinctCircumradii.sInf_isGood_eq_seven; the two pillars are censusComplete and restUnrealizable. The axiom log is axioms-principia.txt. The correspondence table is §8.2 of the paper (the ledger of machine-checked statements)
article with amsmath, amsthm, amssymb, longtable and hyperref). Each paper's LaTeX source is linked in its entry above.