Lean 4 kernel checks of three published combinatorial constructions: kissing configurations in dimension 32, a Ramsey colouring for R(5,15), and nine constant-weight codes

Summary This note gives Lean 4 kernel checks of constructions published by other authors. It states no bound of its own. The bounds in the table are those stated by the cited authors; this note only checks them. Each theorem is proved with core Lean 4.35.0 and no Mathlib. #print axioms reports only propext, Classical.choice and Quot.sound. No sorry, native_decide, implemented_by, extern or added axiom is used. BoundConstruction (credit)Lean theoremtau_32 >= 347584Shuxing Yang et al., arXiv 2609.35051KissA.kissing32_ge_347584tau_32 >= 352320Qihong Lin, Zenodo 23552484KissB.kissing32_ge_352320R(5,15) >= 279Arhan Canli, github.com/arhancanli/quantavane-ramsey-records at commit 21ede2cR515_finalA(n,6,w) >= M, nine cells listed belowChris Dzoba, arXiv 2610.24025v1 ancillary filesDzX.final, one per cell The nine code cells (n, w, M): (24,12,5566), (27,11,19305), (27,12,24804), (27,13,27783), (28,9,11388), (28,10,19110), (29,9,14781), (29,10,27183), (29,11,42042). Statements Kissing: K integer vectors in Z^32, each of squared norm 32, with pairwise inner product at most 16. In both cases K = 2^17 + 128m + 1984, where m is the number of weight-8 supports (m = 1676 for 347584, m = 1713 for 352320). Scaling to unit length gives K points at pairwise angle at least 60 degrees. That scaling step is prose and is not in Lean. Ramsey: the circulant 2-colouring of K_278 with the red connection set S given in the source file (|S| = 95; sha256 in MANIFEST) has no red K5 and no blue K15. Codes: each code has exactly M distinct binary words of length n and weight w, with pairwise Hamming distance at least 6. Method, in outline Finite data facts are checked by decide +kernel in chunked modules. General lemmas, proved once, lift the data facts to the stated theorems; each checker used is proved sound in Lean. Checks Every module builds with return code 0; logs are in the archive. A separate Python script recomputes from the source files the stated properties (norms and inner products; clique absence; word count, weights and minimum distance) and agrees with the Lean data. Negative controls (two for the kissing case, two for the Ramsey case, one for the code A(24,6,12)) use deliberately corrupted inputs; each fails in the predicted module. Part of each project was rebuilt a second time from an empty cache: the full kissing case A chain; for Ramsey, the general lemmas, the red-clique module and three of eleven data modules; two of the nine code projects in full. Input sha256 values are listed in MANIFEST files in the archive. Not claimed Exact values; optimality; new bounds; anything about how the constructions were found. Files certificates_kernel3.zip: Lean sources, input files with sha256, MANIFESTs, build return-code logs.