computer-assisted-proof

A software that assists a previous version of the proof of Gerver's conjecture, using a custom geometric branch-and-bound algorithm, and the exact rational QP solver powered by CGAL

An interval library for OCaml

A Lean 4 formalization of the ternary (weak) Goldbach theorem, with an explicit audited finite and computational trust boundary.

Efficient Encoding of the Queen Domination Problem into SAT Using Hilbert Curve Ordering, Static Symmetry Breaking and CnC

Open-source re-implementation of DeepMind's unstable singularity detection methods using PINNs for blow-up solutions in fluid dynamics

Executable certificate framework for a proof candidate of Graham’s rearrangement conjecture / Erdős #475, with local branch checkers and reproducible audit scripts.

The Multi Agent Transportation Problem: Solvers, Evaluations, and Computer-Assisted Proofs

Complete reproducible working-proof chain and exact verification materials for Dittert’s conjecture (all dimensions; under review)

Computer-assisted proof that the minimal superpermutation on six symbols has length 872. Machine-checked evidence ledger, adversarial audits, 15-second verification path. Preliminary.

Calibrated residual-landscape survey of the linearized Navier–Stokes operator at the Hou–Wang–Yang self-similar profile

Open, fully rigorous re-certification of White's lower bound for Erdős's minimum-overlap problem (#36), with an independent verifier

Computer-assisted proofs and clean-room audits for the r=10 and r=11 fixed cases of Erdős Problem 617.

Exact computer-assisted proof candidate for octahedron comparison in geodesic CAT(0) spaces

Computer-assisted proof and reproducibility package for Erdős Problem 848, with exact certificates and separately implemented checkers.

Computer-assisted proof that the 7₂ knot regulator integral in Ramanujan Challenge 3.1 equals 4π²/85.

https://en.wikipedia.org/wiki/Proof_assistant; 一錯特錯錯到底! 爆炸原理是重哪來的?

Proof claims and reproducible verification for the r=5,6,7,8 cases of Erdős Problem 617.

An independent structural proof excluding the (72,108) case of the plane Jacobian Conjecture (GGHV, arXiv:2204.14178) — conditionally raising the counterexample degree bound from 108 to 125. Priority for the exclusion is B. Helali's (doi:10.5281/zenodo.21479814). Exact sympy checkers, spec-only auditors, Lean-certified core identity.

Frankl's union-closed conjecture beyond cyclic symmetry: deciding transitive-invariant families without a full cycle on 14+ points, with SAT certificates. Sequel to frankl-cyclic-sat. Work in progress, run by a Claude Code agent loop.

Reproducible computer-assisted proof for unboppy balanced binary rotors of fundamental period 24