FAQ

Why extend Conventional Commits instead of inventing a new format?

The ergonomics are already right: a short, parseable header plus git-trailer footers, read by both people and tools. CKC keeps the grammar and only adds vocabulary, so every CKC commit stays a valid Conventional Commit and existing tooling keeps working.

Why two axes? Isn't a status enough?

A status alone cannot tell you what breaks. Software conflates the two because it has one scale, compatibility. Knowledge needs both: dependency impact (did this invalidate dependents?) and epistemic status (how established is it?). A result can advance in status without breaking anything (open to machine-checked), and a commit can break dependents without changing its own status (a re-statement). Keeping them apart is what makes the ClaimGraph well-defined.

Why is status a footer instead of part of the type?

Status is mutable; the type is not. When a sorry closes months later, you do not rewrite the old commit's type. You add a new formalize commit that moves the Status: footer forward. The type records what happened; the footer records what is believed now, taken from the latest commit that touched the claim.

Is introducing an axiom a "breaking change"?

Usually not, on the dependency-impact axis. Citing an axiom is additive, since it introduces an object, so it does not invalidate dependents. It is a trusted-base event on the status axis: the status becomes axiomatised and the commit carries an AXIOM: footer. It is breaking only when it replaces a previously proved result with an assumed one.

Does CKC require Lean, or a proof assistant at all?

No. The proof profile is sharpest with a proof assistant, because the trusted base is exact, but the science profile needs none, and the shared core (conjecture, lit, review, refute, expose) is assistant-agnostic.

Does the proof profile work with Rocq, Coq, Isabelle, or Agda?

Yes. The profile needs two things from a system: a stable name for a declaration, and a way to report what a proof assumes. Lean is the reference because #print axioms makes that explicit, but the same three states exist everywhere. Use Verified-By: to name the system and version, and prefix the formal name in Formal-Statement: (lean:, rocq:, coq:, isabelle:, agda:). The assumption check is #print axioms in Lean, Print Assumptions in Rocq and Coq, thm_deps in Isabelle, and the --safe flag with no postulates in Agda. The proof profile lists the mapping.

How is this kept honest if nothing enforces it?

CKC is convention-first, like Conventional Commits itself. The proof profile is honest by construction in one respect: the Status: and Axioms: footers are meant to be the literal output of the assistant's assumption check. An opt-in checker can compare those footers against the kernel and reject a commit that claims machine-checked while a sorry or a non-standard axiom is present (ckc-tools ships one). And v0.2.0 adds the layer the kernel cannot reach: transcription fidelity, because a perfectly kernel-honest commit can still transcribe its source wrongly.

The kernel already checks everything. Why do I need Source-Ref:?

The kernel checks the statement as written; it has no opinion on whether that statement is the one the source proved. A transcribed axiom that silently drops one of the paper's hypotheses is kernel-honest and status-honest and still false: in one audited formalization, nearly every cited axiom failed exactly this way, one refutable in three lines from a missing μ ≠ ν, and every gate passed. Source-Ref: pins the verbatim locus so comparing the statements is a diff, not an archaeology project, and Refutation-Attempt: records that someone tried to break the statement as written. The case study walks through the incident.

What is the relationship to SemVer?

Semantic Versioning (SemVer) is the single decision Conventional Commits serves. CKC's equivalent is the ClaimGraph, from which a SemVer-style release version can be derived for a knowledge artifact: a breaking knowledge event is a MAJOR release, a new result or replication is a MINOR, a repair or cleanup is a PATCH. The graph and the status report are the main payoff; the version number is optional.

How do Depends-On: and Refutes: survive someone rephrasing a theorem?

Through stable identifiers (see the Identifiers page). In the proof profile the identifier is the assistant's fully-qualified name, which is already rename-aware. In the science profile it is a curated slug in claims.toml, optionally bound to a DOI on publication. Commit hashes are not used as claim ids: a hash identifies a change, not a claim.

Why are negative results their own types?

Because hiding them is the failure mode CKC exists to prevent. A counterexample, a disproof, a null result, and a failed replication are refute, null, and replicate commits, never dropped or relabelled as a fix. The ClaimGraph treats them as the events they are.

How does this relate to nanopublications and PROV?

They are relatives. A nanopublication is an assertion with its provenance and publication info; W3C PROV is a general provenance model. CKC carries the same idea (assertion, provenance, relations) but lives where the work already happens, in the commit log.