An independent research program in machine-verified mathematics · github.com/05oz/certify · daniel@halfounce.io
The program was founded in 2026. The program publishes results in combinatorics, quantum error correction, and algebraic geometry; every published claim is accompanied by a certificate that can be replayed by the reader — most with the Python standard library alone — and every release records its dated prior-art review. Recent results include the exact logical error probability of the rotated surface code under a lookup-table decoder at distances 3 and 5, in a regime too rare to reach by direct simulation, the determination of a previously unknown value in Erdős Problem #112 (the oriented Ramsey number k(3,4) = 21), the first machine-checkable determination of the minimum distance of the [[288,12,18]] bivariate-bicycle code, the verification of Kelmans' 1984 packing problem over all 3-connected cubic graphs on at most 22 vertices, the first certified determination of the tournament packing numbers ν₃(9) and ν₃(10), extending a record established in 2004, and a certificate-backed automorphism exclusion for the [[14,3,5]] code existence question, open since 2005.
Computation is performed with AI systems operating under an adversarial verification protocol: results are independently re-derived with separately written code, checked against the primary literature before any claim is made, and released only with their machine-checkable certificates. The protocol, rather than any single computation, is the program's contribution to method. The organising principle is unchanged from the first release: a computational claim should travel with a witness that a reader can check independently, without repeating the search and without trusting the software that found it.
The library lists every preprint and note this program has released, newest first, each with its PDF, its certificates, its dated prior-art record and its archival DOI. That list is maintained in one place only, so that no second copy of it can fall out of date; nothing appears in it before the artifacts a reader would need to check it are public.
Every published claim is accompanied by the script that establishes it. The scripts assert their results and fail loudly; the certificates are short enough to check by hand-written code with no solver in the loop.
git clone https://github.com/05oz/certify cd certify python3 -m venv venv && venv/bin/pip install sympy venv/bin/python scripts/core_verify.py # the map, its Jacobian, the collisions venv/bin/python scripts/cover_verify.py # the cover and the image theorem venv/bin/python scripts/weyl_verify.py # the Weyl-algebra endomorphism
Reproducing the Gröbner-basis certificates additionally requires msolve. Instructions are in the repository. The commands above are the entry point for the Alpöge Keller work; each further result ships its own checker alongside its certificates, indexed from the repository README.
Corrections, prior references, and counterexamples are welcome and will be credited. If a result here is already known, a pointer to the source is the most useful thing you can send.