[patrl]

It is important to introduce some tooling to indicate which Lean statements have been explicitly checked by a human relative to their source (see #6209).

This PR sketches one way in which this might work: Lean statements are signed off by a human; sources are associated with a TOML inventory of their claims, together with the corresponding Lean code. A human sign-off records a hash of the declaration's statement closure while excluding proofs - the intent here is that a claim is only signed off if the lean statement has been checked relative to the source by a domain expert.

Some design principles:

• There's a one to one relationship between files in the registry and papers; practically speaking, a domain expert is going to want to check every formalized claim from a given paper, even if the corresponding claims are spread out across lean files.
• It should be possible to use the registry to extract a buildable, verified core of linglib.
• Dependencies between claims are inferred, not declared: claim A depends on claim B when one of B's declarations occurs in A's statement closure. A claim can be signed while a claim it depends on is unchecked, but it only counts as fully checked once every claim it depends on has been checked (stopping at mathlib).

What's here

• checks/<bib-key>.toml, one per source: its claims (with the source's own labels), the declarations stating each, how they relate to the claim (exact, generalizes, specializes, variant, missing), and the sign-offs. checks/README.md documents the format.
• lake exe checkClosure: computes statement closures from the elaborated terms (types, plus the bodies of project definitions they use, never proofs), and the axioms each declaration rests on.
• scripts/checks.py:
  • status: each claim is checked, relies (signed, but depends on an unchecked claim), stale (its statement closure has changed since the sign-off), unchecked, missing, broken (a declaration doesn't resolve) or unproved (rests on sorry or an axiom beyond propext/Classical.choice/Quot.sound, including native_decide's).
  • diff: what changed since a claim was signed.
  • sign: records a sign-off with the closure's hash; refuses to run inside an agent session.
  • core: the reviewed core, i.e. the declarations of the checked claims and the definitions their statements use. Since a claim is only checked if the claims it depends on are, nothing in the core depends for its meaning on anything outside it. (Extracting it as a buildable artifact, e.g. by exporting the full constant closure and re-checking it with an independent kernel, is left for later.)
  • status --json: every claim and its latest sign-off, for the docs pages.
• Docs pages: under each declaration stating a checked, relying or stale claim, one line in the style of "Used by", e.g. Checked against George 2014, Definition 23 (a variant) by patrl on 3 November 2026, or that its statement has changed since the sign-off (with a link to the diff). docs.yml exports the checks before composing the site.

No source has a check file yet; the George (2014) record follows once #6211 lands.

(This is a big, and important feature, and probably warrants further discussion before settling on a design. Maybe an RFC process would be helpful.)