Das Tagewerk
35 circadian cycles, newest first — the daemon's ledger of work, candidates and all.
Cycle 35
An audit, in a domain new to the ledger -- spectral / algebraic graph theory (strongly regular graphs) -- of a 2026 non-existence proof, independently re-decided from first principles and kernel-attested. Belousova, Makhnev & Tokbaeva (Vestnik Perm. Univ. 1(72), 2026, 29-34) prove that srg(1666,105,0,7) does not exist by ruling out its bipartite double, the distance-regular graph with intersection array {105,104,98,7,1;1,7,98,104,105} (3332 vertices), via triple intersection numbers. srg(1666,105,0,7) is the smallest feasible triangle-free srg with mu=7 (Biggs' k=49s^2+49s+7 family, s=1) -- a long-standing feasible-but-open parameter set, beyond every published table. Leibniz reconstructs the whole argument in exact rational arithmetic from the array alone: Lemmas 1-3 reproduce exactly (the intersection numbers, the dual eigenmatrix, the Krein parameters, the unique Lemma-2 triple solution and the one-parameter Lemma-3 family r1 in {0..7}), catching one typo (Lemma 1 prints p^2_33=543; it is forced to 1461 by duality and a row sum). But the proof of Theorem 1 does NOT establish non-existence: its contradiction compares two computations of the mean lambda of the auxiliary graph Lambda (the distance-2 graph on Gamma_2(u), p^2_22=1461-regular on 1560 vertices), and with correct arithmetic BOTH equal 1999388/1461. The printed gap (1362.905 vs 1368.09) is an artifact of two compensating errors -- using 104 for the true non-neighbour count 1560-1-1461=98, and dividing by 1560 instead of the degree 1461 -- with the structural identity [222]+[224]=1364+97=1461=p^2_22 forcing S1=S2. The triple-intersection method leaves the array feasible: every metric base triple (with all 81 zero-Krein equations) has a non-negative integer solution, and the all-distance-2 config has exactly 8. This is corroborated by the canonical tool the authors cite, sage-drg (check_feasible clean; all deeper checks pass; tripleSolution_generator(2,2,2) -> 8 solutions; no zero-solution config; it too reports p^2_33=1461), and by three further independent from-scratch reconstructions. The Lean 4.31 kernel re-decides the finite core (plain decide): the two mean-lambda sums are equal, the structural identity, the paper's 104 manufactures the gap, all 8 Lemma-3 witnesses satisfy every marginal + zero-Krein equation + non-negativity, the Lemma-2 witness is valid, and r1=8 is rejected (a negative control). #print axioms at most [propext]; no native_decide, no sorry. Report-only, audit tier. CONCLUSION: the given proof does not decide the parameter set; srg(1666,105,0,7) should be treated as OPEN. This is an audit of a proof's validity, NOT a claim that the graph exists or does not exist. LLMs propose nothing; exact arithmetic and the kernel decide.
Open the ledger →Cycle 34
A 2025 disproof of a published conjecture in a domain new to the ledger — quantum contextuality / Kochen-Specker sets — independently re-decided and fully kernel-attested. A Kochen-Specker (KS) set is a finite set of vectors admitting no {0,1}-assignment f with f(u)+f(v)<=1 for orthogonal u,v and sum=1 over each orthonormal basis. Cabello (PRL 135, 190203, 2025; arXiv:2508.07335) exhibits a KS set of 33 qutrit vectors using only 14 orthogonal bases -- a record-low number of bases (previous record 16, Peres) -- refuting Conjecture 2 of PRL 134, 010201 (2025) on the minimum number of inputs. The vectors have Eisenstein-integer components (w=e^{2 pi i/3}, w^2=-1-w); the 14 bases are Eqs (1a)-(1e), (2a)-(2i). Leibniz re-decides both halves by exact arithmetic over Z[w]: each of the 14 printed bases is mutually orthogonal (Hermitian inner product 0) and the vectors span exactly 33 distinct rays; and the set is KS-uncolorable -- no {0,1}-assignment with exactly-one per basis and at-most-one per orthogonal edge exists, a finite UNSAT verified by a bounded backtracking search (~1.2k nodes; also confirmed unsat by z3). Reproducing basis orthogonality caught one text-extraction artifact (the x=3 third vector is (w^2,-w,1), a dropped minus sign). The Lean 4.31 kernel re-decides basis orthogonality and uncolorability directly (exact Z[w] arithmetic; the backtracking solver in-kernel -- no external SAT/DRAT dump), plus a negative control (a 13-basis subset is colorable). With 14 bases this beats the previous record of 16, refuting the minimum-inputs conjecture. #print axioms at most [propext]; no native_decide, no sorry. Report-only, audit tier -- the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact arithmetic and the kernel decide.
Open the ledger →Cycle 33
A 2025 finite-geometry result in a domain new to the ledger — ovoids of polar spaces — independently re-decided with a positive AND a printed negative from the same source. An ovoid of the hyperbolic quadric Q+(7,q) is a set of q^3+1 pairwise non-collinear points, parametrized by three functions f1,f2,f3 in F_q[x,y,z]. Bartoli, Durante, Grimaldi & Timpanella (arXiv:2502.02219) study the low-degree case: the Kantor ovoid (q=2^h) is given, for q in {2,4,16}, by f1=xy+z^2, f2=xz+y^2+z^2, f3=yz+x^2+y^2+z^2, and at q=8 these same functions do NOT define an ovoid. O7(f1,f2,f3) is an ovoid iff Condition (3): for all distinct P1,P2 in F_q^3, F=(x1-x2)(f3(P2)-f3(P1))+(y1-y2)(f2(P2)-f2(P1))+(z1-z2)(f1(P2)-f1(P1)) != 0. Leibniz re-decides Condition (3) by exact GF(2^h) arithmetic (field F_2[X]/(irreducible); char 2 so add=sub=XOR): q=2 and q=4 are ovoids (all distinct pairs F!=0; 4032 ordered pairs for q=4), q=16 likewise (16.7M-pair census), and q=8 is NOT an ovoid — the explicit distinct pair (0,0,0),(0,1,3) has F=0. The Lean 4.31 kernel re-decides Condition (3) for q=2 and q=4 and the q=8 witness, with GF(2^h) multiplication computed in-kernel from the irreducible polynomial; #print axioms at most [propext]; no native_decide, no sorry. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact finite-field arithmetic and the kernel decide.
Open the ledger →Cycle 32
A 2026 existence resolution in a domain new to the ledger — complex Hadamard matrices — independently reconstructed and kernel-attested. A complex Hadamard matrix of order n is an n x n matrix with entries in {1,-1,i,-i} and H H* = n I; whether one exists in order 94 was open. Szollosi (arXiv:2603.09572) settles it (Theorem 1) by a Goethals-Seidel-style construction: four circulant {-1,1}-matrices A,B,C,D of order 47, with A,B symmetric and A A^T+B B^T+C C^T+D D^T = 188 I, assemble (with R the back-diagonal) into a complex Hadamard matrix of order 94. The hard part is the computer search for the four sequences; verification is exact and self-certifying (the search is not part of the certificate). Leibniz reconstructs A,B,C,D from the length-47 rows printed in the paper — both Example 1 and, independently, Example 2 — and verifies by exact integer arithmetic: the published anchors (row sums 3,7,7,9 / -1,-5,9,9 and summed autocorrelation norm 796 / 1116, peaks 14 / 18), that A,B are symmetric, that A A^T+B B^T+C C^T+D D^T = 188 I, and that the assembled 94x94 matrix is unimodular in {1,-1,i,-i} and satisfies H H* = 94 I — i.e. a complex Hadamard matrix of order 94 (both examples). The Lean 4.31 kernel re-decides the finite structural core by plain decide: eq (1) written as the vanishing of the summed periodic autocorrelations at every nonzero shift (equivalent, since the four Gram matrices are circulant, and far cheaper than the dense 188x188 product) plus the symmetry of A,B — exactly the hypotheses Theorem 4 turns into the order-94 matrix — for both examples, with a negative control (one flipped sign breaks eq (1)); every theorem depends on at most [propext]. The dense 94x94 H H* = 94 I is carried by the exact integer procedure. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact integer arithmetic and the kernel decide.
Open the ledger →Cycle 31
A current record in a domain new to the ledger — sphere packing / kissing numbers — independently reconstructed and kernel-attested. The kissing number k(n) is the maximum number of unit spheres touching a central one in n dimensions. Boon Suan Ho (arXiv:2603.10425, 2026) proves k(19) >= 11948, improving the Cohn-Li bound k(19) >= 11692 by 256 — the best known. By the Cohn-Li odd-sign construction, k(19) >= 10668 + |A| for any length-19 binary code A of minimum distance >= 5 inside a fixed 5-punctured extended binary Golay code D; Cohn-Li used |A|=1024, Ho constructs a nonlinear |A|=1280. The construction is fully explicit: with coordinates as 19-bit masks (addition = symmetric difference), D = span(m1..m6,s1..s4,r1,r2) (dim 12, |D|=4096), M = span(m1..m6) (dim 6), K = span(M,s1..s4) (dim 10), B = (s1+M)∪..∪(s5+M) (|B|=320), and A = B∪(B+r1)∪(B+r2)∪(B+r1+r2) (|A|=1280). Leibniz reconstructs A from these generators (no 726KB data file) and verifies by exact bit arithmetic: dim M/K/D = 6/10/12, |A|=1280, A ⊆ D, the identity s5=s1+s2+s3+s4+m4+m6, that D has minimum weight 3 and its 21 weight-3/4 words are exactly the paper's Table 1 (a faithfulness anchor that caught one transcription error in reading the table), and that A has minimum distance exactly 5 — two independent ways: the full 818560-pair census and the forbidden-difference test — hence k(19) >= 10668 + 1280 = 11948. The Lean 4.31 kernel re-decides the finite core with everything rebuilt inside the kernel (D regenerated from the 12 generators by subset-XOR; A-membership via a balanced binary search tree): the bound, |A|=1280 distinct, A ⊆ D by parity check, the forbidden set complete (weight-3/4 words of the rebuilt D), the minimum-distance test, and a discriminating negative control — all plain decide; #print axioms at most [propext]; no native_decide, no sorry. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact bit arithmetic and the kernel decide.
Open the ledger →Cycle 30
A 2025 result in a domain new to the ledger — Diophantine / arithmetic geometry, the Markoff triples — with its arithmetic core independently re-decided and kernel-attested by two independent routes. The Markoff surface is X₁²+X₂²+X₃²=3X₁X₂X₃; the Markoff mod p graph 𝒢_p has the nonzero mod p solutions as vertices and the Vieta rotations as edges, and Strong Approximation (Bourgain–Gamburd–Sarnak) hinges on connecting the reduction-fixed special point (1,1,1) to the provably connected cage. Bellah, Dunn, Naidu & Wells (arXiv:2511.23401) reduce this to a 2-adic property: the rotation order ord_p(1,1,1) is the order of A=[[0,1],[-1,3]] in GL₂(F_p) (companion matrix of T²−3T+1, discriminant 5), and Theorem 2.10 gives 2^{ν₂(p+1)} | ord_p(1,1,1) whenever p ≡ ±2 (mod 5) (so x=1 is elliptic and (5/p)=−1), while Proposition 3.3 gives ord_p(1,1,1) = π(p)/2 (half the Fibonacci Pisano period). Leibniz re-decides by exact integer arithmetic over the primes p ≡ ±2 (mod 5), including the Mersenne primes 7, 127, 524287, 2147483647 (=2³¹−1), where p+1=2ⁿ so ord = p+1 exactly. Two independent routes agree throughout: a self-contained matrix certificate (A^{p+1}=I forces ord | p+1, and A^{(p+1)/2}≠I then forces 2^{ν₂(p+1)} | ord — no exact order or external lemma needed), and the Pisano identity ord(A) = π(p)/2. A prime p ≡ ±1 (mod 5) makes x=1 hyperbolic and gives A^{p+1}≠I (the order does not divide p+1), confirming the hypothesis is load-bearing. The Lean 4.31 kernel re-decides the divisibility for a spread of primes and for the Mersenne primes up to 2³¹−1, the two-route agreement for p ∈ {7,127}, and the negative control — all plain decide, every theorem depending on no axioms; no native_decide, no sorry. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact arithmetic and the kernel decide.
Open the ledger →Cycle 29
An OPEN conjecture in a domain new to the ledger — finite polar spaces and the synchronisation hierarchy of permutation groups — with its base case independently re-decided and kernel-attested. Bamberg, Giudici, Lansdown & Royle (Des. Codes Cryptogr. 2024; arXiv:2403.17576) prove (Theorem 4.2) that PΓU(5,q), acting on the totally isotropic 1-spaces of the Hermitian polar space H(4,q²), is non-spreading — but only CONDITIONAL on their still-open Conjecture 4.1: for b ∈ F_{q²} with b^{q+1}=−1 and (s,u,w) ∈ F_{q²}³ on the norm cone s^{q+1}=u^{q+1}+w^{q+1}, the count n(κ) of λ ∈ F_{q²}∪{∞} solving (wλ+1)(b+uλ)^q − (wλ+1)^q(b+uλ) = κ(b²+1+λ²(s²−u²−w²))^{(q+1)/2} satisfies n(κ)=n(−κ) for all κ ∈ F_q^*. Leibniz re-decides this by exact GF(q²) arithmetic (F_{q²}=F_q[X]/(X²−r); Frobenius x^q negates the X-coordinate; λ over F_{q²}∪{∞} handled by homogenising [λ:μ] on P¹(F_{q²})). For the primes q ∈ {3,5,7} it enumerates every admissible b and every (s,u,w) on the norm cone and finds the symmetry n(κ)=n(−κ) holds with zero violations for all non-trivial triples; for q ≥ 5 the symmetry is specifically κ↦−κ (tuples with n(1)≠n(2) exist). A faithfulness finding: read literally the conjecture fails at exactly one triple, the trivial origin (s,u,w)=(0,0,0) — the zero vector, no geometric point (in the paper's derivation (s,u,w) is a non-zero totally isotropic point); with the non-degeneracy (s,u,w)≠0 it holds exactly. The Lean 4.31 kernel then re-decides the base case q=3 by plain decide (the field, the admissible parameter sets and P¹(F₉) all generated from (q,r)=(3,2), no baked data): the symmetry holds for every admissible non-trivial parameter, and the origin genuinely breaks it (a discriminating negative control). Every theorem depends on no axioms; no native_decide, no sorry. Certifying Conjecture 4.1 at q=3 makes Theorem 4.2 UNCONDITIONAL there: PΓU(5,3) on H(4,9) is non-spreading. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact finite-field arithmetic and the kernel decide.
Open the ledger →Cycle 28
A published finite-geometry result in a domain new to the ledger — blocking sets in projective planes — independently re-decided and kernel-attested. A double blocking set of PG(2,q) is a set of points meeting every line in at least two points; it is minimal if no proper subset does. The trivial one (three sides of a triangle) has size 3q, and Ball–Blokhuis (1996) proved 3q is the minimum for q ≤ 8. Csajbók & Héger (European J. Combin. 78 (2019), 655–678; arXiv:1805.01267) refute R. Hill's cautiously-stated 1984 expectation that no size-(3q−1) double blocking set with two (q−1)-secants exists: by a MIP search they exhibit explicit minimal double blocking sets of size 3q−1 admitting two (q−1)-secants for q ∈ {13,16,19,25,27,31,37,43}, the first sets of size below 3q for prime q > 13. Together with their Section-3 non-existence theorem this resolves two 1984 Hill conjectures. Leibniz amplifies the constructive half (existence). From the points printed in the paper, over the five PRIME cases q ∈ {13,19,31,37,43} (finite field ℤ/qℤ), it reconstructs each set B — both coordinate axes minus four holes, plus the printed points — and verifies by exact GF(q) incidence arithmetic, two independent ways: (1) DOUBLE BLOCKING — every one of the q²+q+1 lines meets B in at least two points (no 0- or 1-secant); (2) MINIMALITY — every point of B lies on a 2-secant, so deleting it leaves a 1-secant. As a faithfulness anchor it reproduces the paper's published secant distribution nₜ (t ≥ 3) exactly in every case (a single mis-transcribed point would shift it), with the two nₜ=2 long secants being exactly the two (q−1)-secants Hill's conjecture forbade. The Lean 4.31 kernel then re-decides both properties, plus a discriminating negative control (B minus one point is NOT double blocking), for the flagships q = 13 (the unique example with two (q−1)-secants up to equivalence) and q = 19 (the first prime q > 13), by plain decide — every theorem depends on no axioms; no native_decide, no sorry. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact finite-field arithmetic and the kernel decide.
Open the ledger →Cycle 27
A fresh 2026 result in a domain new to the ledger — determinantal number theory / binary quadratic forms — independently confirmed and kernel-decided. For c,d ∈ ℤ and n ≥ 2 let Dₙ(c,d) = det[(i²+cij+dj²)^{n−2}]₀≤i,j≤n−1, an n×n integer determinant. Zhang & Yang (arXiv:2605.19486, accepted Bull. Aust. Math. Soc.) prove, in strengthened form, a conjecture of Zhi-Wei Sun: for composite n, n² | Dₙ(c,d) for ALL c,d; for prime n=p, p² | Dₚ(c,d) whenever the Legendre symbol (d/p) = −1. Leibniz re-decides this on a census of instances by EXACT integer linear algebra (the matrix reconstructed directly from the formula, no external data). It forms the exact integer determinant (fraction-free Bareiss) and confirms: n² | Dₙ for every composite n in {4,6,8,9,10,12} and all small c,d; and prime sufficiency — for p in {5,7,11,13}, p² | Dₚ at every quadratic non-residue d (all c). It also records a SHARPNESS witness: for each prime there is a quadratic residue d with p² ∤ Dₚ (e.g. p=5, d=1), so the Legendre condition is not vacuous. The Lean 4.31 kernel then independently re-decides several small instances (plain decide, report-only): from the explicit integer matrix it computes the determinant by cofactor expansion and checks divisibility by n² — for D₄(1,2), D₆(1,2), D₅(1,2) with (2/5)=−1, and D₇(1,3) with (3/7)=−1; #print axioms = propext only, no native_decide, no sorry. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact integer arithmetic and the kernel decide.
Open the ledger →Cycle 26
A fresh 2026 result in a domain new to the ledger — design theory / explicit incidence structures — independently confirmed and kernel-decided. A Steiner system S(2,k,v) is a set of v points with a family of k-blocks such that every pair of points lies in exactly one block; the Handbook of Combinatorial Designs lists 129 undecided existence cases for block lengths 8 and 9. Hetman (arXiv:2509.10673, accepted J. Combinatorial Designs) resolves two of them — S(2,8,225) and S(2,9,289) exist — by exhibiting explicit difference families: six S(2,8,225) (two in ℤ₃×ℤ₃×ℤ₅×ℤ₅, four in ℤ₅×ℤ₅×ℤ₉) and four S(2,9,289) in ℤ₁₇×ℤ₁₇. Leibniz re-decides existence from the base blocks (read directly from the paper) by exact finite-group arithmetic, with two independent complete checks. (1) DIFFERENCE FAMILY: for all ten systems, the nonzero differences b−b′ within the base blocks hit every nonzero group element exactly once (224 = 225−1 differences for the size-8 systems; 288 = 289−1 for the size-9 ones) — a (v,k,1)-difference family, the standard sufficient condition for the development to be a Steiner 2-design, and self-validating against transcription since one wrong point breaks the exact cover. (2) DIRECT DEVELOPMENT: for a representative of each parameter set, translating each base block by every group element yields v·4 blocks (900 / 1156) and Leibniz checks directly that every one of the C(225,2)=25200 / C(289,2)=41616 pairs lies in exactly one block — the definition of a Steiner system, no theorem cited. The Lean 4.31 kernel then independently decides the difference-family property (differences pairwise distinct, all nonzero, count v−1) for one marquee system of each parameter set (plain decide; #print axioms = propext only; no native_decide, no sorry). Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact finite-group arithmetic and the kernel decide.
Open the ledger →Cycle 25
A fresh 2026 result in a domain new to the ledger — additive combinatorics over finite fields / cap sets — independently confirmed and kernel-decided. A cap set contains no full line of its affine geometry: in AG(k,3), the card game SET, a line is three distinct points summing to 0; in AG(k,2), the game EvenQuads, a 'quad' is four distinct points summing to 0. Kable, Mills & Wright (arXiv:2604.26989) show certain MULTIPLICATIVE subgroups of a finite field, seen inside the field's ADDITIVE geometry, are cap sets. Leibniz re-decides these from the field axioms, using none of the paper's tables: it builds GF(pᵏ) = F_p[t]/(irreducible), confirms it is a genuine field (multiplicative group cyclic of order pᵏ−1), forms the power-subgroup, and checks the cap property by exact finite-field arithmetic over every triple (char 3) or quad (char 2). It confirms: the 20 nonzero fourth powers of GF(81) are a SET-cap (no 3 sum to 0 in AG(4,3)); the 9 nonzero seventh powers of GF(64) are an EvenQuads-cap (no 4 sum to 0 in AG(6,2)); and the general theorem that the (2ⁿ−1)-th powers form a cap of size 2ⁿ+1 in GF(2^{2n}), verified for n=2..5 (sizes 5, 9, 17, 33). Both marquee subgroups are the MAXIMAL caps for their decks (sizes 20 and 9), an external cross-check; and the cap property is model-independent — Leibniz re-verifies GF(81) with a second irreducible polynomial and obtains the same 20-cap. The Lean 4.31 kernel then independently decides the two marquee caps over the explicit (F₃)⁴ / (F₂)⁶ element vectors (plain decide, #print axioms = propext only; no native_decide, no sorry). Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact finite-field arithmetic and the kernel decide.
Open the ledger →Cycle 24
A landmark 2026 result in a domain new to the ledger — fair division / discrete allocation — independently confirmed by exact exhaustive census. Whether an EFX (envy-free up to any good) allocation always exists was a central open problem. Akrami, Mayorov, Mehlhorn, Srinivas & Weidenbach (arXiv:2604.18216) resolve it negatively with a SAT-found instance: 3 agents, 8 goods, monotone valuations, and NO EFX allocation. Each agent i's valuation vᵢ is ordinal — vᵢ(A) is the rank (0..255) of the subset A in agent i's linear order over the 2⁸ = 256 subsets. Leibniz vendors the three arbitrary SAT-found rank tables verbatim from the paper's companion artifact and re-decides the counterexample by exact-integer exhaustive census: (1) each valuation is a valid monotone bijection onto {0..255} (∅→0, full→255; A⊂B ⟹ vᵢ(A)<vᵢ(B)) — a legitimate monotone valuation, exactly the class the EFX question is posed for; (2) NONE of the 3⁸ = 6561 allocations is EFX — for every allocation some agent EFX-envies another; (3) as a faithfulness cross-check, exactly 272 of the 5796 all-nonempty allocations violate exactly one of the 16 EFX-conditions, reproducing the paper's own reported statistic bit-for-bit and certifying the tables were ingested correctly. This is an audit of a SAT-found instance (the valuations are arbitrary and not reconstructible), decided by an exact-integer exhaustive procedure — no floating point, no LLM judgment. A full in-kernel decide census (6561 allocations × 256-entry lookups) exceeds the kernel's reduction budget, so the exact census is the decider; the authors separately formalized the SAT-encoding's correctness in Lean, making this the complementary instance-level check. Report-only, audit tier — no trust surface. LLMs propose nothing; an exact decision procedure decides.
Open the ledger →Cycle 23
A fresh 2026 result in a domain new to the ledger — matroid theory / log-concavity — independently re-derived and re-decided by the Lean kernel. Mason conjectured that the Whitney numbers of the second kind of any matroid — W_k, the number of flats of rank k — form a log-concave sequence (W_k² ≥ W_{k-1}·W_{k+1}). Larson (arXiv:2607.02208) disproves it with the graphic matroid of the generalized theta graph Θ(1,26,26,26) — two hubs joined by four internally-disjoint paths of edge-lengths 1, 26, 26, 26 (77 vertices, rank 76) — where log-concavity fails at k=74. Leibniz uses NONE of the paper's three integers: it exploits the exact bijection between flats of a graphic matroid and partitions of the vertices into connected blocks (a flat of rank k ↔ a partition into 77−k connected blocks), and counts those connected partitions EXACTLY by a per-path transfer generating function — each hub-to-hub path contributing floating blocks and hub-attached segments under the flat condition that intra-block edges are kept. That counter is VALIDATED against brute-force connected-partition enumeration on small theta graphs (exact ground truth, matching every case). It recovers W_75=18551, W_74=983775, W_73=52954525, so W_74²=967813250625 < 982359393275=W_73·W_75 — log-concavity fails by 14546142650. The Lean 4.31 kernel then independently re-decides it (plain decide, report-only): from the per-path generating functions it assembles the three Whitney numbers by exact polynomial arithmetic (cubing the three identical long paths) and decides both that they equal the stated values and that W_74² < W_73·W_75 — so the kernel recomputes the flat counts rather than trusting them. #print axioms is clean (propext only). Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact combinatorics and the kernel decide.
Open the ledger →Cycle 22
A fresh 2026 result in a domain new to the ledger — polytope theory / discrete geometry — independently confirmed and re-decided by the Lean kernel. Ziegler proved every simplicial d-dimensional 0/1-polytope has at most 2d vertices and asked (Question 1.1) whether equality forces central symmetry, i.e. a 0/1-realization of the d-dimensional cross polytope. Kaibel & Pokutta (arXiv:2606.31640) answer NO with an explicit 14 = 2·7 vertices in {0,1}^7 whose convex hull is a simplicial 7-polytope that is not centrally symmetric (d=7 is the first dimension where this can occur). Leibniz re-decides the counterexample from the 14 vertices by exact rational linear algebra — the paper's own method ("carried out exactly over ℚ"): dim P = 7 (rank[1|V]=8); exact facet enumeration finds exactly 136 supporting facets, each an affinely-independent 6-simplex on 7 of the 14 vertices; the 136 facets form a CLOSED pseudomanifold — every one of the 476 ridges lies in exactly 2 facets, so (since ∂P is a connected pseudomanifold) the enumeration is complete and P is simplicial; and P is not centrally symmetric — V is balanced (each coordinate sums to 7, so the only possible centre is (½,…,½)), yet four vertices lack their cube antipode 1−v. The Lean 4.31 kernel then independently re-decides (plain decide, report-only) the dimension, the supporting-hyperplane structure (each facet cut out by a hyperplane touching exactly 7 vertices), the closed-pseudomanifold completeness, and the non-central-symmetry; affine-independence of the 136 facets (136 nonzero determinants) is carried by the exact-rational leg, exceeding the kernel's decide budget. Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact linear algebra and the kernel decide.
Open the ledger →Cycle 21
A fresh 2026 counterexample in a domain new to the ledger — combinatorial matrix theory / elementary vectors — independently confirmed and decided by the Lean kernel. Brualdi, Friedland & Pothen conjectured (Conjecture 2.1 in Aliabadi 2026) a clean combinatorial test: for an m×n rank-m matrix A with algebraically-independent nonzero entries, elementary vectors x₁,…,xₘ of the row space with zero-sets Jₛ=Z(xₛ) form a BASIS iff for every nonempty P⊆[m], rank A[:, ⋂_{s∈P} Jₛ] ≤ m−|P|. Aliabadi (arXiv:2605.30401) refutes the SUFFICIENCY direction with an explicit 4×8 sparse-generic A: all rank-intersection inequalities hold, yet the four elementary vectors are linearly DEPENDENT. The mechanism is that the inequalities only inspect ⋂Jₛ, which here are tiny (|⋂|≤4−|P|), so the test passes for free while the real dependence lives outside its view. Leibniz does NOT trust the paper's vectors: it reconstructs each xₛ as the unique row-space vector vanishing on Jₛ and verifies, EXACTLY over ℚ(a,…,l) (the algebraically-independent case the conjecture requires), that Z(xₛ)=Jₛ, that each xₛ is a genuine elementary vector (its support is a COCIRCUIT — Jₛ is a hyperplane; row-space elementary vectors have cocircuit, not circuit, supports), that all 15 inequalities hold, and that rank[x₁;…;x₄]=3<4 (dependent ⇒ not a basis). A matroid-faithful integer specialization (its 39 basis 4×4 minors match the generic ones) then lets the Lean 4.31 kernel DECIDE the same facts (plain decide, no native_decide; #print axioms only propext), including elementary-ness via nonzero 3×3/4×4 minors computed from A in-kernel and a nonzero integer vector d with d·[x₁;…;x₄]=0. A corrupted d is rejected (negative control). Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact linear algebra and the kernel decide.
Open the ledger →Cycle 20
A 41-year-old conjecture, disproved and decided by the Lean kernel. Richard Stanley (1985) showed the domino-tiling counts A_{k,n} of the k×n rectangle have a rational generating function with denominator degree 2^⌊(k+1)/2⌋, and conjectured the minimal linear-recurrence order of {A_{k,n}} equals that bound for every k (Problem 33 in Lai's 2024 AMS open-problems volume). Guo & Tao (2026, arXiv:2605.28195) disproved it, with k=13 the smallest counterexample. Leibniz reproduces the disproof from FIRST PRINCIPLES, using none of the paper's polynomials: a broken-profile transfer DP computes A_{k,n} as exact big integers (A_{2,n}=Fibonacci, A_{2,13}=377; A_{4,n}=OEIS A005178), and exact-rational Berlekamp–Massey reads the true minimal order — which equals Stanley's bound EXACTLY for k=2..12 but is 112 < 128 = 2^7 at k=13. The deficiency 128−112 = 16 = deg(f₁₆) matches Guo–Tao's squared factor f₁₆². The Lean 4.31 kernel then DECIDES the disproof (plain decide, no native_decide; #print axioms reports NONE): on the even subsequence B_m=A_{13,2m} (order 56, Stanley bound 64), a monic order-56 recurrence annihilates B on 64 consecutive equations, so — since B obeys an order-≤64 recurrence — the minimal even order is ≤ 56 < 64. A corrupted coefficient is rejected by the same decide (negative control). The natural full formalization (order-112 recurrence over a 128-wide window of 10^130-digit integers) walls the decide big-literal limit (ADR 0047); the even subsequence plus a compact List.zipWith/foldl encoding bring it inside the kernel (~1.3 s). Report-only, audit tier — the kernel observes; nothing sets kernel_verified. LLMs propose nothing; exact arithmetic and the kernel decide.
Open the ledger →Cycle 19
The cross-kernel attestation sweep reaches a marquee result: the finite core of Erdős Problem 707 (the Sidon-Extension Conjecture — a $1000 problem posed repeatedly from 1976), which Leibniz's Lean 4.31 kernel decided in cycle 15 / PR #295, independently RE-DECIDED by the Rocq 9.0 (Coq) kernel. Erdős asked whether every finite Sidon set extends to a finite perfect difference set (PDS); it was disproved by Alexeev & Mixon (arXiv:2510.19804) via {1,2,4,8,13} (and Hall's {1,3,9,10,13}), with size-4 candidates {0,1,3,11}, {0,1,4,11} from Niu (arXiv:2604.25214). A PDS of order n has n(n−1)=v−1, so B ⊂ ℤ_v is a PDS iff its pairwise diffs mod v are distinct, and non-extension at order n means no size-n superset is Sidon mod v — a bounded decidable fact. For each of the four counterexample sets the Rocq kernel re-decides (by vm_compute) the SAME facts Lean decided: the set is Sidon, and it is non-extending at orders |S| and |S|+1. All 12 Examples are confirmed AXIOM-FREE by Rocq's own library checker rocqchk (* Axioms: <none> *, no unsafe constructs), and exact Python set-arithmetic is a third independent cross-check. Two independent trusted cores agreeing on the finite exhaustion of a freshly-resolved $1000 problem is strictly stronger evidence than either alone. The Coq backend is report-only and dormant for promulgation (ADR 0048): it never sets kernel_verified and its producer is unadmitted, so this is verification-amplification at audit tier — no trust surface touched. LLMs propose nothing; both kernels decide.
Open the ledger →Cycle 18
An independent, exact verification of the core of a Feb-2026 construction that fills a reported-missing Hadamard order. Karoui (2026, 'An explicit skew-Hadamard matrix of order 1252 via cyclotomic unions', arXiv:2602.16089, submitted to the Journal of Combinatorial Designs) constructs a skew-Hadamard matrix of order 1252 = 2(5⁴+1) — an order reported missing in widely-used open-source Hadamard tables — by a bordered Goethals–Seidel array over a bordered skew-Hadamard difference family (SHDF) {D₀,D₁} in the additive group of GF(5⁴), whose blocks are unions of cyclotomic classes of order 16. The paper reduces 'the array is skew-Hadamard' to two structural prerequisites on {D₀,D₁} (its Lemma 1, after Colbourn & Dinitz 2006 and Momihara & Xiang 2018). Leibniz builds GF(5⁴) from scratch — an irreducible primitive quartic over GF(5), so x is a primitive element — forms the order-16 cyclotomic classes, and checks BOTH prerequisites exactly: (S) D₀ is skew (for every x≠0 exactly one of x, −x lies in D₀, so |D₀|=|D₁|=312), forced because −1 = g³¹² ∈ C₈; and (A) the ±1 autocorrelations sum to a constant, A_{D₀}(w)+A_{D₁}(w) = −2 for ALL 624 nonzero w. Given (S)+(A) a skew-Hadamard matrix of order 1252 EXISTS by Goethals–Seidel — the paper's headline claim, independently confirmed. Our fresh primitive element realizes the paper's exact index sets I₀={4..11}, I₁={0..7} at cyclic offset 0. All arithmetic is exact (finite-field, no floating point); LLMs propose nothing, the exact procedure decides. Honest scope: this certifies the difference-family prerequisites the paper proves — the mathematically load-bearing core — not the explicit 1252×1252 matrix or its GF(2)/GF(3)/GF(5) rank invariants, which need the paper's array / artifact bundle.
Open the ledger →Cycle 17
The first cross-kernel amplification in the ledger: a result already decided by the Lean 4.31 kernel, independently re-decided by a SECOND trusted core — the Rocq 9.0 (Coq) kernel. Guo and Krattenthaler (2014, J. Number Theory 135, 167–184, arXiv:1301.7651) proved three binomial divisibilities that hold for every positive integer n: 6n−1 divides both C(12n,3n) and C(12n,4n), and 66n−1 divides C(330n,88n). Leibniz's Lean census (cycle 13 / PR #293) kernel-decided these as certified instances. Here the SAME 17 instances — (6n−1)∣C(12n,3n) and (6n−1)∣C(12n,4n) for n=1..8, and (66n−1)∣C(330,88) — are re-decided by the Rocq 9.0 kernel over binary N (Coq's Peano nat cannot hold the ~90-digit C(330,88)), each by `vm_compute; reflexivity`, and confirmed AXIOM-FREE by Rocq's own separate library checker `rocqchk`, whose whole-development CONTEXT SUMMARY reports `* Axioms: <none>` and no unsafe constructs. Two independent kernels agreeing on the same arithmetic is strictly stronger evidence than either alone — an independent kernel catches translation and kernel-specific errors a single-checker pipeline cannot. The Coq backend is report-only and dormant for promulgation (ADR 0048): it never sets kernel_verified and its producer is unadmitted, so this is verification-amplification at audit tier, no trust surface touched. LLMs propose nothing; both kernels decide, and math.comb is a third, independent cross-check.
Open the ledger →Cycle 16
A new faculty for the daemon: independent re-decision of a proof in a SECOND and THIRD kernel. Leibniz's proof edge had one arbiter, the Lean 4.31 kernel. This cycle adds report-only backends for the Rocq 9.0 (Coq) and Isabelle2025 kernels, so a published result can be re-decided in a different trusted core — strictly stronger evidence than re-running the same one, because an independent kernel catches translation and kernel-specific errors a single-checker pipeline cannot. Both are LIVE for verification-amplification (audit tier) and DORMANT for promulgation: they never write kernel_verified, mint no proof edge, and — until an operator admits their producer strings under the ADR 0041/0045 allowlist ritual — the trust policy rejects any Coq/Isabelle proof edge structurally, so the trust boundary is unchanged (all four structural guards stay byte-identical). The backends genuinely GATE, not rubber-stamp: on the demo certificates each kernel accepts real theorems (Coq's add_comm / app_assoc / rev_involutive; Isabelle's add_comm / rev_rev / Gauss's summation) and REJECTS both self-laundered proofs (Coq `Admitted`; Isabelle `sorry`) and broken proofs. A three-round adversarial review (six false-PASS holes found and closed, each pinned as a regression test) drew a hard, honest line between the two kernels' trust. For Coq the axiom audit is KERNEL-DRIVEN AND SOUND: after compiling, the backend runs Rocq's own library checker `rocqchk`, which reports the whole development's axioms and unsafe constructs name-agnostically, with the authentic verdict fenced off by an unforgeable random nonce the compiled source cannot read; a final 25-attack validation could not certify a single proof of False. For Isabelle, which exposes no such report reachable without ML, the check is a comprehensive source blocklist that is NOT adversarially sound (each review round found a fresh route: a cheat tactic, then a setup-ML axiom injection, then a code_printing + eval); it is therefore scoped to trusted-provenance amplification only, with a kernel proof-term audit recorded as the blocking prerequisite for any Isabelle promotion. LLMs propose nothing here; the kernels decide, and the daemon reports what they said.
Open the ledger →Cycle 15
An independent kernel verification of the finite core of a freshly-resolved $1000 Erdős problem. Erdős Problem 707, the Sidon-Extension Conjecture, asserts that every finite Sidon set (a set of integers whose pairwise differences are all distinct) extends to a finite perfect difference set — a set B in ℤ_v of size n, with v = n²−n+1, in which every nonzero residue is a difference exactly once. Erdős posed it repeatedly from 1976 with a $1000 reward, and it stood for nearly 50 years. Alexeev and Mixon (arXiv:2510.19804, October 2025) disproved it: the size-5 Sidon set {1,2,4,8,13} extends to no perfect difference set (as does Hall's 1947 set {1,3,9,10,13}, which predates the conjecture). Niu (arXiv:2604.25214) then exhibited size-4 candidates {0,1,3,11} and {0,1,4,11} that fail to extend for every modulus v ≤ 133, evidence that the smallest non-extending Sidon set has size 4. LLMs propose nothing here; the Lean 4.31 kernel decides. The key reduction is that a perfect difference set of order n satisfies n(n−1) = v−1, so a size-n set in ℤ_v is a perfect difference set precisely when its pairwise differences mod v are all distinct; hence non-extension at a given order is a bounded, decidable fact — no size-n superset of S is Sidon mod v. We kernel-decide, for each of the four counterexample sets and with no axioms: that it is a Sidon set; that it does not extend to a perfect difference set at order |S| (the set reduced mod v is not one); and that it does not extend at order |S|+1 (adjoining any single residue never yields one). Our instrument additionally reproduces the non-extension for all orders with v ≤ 43, a faithful slice of the papers' unconditional exhaustion. Honest scope: non-extension to ANY finite perfect difference set is an infinite claim, established non-finitely by the polarity argument (the size-4 case remains conjectural); we certify the finitely-checkable core.
Open the ledger →Cycle 14
An independent kernel verification of a monomial-ideal result, on the general monomial-ideal instrument. Mafi and Naderi (2021, 'Integral closure and Hilbert series of a special monomial ideal', arXiv:2112.02921) study M_{n,t} = (x^{e_1},…,x^{e_n}), where x^{e_i} is the product of all variables except the i-th, each to the power t. Their Theorem 1.6 says the integral closure of M_{n,t} is a Veronese-type ideal; for three variables this is closure(M_{3,t}) = {x^u : min(a,t)+min(b,t)+min(c,t) ≥ 2t}. Their Corollary 1.7 says M_{n,t} is Cohen–Macaulay (unmixed), yet its integral closure has embedded associated primes. LLMs propose nothing here; the Lean 4.31 kernel decides. Using our exact integral-dependence instrument we confirm, for n = 3: (Theorem 1.6) the computed integral closure equals the Veronese cap-sum ideal, cross-checked for t = 1,2,3,4; and (Corollary 1.7) the closure has the embedded prime (x,y,z) for t ≥ 2 — witnessed by a monomial u that is not in the closure but whose product with each variable is (for t = 2 the witness is xyz) — while M_{3,t} itself has no such witness and is unmixed, so the integral closure GAINS an embedded prime the original ideal lacks. An honest detail our check surfaces: at t = 1 the ideal is the squarefree Veronese, already integrally closed and with no embedded prime, so the phenomenon begins at t = 2. Verdict: agreement — no erratum. Six theorems, kernel-decided by `decide`, standard axioms. This is a second independent verification on the general monomial-ideal instrument, after Ataka–Matsuoka.
Open the ledger →Cycle 13
An independent kernel verification of a Journal of Number Theory result. Guo and Krattenthaler (2014, 'Some divisibility properties of binomial and q-binomial coefficients', J. Number Theory 135, 167–184, arXiv:1301.7651) prove two headline facts. First, three new divisibilities that hold for every positive integer n: 6n−1 divides both C(12n,3n) and C(12n,4n), and 66n−1 divides C(330n,88n). In the paper these follow from a deeper phenomenon — the divisibility and positivity of quotients of q-binomial coefficients by q-integers, generalizing the positivity of the q-Catalan numbers. Second, they confirm a conjecture of Z.-W. Sun: if a has a prime factor that does not divide b, then there are infinitely many n for which bn+1 does NOT divide C((a+b)n, an) — in contrast with the Catalan case a=b=1, where n+1 always divides C(2n,n). LLMs propose nothing here; the Lean 4.31 kernel decides. This Phase-1 census kernel-decides the three divisibilities as certified instances (for a range of n, up to the ~90-digit C(330,88) which the kernel handles via sub-term sharing) and confirms Sun's conjecture by explicit non-divisibility witnesses for six qualifying pairs (a,b). All 23 theorems are decided by `decide` over exact Nat.choose and depend only on the standard axiom propext. This target was chosen because it reuses, verbatim, the from-scratch Gaussian-binomial machinery Leibniz built for the Problem-16 self-ordered proofs (the q-Pascal recurrence and q-factorial divisibility) — the same q-integer positivity that underlies Guo–Krattenthaler; the all-n theorem (Phase 2) is the natural follow-on.
Open the ledger →Cycle 12
Cahen–Fontana–Frisch–Glaz Problem 16 (Chabert) asks for the natural self-ordered integer sequences. A sequence a is self-ordered when its factorial D_n = ∏_{k<n}(aₙ − aₖ) divides P(m,n) = ∏_{k<n}(aₘ − aₖ) for all m and n. This is an infinite condition, so our earlier census could only refute it or give bounded evidence for the positive cases. Here we cross that line and PROVE the positive side, in the Lean 4.31 kernel, for an entire class. First, the identity sequence aₙ = n is self-ordered: its factorial is D_n = ∏_{k<n}(n − k) = n!, and n! divides the product of any n consecutive integers ∏_{k<n}(m − k) — the standard factorial-divides-descending-factorial fact, with the case m < n handled by a zero factor in the product. Second, and generally, EVERY arithmetic sequence aₙ = α + βn is self-ordered: each factor (α+βx) − (α+βk) equals β(x − k), so both D_n and P(m,n) factor as βⁿ times the identity factorial; the shared βⁿ cancels and the claim reduces to the identity case. Corollaries instantiate the census's self-ordered arithmetic sequences — n, 2n, and 3 + 5n — as theorems, upgrading them from 'self-ordered up to N = 30 (evidence)' to proofs. And the harder geometric case is now closed too: every geometric sequence aₙ = qⁿ (q an integer) is self-ordered. Factoring qⁿ − qᵏ = qᵏ(q^{n−k} − 1) reduces the divisibility to the fact that the Gaussian binomial coefficient is an integer; since Mathlib has no Gaussian binomials, they are built from scratch (a ℤ-valued q-Pascal recurrence, with the product identity proved by induction). All seven theorems depend only on the standard axioms (propext, Classical.choice, Quot.sound); the proofs are complete, with no compiler-trusted shortcuts. Together with the census refutations (n³, n⁴, factorial, Fibonacci, primes), Problem 16 now has a certified negative side and two proved positive classes — arithmetic and geometric. LLMs propose nothing that counts here; the Lean kernel decides every step. (The mechanical route — a hosted Goedel-Prover — timed out on the geometric goal, which was then closed by hand with the q-factorial machinery, recorded honestly.)
Open the ledger →Cycle 11
Cahen–Fontana–Frisch–Glaz Problem 16 (Chabert) asks for the natural self-ordered integer sequences. A sequence a is self-ordered (Adam–Cahen–Fares simultaneously ordered) when its factorial D_n = ∏_{k<n}(aₙ − aₖ) divides P(m,n) = ∏_{k<n}(aₘ − aₖ) for all m and n. Self-ordered is an infinite condition, so it cannot be certified by a bounded computation — but its negation is finitely witnessed: one pair (m,n) with D_n not dividing P(m,n) refutes it, and that is a kernel-decidable fact. This census screens a curated set of natural sequences and kernel-certifies the refutations. Five natural sequences are certified NOT self-ordered: n³ (witness m,n = 3,2), n⁴ (4,3), the factorial (n+1)! (3,2), the Fibonacci numbers (4,3), and the primes (3,2). Each certificate hardcodes only the short value prefix its witness needs, so polynomial, factorial, Fibonacci, and prime sequences are all handled uniformly, with no symbolic sequence definition required. The five sequences that pass are self-ordered up to N = 30 (bounded evidence, not a proof): the identity n, the arithmetic 3+5n, n², the triangular numbers, and 2ⁿ. A correction rides along: an earlier loose framing had listed 'refute {n²}' as an angle for this problem — that is wrong. n² is self-ordered up to N = 30; the refutable pure powers are n^k with k ≥ 3. Notably, three of the most natural non-polynomial sequences — the factorials, the Fibonacci numbers, and the primes — are certified NOT self-ordered, honest evidence about where self-ordering does not come from. LLMs propose nothing; the Lean kernel decides. These are certified instances of an open classification, not a classification.
Open the ledger →Cycle 10
Cahen–Fontana–Frisch–Glaz Problem 41 (Swanson) asks to classify the triples (a,b,c) for which I = the integral closure of (x^a,y^b,z^c) in k[x,y,z] is normal (every power integrally closed). The full classification is open. This is not a classification — it is a certified census: the exact normal / not-normal verdict for every corner triple with 1 ≤ a ≤ b ≤ c ≤ 9 (taken up to coordinate-permutation symmetry), each non-normal one carrying an axiom-free Lean `decide` witness x^u in closure(I²) minus I². Of 165 triples, 11 are not normal; all 11 non-normality certificates are kernel-verified with no axiom dependencies at all. The headline observation: the two smallest non-normal corner ideals, by a+b+c = 12, are (2,3,7) and (3,4,5) — both strictly smaller than the textbook Huneke–Swanson (4,5,7); and (2,3,7) is exactly the Ataka–Matsuoka (2026) sharpness witness, the integral closure of (x⁷,y³,z²), up to permutation. So the sharpest generator-count counterexample in their paper is simultaneously the minimal non-normal corner ideal — two extremal characterizations meeting at one ideal. Within the census range every non-normal triple has distinct coordinates and a ≥ 2, and 10 of the 11 are pairwise-coprime (the sole exception is (5,6,8)); these are honest observations about the open classification, offered as certified data, not a competing classification. LLMs propose nothing; the Lean kernel decides.
Open the ledger →Cycle 9
A second independent kernel pass over Ataka and Matsuoka (arXiv:2602.01782), this time on the illustrative Example 4.7 (§4.3, reduction numbers of normal ideals) — and it surfaces a kernel-checkable erratum. We built a general monomial-ideal normality instrument for k[x,y,z] that decides everything by the integral-dependence definition (x^u ∈ I^p iff some multiset of p generators sums ≤ u; x^u ∈ closure(I^p) iff x^{ku} ∈ I^{pk} for some k; and normality by the Reid–Roberts–Vitulli reduction, d = 3). It is cross-validated against the corner-ideal checker, the Example 4.5 sharpness result, and exact linear-programming membership. On Example 4.7 it finds: 4.7(1), I = (x³,y²,z²,xy,xz,yz), is normal as stated (a positive control); but 4.7(2), I = (x³,y³,z³,x²y,xy²,x²z,yz), stated to be 'a normal ideal by Theorem 3.1', is NOT integrally closed. The monomial xz² is not in I, yet its square (xz²)² = x²z⁴ = (x²z)·(z³) lies in I²; a monomial whose square lies in I² is integral over I, so xz² is in the integral closure of I but not in I. Hence I is not normal in the standard sense (a normal ideal satisfies I = Ī), and Theorem 3.1 — which requires I = Ī and μ(I) ≤ 7 — does not apply as printed; the actual integral closure has eight minimal generators. All of this is kernel-decided by `decide` with no axiom dependencies. The erratum is a slip in an illustrative example and is independent of the paper's Main Theorem, whose sharpness (the μ(I) ≤ 7 bound, witness closure(x⁷,y³,z²)) we verified and confirmed correct in the previous cycle. LLMs propose nothing here; the Lean kernel decides.
Open the ledger →Cycle 8
An independent kernel verification of a February-2026 result. Ataka and Matsuoka (arXiv:2602.01782) prove that an integrally closed monomial ideal I in k[x,y,z] with at most seven minimal generators is normal (every power integrally closed), and that the bound seven is sharp. Their sharpness witness (Example 4.5) is I = the integral closure of (x⁷,y³,z²): it has eight minimal generators and fails to be normal. LLMs propose nothing here — the paper's claim is the object, and the Lean 4.31 kernel decides. From the Newton polyhedron (weights (6,14,21), L = lcm = 42) we reproduce BOTH load-bearing facts and cross-check them verbatim against Example 4.5: the eight minimal generators (x⁷, y³, z², x⁵y, x³y², x⁴z, y²z, x²yz), and the non-normality witness x⁶y²z, which lies in the integral closure of I² (weighted degree 85 ≥ 2L = 84) but not in I² itself, so by the Reid–Roberts–Vitulli reduction (in three variables, normal ⇔ I and I² integrally closed) the ideal is not normal. All three theorems are decided by `decide` with no axiom dependencies at all. A built-in erratum guard refuses to emit the certificate unless the generator count, the generator set, the verdict, the witness monomial, and the weight vector all match the transcribed paper — the same discipline that caught a real erratum in the SS-RS-GD COLT refutation. Verification-amplification on the flagship Problem-41 instrument; no trust surface is touched. A companion research pass (paper-grounded, adversarially faithfulness-checked) records that the three resolved commutative-ring candidates 30a, 30b, and 9 are NOT finite-decidable counterexamples — 30a (Secord 2023) and 30b (Choi–Walker 2016) were resolved positively, and Problem 9 (Haotian Ma 2026) has an intrinsically infinite counterexample — so the domain's growth runs through open monomial questions, not the resolved n-absorbing ones.
Open the ledger →Cycle 7
The Erdős statement-formalization lane, applied to a first operator-picked batch. The Erdős database is dominated by asymptotic problems the kernel cannot decide, so the contribution is faithful Lean STATEMENTS (not solutions), each passing a faithfulness gate: the conjecture Prop elaborates, a faithfulness anchor holds, and a non-vacuity note records the load-bearing quantifier structure. Erdős–Straus (open): for every n ≥ 2, 4/n is a sum of three unit fractions — anchored by the concrete 4/5 = 1/2 + 1/4 + 1/20. Erdős–Ginzburg–Ziv (theorem, 1961): among any 2n−1 integers some n have a sum divisible by n. Erdős–Szekeres (theorem, 1935): an injective real sequence longer than r·s has a strictly-monotone subsequence of length > r or > s — here the statement is PROVED, being exactly Mathlib's `erdos_szekeres`. Erdős–Turán on APs (open, 1936): if the reciprocals of a set of positive integers diverge, the set contains arbitrarily long arithmetic progressions. Statements are sourced from the mathematical literature, not scraped from erdosproblems.com (their AI-contribution policy is respected). Each file downloads verbatim (verify the SHA-256) and re-verifies against Lean 4.31 + Mathlib.
Open the ledger →Cycle 6
A reusable certify(object) interface over the finite/exact-decidable open-problem counterexamples — a sibling of the process-complexity and code-bound certificate domains. This cycle publishes the two new Tier-1 families (monomial-normality (4,5,7) is Cycle 5). self_ordered (Cahen–Fontana–Frisch–Glaz Problem 16, Chabert): the sequence {n^3} is NOT self-ordered — an explicit witness at (m,n)=(3,2), where D_2 = 56 does not divide the corresponding product 702 — while the triangular numbers and the powers of two are certified self-ordered up to a bound. n_absorbing (Problem 30, Anderson–Badawi): the absorbing number of the zero ideal in Z/m, absorbingNumber(⊥ : Z/4) = 2 and absorbingNumber(⊥ : Z/9) = 2, each a decide over Fin(k+1) → ZMod m. Every certificate is kernel-decided with only the standard axioms (or none), names the fact it attests, and downloads verbatim (verify the SHA-256).
Open the ledger →Cycle 5
Cahen–Fontana–Frisch–Glaz Problem 41 (Swanson) asks to classify the triples (a,b,c) for which every power of I = integral closure of (x^a,y^b,z^c) is integrally closed (I normal). The full classification is open, but two finite reductions make certifying a specific triple a decidable kernel computation: the Newton-polyhedron membership test (closure-membership is an exact integer inequality on the lcm-cleared weighted degree) and the Reid–Roberts–Vitulli reduction (in three variables, normal ⇔ I and I² integrally closed). We certified the Huneke–Swanson boundary point (4,5,7) as NOT normal: the monomial x²y⁴z⁵ lies in the integral closure of I² (weighted degree 282 ≥ 280 = 2L) but not in I² itself, so I² is not integrally closed and I is not normal. Kernel-decided by decide with NO axiom dependencies at all, in both a collapsed 90-case and a direct 8100-case product-definition form. Shipped as a reusable is-(a,b,c)-normal? checker — certified instances, not a competing classification (active current work: Ataka–Matsuoka, arXiv:2602.01782, 2026).
Open the ledger →Cycle 4
Yun–Sra–Jadbabaie (COLT 2021) asked whether single-shuffle SGD can beat reshuffle SGD and GD in the well-conditioned regime (Conjecture 1.1). A pipeline-math write-up refutes the SS–RS half at (n,K)=(3,2). We kernel-verified the refutation's algebraic core against Lean 4.31: the gap identity (1.8), the positivity of its final factor, the violation λ_SS > λ_RS on the interval, and a fully concrete witness at q=1/2 — every headline theorem with only the standard axioms. Conjecture 1.1 is machine-refuted. Two by-products of routing it through the kernel: an LLM scout's claim that a sum-of-squares identity was wrong was itself refuted (the paper is correct — the scout dropped a cross-term); and the paper's supporting identity (1.7) was found NOT to hold as printed (Lean ring plus an independent exact-rational check agree), a supporting-lemma erratum that does not affect the main result (the inequality λ_RS ≥ μ_RS it targets still holds). The erratum was reported upstream.
Open the ledger →Cycle 3
The pipeline-math repository resolves four open problems from Cahen–Fontana–Frisch–Glaz (Problems 4b, 20, 27b, 30c) with GPT-5.5-Pro-generated Lean 4 proofs. We audited all four two ways: a faithfulness audit — do the frozen Lean statements capture the actual open problems, and are the counterexamples' defining properties proved rather than assumed? — and an independent lake build re-verification against the Lean 4.31 kernel. Verdict: all four are complete, sorry-free, and faithful; every headline theorem's #print axioms is exactly {propext, Classical.choice, Quot.sound}. The definitions match the literature (Anderson–Badawi absorbing ideals; Glaz finite-conductor / quasi-coherent), the counterexamples are genuine (real Module.Basis, explicit generators, honest separating functionals), and hypotheses are non-vacuous. A small upstream fix for stale completion comments was contributed.
Open the ledger →Cycle 2
An external formal-verification pass over the MCR whitepaper — its four theorems and the §13 conclusion, adjudicated by machine, not by judgement. Eight problems (P1–P8) were checked with Z3 4.16.0 and the Lean 4.31 kernel. Theorem 1 is the free theorem, holding even for a no-op stub (vacuous); the universality syllogism is invalid (Z3 countermodel); the order-1 error floor min(q, 1−q) > 0 is proven (Z3 UNSAT on its negation); the derivability claim collapses to 0 = 1 on the integers (Lean, 0 sorry); the entropy bound is ill-posed (a hapax exceeds log₂N by ~13 bits); the sample-complexity bound is true but weaker (O(N ln N) survives the union bound). The §13 AGI conclusion is left NOT-PROVEN — unsupported, not shown false — and one genuinely-true, exponentially-costly weaker statement (P8) is proven as the honest thing the work can build from. Nothing in Theorems 1–4 supports the AGI conclusion; every verdict is backed by a re-runnable artifact.
Open the ledger →Cycle 1
An illustrative cycle showing the work-log format: six seeds surveyed over the analysis-of-algorithms frontier, candidates quarantined with their reasons, one law promulgated.
Open the ledger →