dpah

4 ms·

1. 1.▲
   by dpah 7y ago

   Well, there is the entire mathematical components library[0]. It's still fairly elementary, roughly at an advanced undergraduate level. Right now it actually takes far more time to write lean code than to prove things by hand. What i
2. 2.▲
   by dpah 7y ago

   I've used Lean a fair bit (mostly contributing to mathlib), and have had a cursory glance at Coq. They are pretty similar, with really similar foundations. Both use variants of Calculus of Inductive Constructions for their foundation.
3. 3.▲
   by dpah 7y ago

   They are employing a dark pattern to make it seem that way, but it isn't so. You can just click "next" without actually entering an email. But there is no indication that the field is optional.