Talia Ringer on Nostr: Hilbert seems to strike an unhappy medium. E is meant to mirror Euclid's proofs very ...

Hilbert seems to strike an unhappy medium. E is meant to mirror Euclid's proofs very closely, so usability should be at the forefront, but the axiom set is quite large (thankfully the metatheory is well understood though). The student prototype however used a small DTT kernel, then some internal kernel axioms on top of that to model E