What "proved" means

The kernel tells you a proof is correct. The scope tells you how much the theorem says, and lein verify prints it for each theorem.

For all inputs

A for-all statement quantifies over data, so it holds for any input the types allow, tried or not. From math/finite/rational_argmax.clj:

decision/finite-nnrat-argmax-dominates :
  for every type of actions A, every finite set of actions, every scoring
  function, and every candidate in the set:
    score(candidate) <= score(argmax)

Worked instances

An instance is a statement about specific values. From the Christofides module:

christofides/tour-at-most-bound :  13 <= 15

A tour of cost 13 is within the bound 15 for an instance whose optimum is 10. The theorem covers no other tours and does not prove the algorithm’s 3/2 approximation guarantee. Worked instances pin down what a decision step computes on concrete data, and since they are re-checked on every run, a changed definition shows at once.

Definitional unfoldings

An unfolding quantifies over data and is proved by reflexivity, because a definition unfolds to the right-hand side. It says no more than the definition.

How the scope is decided

lein verify classifies each theorem from its own type:

lein verify rainbow.algorithms.proofs.ahof.christofides

OK    rainbow.algorithms.proofs.ahof.christofides (3 theorems: 0 for all inputs, 0 definitional unfoldings, 3 worked instances)
       checked   instance  christofides/tour-at-most-bound  axiom-free
       ...

The rules are in rainbow.main (source):

• for-all: one of the statement’s leading binders ranges over a type outside Prop, such as numbers, vectors, sets or a type variable.
• instance: no leading binder ranges over data. The statement has no binders, as in 13 <= 15, or only hypotheses. A negation or an implication between closed propositions counts as an instance.
• unfolding: the statement quantifies over data, and the proof, under its binders, is an application of equality/reflexive.

rainbow.main sits outside the trusted base and works from the kernel’s type inference and the proof term. Modules whose theorems are all worked instances say so at the end of their docstring, under “Scope (measured by the kernel)”, generated from this classification.

The operations-research catalogue

Each of the 222 algorithms in the Applied Higher-Order Functions catalogue has kernel-checked theorems about its decision step: the test, selection or update it is built around. Of the 415 algorithm proof modules, 48 prove a for-all statement that is not an unfolding, and the rest check worked instances or unfoldings. Guarantees such as optimality, convergence or approximation ratios are claimed only where a theorem states them, and the module docstrings say which.

Axioms

All but eight of the corpus’s theorems report axiom-free. The eight, in math/finite/set_boundary.clj and set_union.clj, use logic/excluded-middle or logic/proposition-extensionality, and the coverage tests name them with their axioms. Some re-proofs of Mathlib statements in the default checkpoint store use axioms too, and lein verify prints each theorem’s own profile.