What a machine-checked proof means
A visual guide to Lean, Rocq, Isabelle, Mizar, Agda and Arend, and the distance between a checked derivation and the mathematics it is meant to express.
Read the visual essayNotes
Under Construction
Warning: Artificial Prose
An exploration of mathematics, with arguments and sources close at hand.