Apodictic: Machine-Checked Praxeology🔗

The axiom archaeology of Austrian praxeology, formalized in Lean 4: the narrative of every axiom's pedigree, the findings forced by the proof assistant, the design decisions as they were made, and the rejected encodings as type-checked code.