SeverinVisionary
Follow
doc-batch-gradients measures how much gradient noise whole-document long-context batches add, on open Pythia and OLMo-2 checkpoints. Within-document gradient correlation reaches out to 16K tokens. On code repositories this makes a 16K-token batch behave like roughly 3.5–5× fewer independent samples than packed web text (about 2× for arXiv, small for books). The work is preregistered, the results are released, and everything runs on CPU.
Contact: hanyu.yang.92@gmail.com
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 i…
Python
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 n…
Python
Lean 4-verified lower bound for binary twofold covering codes: K(8,1,2) >= 61, plus an elementary even-n theorem improving five published bounds. First unknown term of OEIS A004045.
Python
Settling Conjectures 10.1, 10.2 and 10.3 of Althofer et al., Alternating plane graphs (Ars Math. Contemp. 8, 2015)
Python
Site root for severinvisionary.github.io: an index of the certified-mathematics deposits, the host-level robots.txt, and the sitemap index over every project landing page.
HTML
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
Python
