Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
dpah
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
4 ms
·
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.
▲
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.
▲
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.