Hanyu Yang — certified mathematics deposits
Machine-checkable results, each with a public certificate, a reproduction command and a DOI. Every claim below is checked by something other than the author's judgement, and each deposit states what it does not establish.
Bernstein's constant: ten rigorously certified digits
β = 0.2801694990 — ten
correctly-rounded decimal places, proved in Arb interval arithmetic, where the
1985 Varga–Carpenter rigorous enclosure determines five.
DOI 10.5281/zenodo.22106774 · repository · OEIS A073001 · dataset, 26 Aug 2026
Twofold coverings of the Hamming cube: a Lean-verified K(8,1,2) ≥ 61
61 ≤ K(8,1,2) ≤ 64 — the lower bound
formalised in Lean 4 with zero sorrys, plus an elementary
even-n theorem improving five published lower bounds.
DOI 10.5281/zenodo.22217672 · repository · OEIS A004045 · software, 3 Sep 2026
Heilbronn's triangle problem in the disk: a certified n = 14 construction
α_disk(14) ≥ 0.0767158857710289397517847755066…
— an explicit 14-point configuration in exact integer coordinates, about +1.075%
above the best earlier documented value; a certified lower bound, not a proved
record.
DOI 10.5281/zenodo.22091169 · repository · dataset, 25 Aug 2026
Three conjectures on alternating plane graphs, settled
Conjectures 10.1, 10.2
and 10.3 of Althöfer et al. (2015) closed — 10.1 proved
unconditionally, the other two by machine-checked witnesses at every order they
claim one for. The fourth problem stays open, and the deposit says why.
DOI 10.5281/zenodo.22269200 · repository · the source paper · software, 2 Sep 2026