A Critical Look at Lean4
amanverasia
15 points
1 comment
October 12, 2026
Related Discussions
Found 5 related stories in 100.2ms across 9,270 title embeddings via pgvector HNSW
- Are We Stuck with Lean? jjgreen · 135 pts · July 30, 2026 · 62% similar
- Fermat's Last Theorem in Lean 4 aaraujo002 · 83 pts · September 04, 2026 · 56% similar
- LeanScreen: Lean Verification Hdjlaf · 30 pts · July 29, 2026 · 55% similar
- Show HN: Lean4 Datalog DSL Based on Google Zanzibar for AI Projects kbradero · 11 pts · July 29, 2026 · 54% similar
- Show HN: Spivak's Calculus formalized in Lean 4 – every theorem, every problem jsLavaGoat · 12 pts · September 26, 2026 · 53% similar
Discussion Highlights (1 comments)
Mithriil
Very interesting. I think it needs to be clear that the fundamental theories (dependent type theory) is very much grounded. It's at the practical implementation of Lean4 that the critic aims at.