Intuitionism is very interesting, but those of us who "grew up" on classical logic can easily accidentally depend on the law of excluded middle applying in all

Intuitionism is very interesting, but those of us who "grew up" on classical logic can easily accidentally depend on the law of excluded middle applying in all cases. The Metamath system lets you specify the axioms you want to use, and then can verify that your proofs only use those axioms (directly or indirectly). There's a Metamath database specifically for intuitionistic logic: https://us.metamath.org/ileuni/mmil.html https://us.metamath.org/ileuni/mmil.html More things have been proven using intuitionistic logic over time.