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.

Disk covering problem (disc covering): global optimality proof claims for n = 11-20, exact certificates, Chinese proofs, and reproducible verification code. External review pending.

Stability of regular N-vortex rings on the sphere, plane and hyperbolic plane: Montaldi–Tokieda Conjecture 13 completed, certified tanh-model thresholds, a Lean 4 check, and the havelock Python package.

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

Domino and domicule tilings and the dimer entropy of the king's graph: exact counts on boards, cylinders and tori, rigorous bounds, papers, OEIS entries and a gallery that draws any tiling.

正十七边形 12 E 尺规作图研究 | Regular 17-gon construction: verified 12 E upper bound, exact replay, and Manim animation.

Research artifacts for the queen domination problem

Self-contained Berge–Fulkerson C(20) proof with complete Lean formalization, explicit native-evaluation trust, and exhaustive certificates.

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 checks nine of the fourteen certificates.

Rigorous bounds and reproducible certificates for covering the unit disk with 100 equal disks, with constructions, local results and failed routes; the global optimum remains open.

Lean 4 formalization of Theorems A and B of arXiv:2609.35632: uniqueness of convex central configurations in the planar four-body problem and the Hessian bound Q ≥ K/4

Audit the declarations a computational result carries, and check they are still true. Producer freshness, counter coherence, provenance pins, partial runs. Read-only by construction.

Independent exact certification of machine-generated mathematics — exact arithmetic, no code shared with the claimant, refusal as a verdict.

Shared-pool Mahjong: computational second-player win, kernel implication and complete recorded native-component coverage. v2 freezes three English papers with errata, sanitized evidence and explicit custody/bookkeeping assumptions. Closed opening Lean proof and independent full replication remain open.

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

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

Sharp thresholds for five-colour cube assemblies: any 15 cubes contain a 2×2×2 solution, and every box size is settled, resolving the five-colour case left open by Berkove, Eickemeyer and Schulman. Paper and Lean formalisation.

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