Lawrence C. Paulson personal blog
“Why not just use Lean?”
I have been told that when proposing to formalise mathematics these days, you have to explain why you are not using Lean. And that reminds me why I left the dependent-typed world 40 years ago: its cultism, insularity and conformity. Lean is a great language with good tools, a large library and a huge, enthusiastic…
- Points
- 304
- HN comments
- 209
- Submissions
- 1
- Cited by
- 0 commenters
Programming LanguagesMath & Algorithms2026
On Hacker News
| Submitted | Title on HN | Points | Comments |
|---|---|---|---|
| Apr 27, 2026 | “Why not just use Lean?” by ibobev | 304 | 209 |
