Toward a machine-checked proof of the claimed Sandier-Serfaty certificate: 4 of 12 stages re-executed in the Lean kernel, one reduction lemma proved, and the measured cost of the rest (a partial formalization; the conjecture is not formally proved)

The Sandier–Serfaty conjecture asks whether the triangular lattice minimizes the renormalized Coulomb energy of a planar point set against a uniform background. A preprint in the openai/math release (AI-generated, not peer reviewed) claims a proof from an analytic reduction plus a finite certificate in exact interval arithmetic with twelve stages. An earlier record (doi:10.5281/zenodo.23653827) reproduced that certificate by running its C++ code. This record starts to formalize it in Lean 4 and reports exactly how far that went. The conjecture is not formally proved, and nothing here says that it is. Two checking levels. L1 (kernel re-execution): a Lean transcription of a stage's interval computation, evaluated by the Lean kernel (decide +kernel, no native_decide), gives bit for bit the integer endpoints printed by the C++ binary. L2 (real-number statement): a Lean theorem that a real number lies in the interval. A third, weaker level E: the executable assertions evaluated on the exact C++ endpoints (arithmetic about given integers only). Counts, from the saved logs. 4 of 12 stages are complete at L1 (init_constants, bcons/eps, calcLam, calcK; calcLam and calcK conditional on the table enclosures, which are premises, and bcons on the lattice coefficients). 1 of 12 is complete at L2 (init_constants: log 2, pi, p, R0, a as real numbers). Together the ported stages re-execute 1,685,129 of 1,238,829,689 interval multiplications and inversions of the C++ run (0.136 %). All 22 printed integer pairs and every assertion that the C++ makes after calcK (lambda range, K<0, f(l)>0, slope, the two global_grid assertions, the inside_hess minima) plus the |c_1|<1 check are kernel-checked as arithmetic on the exact endpoints (level E); the core_test bound check of stage 4 (core.hpp:274) is not covered, and the table separation check is checked only window by window. Two theorems added after the audit (ChainLink.lean) tie the stage-8 slope and f(l) literals to the L1 outputs. Eleven planted false claims are rejected (three must-fail files, rc 1), each mapped to one planted theorem, and the honest refutations are kernel-checked theorems. The chunk tiling of the stages is guaranteed by the generator, not checked in Lean (a script finds the ranges contiguous). One reduction lemma. The manuscript's Lemma dual:signed-endpoints is proved completely in Lean as signed_endpoints (Lean statement and the manuscript's wording side by side), with an algebraic step of the assembly proposition and a numerical fact; the lemma is stated for an abstract kernel G and is not connected to the certificate. Of the 31 numbered reduction steps audited earlier, one is complete in Lean and the algebraic part of a second. Cost of the rest. L1 for the unported computations (stage rows 2-4 and 9-12) is projected at about 854-2,240 core-hours (counts from an instrumented C++ run times measured kernel rates, at a machine load average of 12-16; the lower end is not conservative: an independent rebuild on a quiet machine compiled 2.2-2.7 times faster, so 854 is not a lower bound); the larger gap is L2 for the analytic content and the reduction, a multi-month project. LeanFlow gained a fail-closed decide_kernel tactic (94 tests pass). Limitations. One AI agent wrote the generators and the Lean files. A separate AI agent instance (not a person) audited the work (AUDIT.md, verdict ACCEPT_WITH_CORRECTIONS): it rebuilt 13 modules from source with byte-identical oleans, re-ran the three must-fail files and the axiom aggregates and type-checked Chain.lean; the other 28 chunk files, CalcK.lean and CalcLam.lean were not rebuilt independently. Some endpoints come from an instrumented copy of the C++ (counters and endpoint prints only); no human has audited any statement. The Elenchus ledger gate reports 0 blocking findings and 16 flags (exit code 1), one LEDGER_UNAUDITED_TIER_A for each Tier A row; they stay open because an agent audit is not a person's certification. Everything resting on the openai/math manuscript is conditional on it.