Trustworthy Automated Reasoning
summary
Claims validated with formally-verified proof checker: Boolean Pythagorean Triples is unsatisfiable for 1..7,824 with proofs that reach terabytes to petabytes but validate; Keller’s conjecture is false from dimension eight; packing chromatic number work yields a 5-chromatic unit-distance graph reduced from 1,581 to about 510 vertices. Toolchain uses a single proof rule (DRAT-style), backward proof checking on outputs from high-performance solvers (800 cores, two days ≈ four CPU years), heavy use of re-encoding and unsatisfiable core extraction to shrink instances, and four verified checkers (Coq, Isabelle, ACL2, K-CaML).
AI-written summary · about
chapters (9)
- 0:00Introduction to trusted proof
- 6:05Methodology of proof checking
- 12:56Efficient proof verification
- 20:38Building a reliable tool chain
- 23:56Case study: Chromatic number
- 36:08Challenges in core minimization
- 41:54Keller's conjecture and proofs
- 48:55Advanced techniques: Click hints
- 53:16Conclusion and discussion
related talks
24mCertifying the decidability of the word problem in monoids at large
21mMassive proofs for the masses
25mProperty-agnostic base case extension for scalable verification of distributed systems
21mA Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
01h 07mSatisfiability Algorithms I
35mWhy Extension-Based Proofs Fail
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
16mSpain: Succinct Proofs for Numerical Computations