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.
Open-source re-implementation of DeepMind's unstable singularity detection methods using PINNs for blow-up solutions in fluid dynamics
Research artifacts for the queen domination problem
在固定尺规模型下研究最少作图步数：提供正十七边形 17E 与正257边形 69E 构造的精确证书、SageMath 验证、搜索记录和 Manim 动画。
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.
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.
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.
Computer-assisted proof that the minimal superpermutation on six symbols has length 872. Machine-checked evidence ledger, adversarial audits, 15-second verification path. Preliminary.
Rigorous partial progress toward a global 68.10% PairCeiling certificate
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)
Weil's explicit formula for ζ(s): an exact magic function F = Ξ²H shows the Odlyzko–Poitou–Serre method is sharp for ζ (κ* ≤ 0), and every positive solution is ζ's own zeros and primes (Conjectures S and U of Part I). Paper, certificates, Lean 4 spine and reviewing guide.
An adversarial, fully-banked search for a Navier-Stokes blow-up certificate: 440 legs, no solution found, and an honest record of why. Every claim tiered, every gate falsifiable, all data banked. Independently kernel-checked the Lean Navier-Stokes formalisation. MIT + CC BY - fork it and carry on.
Lean formalization of the Berge–Fulkerson C(24) theorem, with exhaustive finite verification and reproducible proof evidence.
To associate your repository with the computer-assisted-proof topic, visit your repo's landing page and select "manage topics."