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…
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…
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.
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…
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…
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.