A specification for adding human- and machine-readable meaning to commits that record mathematical proofs and scientific findings.
Changing code raises one question that really matters: does it break what depends on it? Changing knowledge raises a second, independent one: how sure are we it's true? CKC tracks these as two separate axes. Keeping them apart is the whole design.
| Does it break what builds on it?impact · axis 1 | How sure are we it's true?status · axis 2 | |
|---|---|---|
| in plain terms | if this turns out wrong, what else falls with it? | is it a guess, proven, or machine-checked? |
| written in the commit | the type and a ! mark |
a Status: line at the bottom |
| can it change later? | no, it records what happened | yes, a later commit can raise or lower it |
| for example | refute!, retract!, formalize |
conjectured → proved → machine-checked |
Why two and not one? Code is either compatible or it isn't, so one axis covers it. Knowledge moves on both at once, and they move independently, so you can't fold them into a single number.
Because they're separate, you never rewrite the past to update the present. Resolve a question that was left open and that's a new commit nudging its status from open to verified. The earlier record stays intact. One result can carry both signals at once: well established, yet still flagged as resting on an assumption.
Unchanged from Conventional Commits. Every CKC commit is a valid one.
<type>[~][(scope)][!]: <description>
[body]
[footers] # git-trailer key: value, repeatable; relations and provenance
! or BREAKING CHANGE: means it
invalidates dependents (axis 1). ~ is an optional at-a-glance flag for a
trusted-base caveat; the footer is the record.
A profile is a domain vocabulary on top of the shared core. CKC ships two: proof for mathematics and formal proving (Lean and Mathlib are the reference; Rocq, Coq, Isabelle, and Agda work too), and science for empirical work. The type you choose implies the profile. Full detail: the spec.
Each result carries footers. A quiet status says how settled it is right now (axis 2). A loud marker warns anything built on it about what it leans on (axis 1), the way a breaking change warns dependents in software.
A Status: line that climbs as the work
gets firmer. It is checked against ground truth, never just asserted.
math.machine-checked | proof: fully verified, no gaps |
math.axiomatised | proof: verified, but leans on a cited axiom |
math.open | proof: still has an unproven gap |
sci.replicated | science: measured, then reproduced |
sci.falsified | science: tested, came out false |
An uppercase warning that travels to everything downstream, so a reader sees the caveat without digging:
AXIOM: | it rests on an assumption stated as an axiom |
OPEN: | it still has an unproven gap |
ASSUMES: | science: it rests on an untested assumption |
UNREPLICATED: | science: it has been run only once |
A third kind of footer wires results into
the ClaimGraph: Depends-On, Proves,
Refutes, Closes, Supersedes.
formalize(thm): close the d-fold separable factorization Lean: Sep.factorization Status: math.machine-checked Axioms: propext, Classical.choice, Quot.sound Closes: conjecture:master-formula
axiomatize~(lemma): cite the logarithmic rank bound Lean: Approx.rankBound Status: math.axiomatised AXIOM: Approx.rankBound (rank K = O(log 1/ε)) Cites: Braess & Hackbusch 2005
refute(claim)!: a counterexample blocks naive factorization Disproves: conjecture:naive-separable Status: math.disproved BREAKING CHANGE: conjecture:naive-separable withdrawn; the compensation result depends on it.
experiment(non-additive): rank K=1 vs K>1 on hard targets Status: sci.measured Metric: MSE Seed: 0..4 Hardware: 1 GPU UNREPLICATED: single machine, 5 seeds Closes: conjecture:rank-helps
More on the examples page.
The relation footers form a dependency graph of claims. From it, tooling can: