Conventional Knowledge Commits

How the ClaimGraph works

CKC records knowledge claims and how they depend on each other as ordinary git commits. claimgraph reads that history back and rebuilds the graph, then computes the two things you want to know: what is really proved, and what breaks if a claim falls.

01The idea

A node is a claim: a theorem, lemma, definition, conjecture, or empirical finding, named by a stable identifier (a Lean fully-qualified name, or a slug in claims.toml). An edge is a relation between claims, written as a git-trailer footer in a commit message. There is no separate database. The commit history is the source of truth, and the graph is built from it on demand.

The relation footers and status values are defined in the CKC spec; this page shows what the tool builds from them.

02The pipeline

Every claimgraph build walks the commits oldest-first, builds the claims and relations, then derives the views and serializes them. Nothing downstream is maintained by hand.

claimgraph pipeline: git log and claims.toml are parsed by ckc-lint, built into a graph of claims and relations, the derived views are computed, emitted to claimgraph.json, and rendered by the Cytoscape viewer
git history → parse (ckc-lint) → build graph → compute derived views → claimgraph.json → viewer. Click to enlarge.

03Where the information comes from

The information lives in commit-message footers (git trailers). A commit asserts a claim, sets its status, and relates it to others:

formalize(four-color): a fully machine-checked Four Colour Theorem in Coq

Formal-Statement: rocq:FourColor.four_color_theorem
Status: math.machine-checked
Depends-On: FourColor.reducible
Closes: conjecture:four-color

Relations like Depends-On and Assumes form the dependency graph that everything propagates over. The rest are events. (The full footer vocabulary lives in the spec.) A breaking event uses ! or BREAKING CHANGE: and knocks the target down:

refute(kempe)!: two Kempe chains can cross, and the interchange fails

Status: math.disproved
Disproves: kempe
BREAKING CHANGE: Kempe's four-colour proof is withdrawn; the conjecture is open again.

The claims.toml registry supplies only the human statement and kind for slug-named claims. Even its status field is a cache. The tool recomputes it and never trusts it as the source of truth.

04What gets computed, not stored

Two views are derived from the edges on every build. They are never written into the history. Recomputing them each time is what keeps them accurate.

Effective status

The minimum status over a claim and its transitive Depends-On/Assumes closure, as the spec defines it. It reports the same thing as Lean's #print axioms.

The Four Colour Theorem's 1976 proof Assumes two computer-checked lemmas axiomatised, so its effective status was axiomatised: proved, but only if you trust the programs. Gonthier's 2005 Coq formalization discharged them, promoting it to machine-checked.

Affected claims

Given a claim, every dependent a refutation or retraction would put in question. Run it before a breaking change to see what you are about to disturb.

When Kempe's 1879 proof disproved was refuted, every claim that Depends-On it would be flagged in question. Nothing correct did, so the flaw stayed contained and the Five Colour Theorem, which rests on the valid chain lemma, stood. That answer comes from the edges, not from a list you keep by hand.

Append-only. A status only ever moves through a new commit, never a rewrite. History is the ledger. The dashboard is read off it.

05Run it yourself

The tool that built this site runs as a CLI on any CKC repository:

# install (pulls in the ckc-lint parser)
pip install git+https://github.com/hotherio/claimgraph.git

# build the graph from a repo's history
claimgraph build /path/to/repo --claims claims.toml -o claimgraph.json

# claims grouped by effective status
claimgraph status --claims claims.toml

# what a refutation would affect, and a claim's effective status
claimgraph affected kempe
claimgraph effective four-color
Note. The live graph is a hand-authored CKC history of the Four Colour Theorem, from the 1852 conjecture to Gonthier's 2005 Coq proof, chosen because it exercises every state: conjectured, a refuted proof, a computer-checked (assumed) step, and a machine-checked formalization. Pointed at a real repository, claimgraph build rebuilds the graph from actual commits.
Open the live graph → Read the spec