Check your first proof

rainbow.math.finite.rational-argmax defines an argmax over a finite set of actions scored by non-negative rationals, and proves the chosen action scores at least as high as any member of the set. You need a clone at v1.4.1 (Install), and you run commands from the repository root.

Verify the module

lein verify rainbow.math.finite.rational-argmax

checkpoint artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz replayed
OK    rainbow.math.finite.rational-argmax (15 theorems: 13 for all inputs, 0 definitional unfoldings, 2 worked instances)
       checked   instance  bool/false-not-true  axiom-free
       checked   instance  bool/true-not-false  axiom-free
       checked   for-all   decision/finite-nnrat-argmax-dominates  axiom-free
       ...

The command replays the default checkpoint, a saved environment of declarations, through the kernel. It installs the module, with the kernel checking each new declaration, then re-checks each theorem in theorem-ids and works out its scope and axioms.

Read the output

If the checkpoint does not replay, the first line is FAIL checkpoint ... did not replay and the command stops. The second line is the module’s verdict with a count of its theorems by scope. OK means the module installed, named at least one theorem, and all its theorems checked.

Each theorem line gives a status, a scope, the alias and the axioms. checked means the kernel accepts the proof, and any other status fails the module. The scope is for-all when the statement quantifies over data, unfolding when it does and the proof is reflexivity, and instance when it is about specific values, like bool/false-not-true (What “proved” means). The last column is axiom-free, or axioms: and the axioms the kernel computed.

The exit code is 0 when all namespaces are OK and 1 otherwise, so the command works as a CI gate:

lein verify rainbow.math.finite.rational-argmax && echo "all checked"

Read the statement in the source

decision/finite-nnrat-argmax-dominates is defined in src/rainbow/math/finite/rational_argmax.clj. The :type is the statement and the :value is the proof, both Clojure data:

(def finite-argmax-dominates-spec
  (let [result (finite-argmax 'A 'actions 'initial 'score)]
    {:name 'decision/finite-nnrat-argmax-dominates
     :universes ['u]
     :type
     (function/forall
      [['A type-u] ['actions (exact-finset-of 'A)]
       ['initial 'A] ['score (function/arrow 'A nnrat)]
       ['candidate 'A]
       ['candidate-member (source-membership 'A 'actions 'candidate)]]
      (rational-at-most (function/app 'score 'candidate)
                        (function/app 'score result)))
     :value
     (function/lam
      [['A type-u] ['actions (exact-finset-of 'A)]
       ['initial 'A] ['score (function/arrow 'A nnrat)]
       ['candidate 'A]
       ['candidate-member (source-membership 'A 'actions 'candidate)]]
      (function/app
       (function/const* 'list/nnrat-argmax-from-bounds-member [U])
       'A 'score 'initial (enumeration 'A 'actions)
       'candidate 'candidate-member))}))

Read the :type as: for any type of actions A in universe u, finite set of actions, initial action, scoring function into the non-negative rationals and candidate in the set, the candidate scores at most what the argmax returns. The proof applies an earlier lemma, list/nnrat-argmax-from-bounds-member.

theorem-specs lists this spec and 14 others, and install adds three definitions and then the 15 theorems through kernel/add-declaration.

Print the statement with lein show

To see what the kernel holds after installing it:

lein show decision/finite-nnrat-argmax-dominates rainbow.math.finite.rational-argmax

The type prints like a function signature. The first line is the alias with its universe parameters, here decision/finite-nnrat-argmax-dominates.{u} :, then the binders, then a line starting with → with the conclusion. A long repeated expression may be shortened to a name and spelled out on a where line.

Kernel binders are de Bruijn indices, so names come from the source spec when elaborating it gives exactly the kernel’s type, and are generated otherwise. A comment line under the statement says which. A legend maps each notation to its constant, and …⟨n⟩ marks n term nodes cut for length.

For an alias it cannot find in the checkpoint or the modules you named, it prints unknown declaration and asks for the module that installs it.

All 15 statements are on the reference page for this module. Commands lists every option.