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.
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 verifies fourteen certificates.
Stochastic Electrodynamics (SED) Library
Dense solver for general linear equality systems Ax=b with certified status classification: unique, infinite, inconsistent, or undecidable with a supported rank interval
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 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.
The Koras-Russell cylinder as an affine modification of A^4 — a commuting square through a motivic 4-sphere, a one-point Borel-Moore defect, and a machine-certified verification layer anyone can re-run in one command
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)
Companion code for 'The fewnomial ladder': certified root counts for F4/F5/F6, exact resultant+Sturm certificate for M_3>=5
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.
Explicit exact certificates improving the known admissible lower bound for the Belgian Chocolate Problem.
Certificate-based results in physics and astronomy: verification artifacts and the programs that check them.
Certified inertia and eigenvalue counting for symmetric matrices, in Arb ball arithmetic
Certified adaptive-order Matérn Gaussian-process inference with uniform likelihood, posterior, and gradient bounds
Experimental formalization and algorithmic investigation of the Belgian Chocolate threshold, including computability-oriented constructions and endpoint analysis. Not a complete solution of the original Belgian Chocolate Problem.
A floor under Newton's inequality: the sharp constant 4/5, and large parts of Sibuya's 1988 conjecture. Machine-checked, independently validated, reviews included.
Explicit group-invariant colourings improving three lower bounds in section 7.1(a) of the dynamic survey Small Ramsey Numbers: R(4,4,4;3) >= 84, R(4,6;3) >= 64, R(5,5;4) >= 36
To associate your repository with the certified-computation topic, visit your repo's landing page and select "manage topics."