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.
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
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.
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 verifies fourteen certificates.
在固定尺规模型下研究最少作图步数：提供正十七边形 17E 与正257边形 69E 构造的精确证书、SageMath 验证、搜索记录和 Manim 动画。
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)
Rigorous partial progress toward a global 68.10% PairCeiling certificate
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.
Computer-assisted proof that the minimal superpermutation on six symbols has length 872. Machine-checked evidence ledger, adversarial audits, 15-second verification path. Preliminary.
Disk covering problem (disc covering): global optimality proof claims for n = 11-20, exact certificates, Chinese proofs, and reproducible verification code. External review pending.
Proof distillation for Sendov's conjecture: rational envelopes, low-degree root isolation, mixed-endpoint bounds, and exact verification.
https://en.wikipedia.org/wiki/Proof_assistant; 一錯特錯錯到底! 爆炸原理是重哪來的?
Candidate exact computer-assisted proof of Erdős Problem 488 through primitive reductions of size seven
To associate your repository with the computer-assisted-proof topic, visit your repo's landing page and select "manage topics."