Conventional Knowledge Commits

Timelines

Each figure replays a project's history one commit at a time: drag the slider and watch every claim's status move from conjecture to machine-checked, where a refutation drops a result back to unproven, and where a silent sorryAx spreads through a dependency closure. These are produced by claimgraph svg-timeline: a few KB of self-contained SVG, laid out automatically from the claim graph, with no viewer bundle. (For the full interactive graph with dependency closures and blast radius, see the Live graph.)

Generated with claimgraph svg-timeline --from-fixture examples/<name>/<name>.commits. The same command runs against a real CKC repository.

The Four Colour Theorem

Guthrie's 1852 conjecture, Kempe's 1879 proof refuted by Heawood in 1890, the 1976 computer-assisted proof, and Gonthier's 2005 Coq formalisation. A refuted result only ever drops back to unproven, never to false.

PFR: the WeakPFR silent contamination

PFR's WeakPFR strand builds to machine-checked, then the 2026 module-system migration silently turns all seven results to sorryAx behind a green build; the downstream corollary becomes the blast radius (own proof intact, but effectively open). A curated reconstruction grounded in a measured proof-rot finding.

Fermat's Last Theorem

From the 1637 margin to Wiles' 1994 proof via the modularity theorem.

The Kepler Conjecture

Hales' 1998 proof and the Flyspeck machine-checked formalisation.