Local Lean formalization permanently registered in Palomar (PALOMAR-2026-08-29-000004). Two-certificate trace-energy deduction for the 67.3316977142% simple critical-line zero research-draft candidate.
Stochastic Electrodynamics (SED) Library
Certified analytic geometry on an explicit K3 surface: a finite holomorphic atlas whose chart domains, transitions and branch continuations are machine-checked rather than asserted. Sixty chart types, exact transitions over Q, outward-rounded arithmetic elsewhere. No Ricci-flat metric claimed. One command checks nine of the fourteen certificates.
Independent exact certification of machine-generated mathematics — exact arithmetic, no code shared with the claimant, refusal as a verdict.
Five volumes, 1,666 pages on the abc conjecture: a global substrate over which Spec Z acquires a base, strain, the Theta-dilation, an unconditional trace-invariance theorem, Theorems A and B conditional on 98 named obligations, and abctk. The abc conjecture remains open. DOI 10.5281/zenodo.23610034.
Certified obstructions and exact forcing for the Earth-Moon and arithmetic Kakeya problems — paper, checkable certificates, full replay.
Five volumes, 1,309 pages on the Hodge Conjecture: algebraicity as a descent datum along a definable prism, twelve axioms, an unconditional equivalence of five formulations, nine obstructions of which two are live. The Hodge conjecture remains open. Open access, DOI 10.5281/zenodo.23597954.
Four volumes, 571 pages on the Birch and Swinnerton-Dyer conjecture: Frobenius–Arakelov–Prismatic spaces, the Master Identity as one determinant line with two trivialisations, a proved conditional descent, twelve conjectures and fourteen obstructions. BSD remains open. Open access, DOI 10.5281/zenodo.23585887.
Four volumes, 1,549 pages on the Riemann Hypothesis: 23 scoped no-go theorems, the Krein Index Theorem, a proved derivation of RH from three unconstructed realization hypotheses, and two obligations posed to be attacked or falsified. RH remains open. Open access, DOI 10.5281/zenodo.23564898.
Certified companion to the Dixmier counterexample in A3 + explicit Poisson-conjecture witness (runnable exact-arithmetic certificate)
Certified exact-integer verifier and certificate for prime-power threshold cutoff tail bounds.
Bernstein's constant to ten rigorously certified digits: beta = 0.2801694990, proved in interval arithmetic (Arb) where the 1985 Varga-Carpenter rigorous enclosure gives five. OEIS A073001. Every number re-derivable from the shipped data in exact arithmetic.
Companion code for 'The fewnomial ladder': certified root counts for F4/F5/F6, exact resultant+Sturm certificate for M_3>=5
Explicit exact certificates improving the known admissible lower bound for the Belgian Chocolate Problem.
Exactly certified work on Heilbronn's triangle problem: one improved lower bound in the unit disk (n=14), plus a rigidity audit of the unit-square landscape. Every number re-derived from integers in exact arithmetic.
Certified computational study of the gap shape of degree-4 sum-of-squares relaxations of unique games. A null result on the main question, two proved theorems on Paley graphs, and a structural determination of the degree-4 extension. Fully reproducible: 132 checks, 0 mismatches.
Books and research by Jinku Guo: generated natural-number arithmetic, prime operators, Yang-Mills mass gap, Standard Model structure, emergent gravity, cosmic structure formation, and P versus NP research through certified polynomial-cost computation. Papers, Lean proofs and V5 numerical code.
Open, fully rigorous re-certification of White's lower bound for Erdős's minimum-overlap problem (#36), with an independent verifier
Settling Conjectures 10.1, 10.2 and 10.3 of Althofer et al., Alternating plane graphs (Ars Math. Contemp. 8, 2015)
Certified adaptive-order Matérn Gaussian-process inference with uniform likelihood, posterior, and gradient bounds
To associate your repository with the certified-computation topic, visit your repo's landing page and select "manage topics."