Lf-lean: The frontier of verified software engineering
alpaylan
18 points
5 comments
March 12, 2026
Related Discussions
Found 5 related stories in 89.5ms across 8,303 title embeddings via pgvector HNSW
- Laws of Software Engineering milanm081 · 906 pts · April 21, 2026 · 59% similar
- Leanstral: Open-source agent for trustworthy coding and formal proof engineering Poudlardo · 407 pts · March 16, 2026 · 59% similar
- “Why not just use Lean?” ibobev · 271 pts · April 27, 2026 · 59% similar
- Reliable Software in the LLM Era mempirate · 102 pts · March 12, 2026 · 57% similar
- A Perfectable Programming Language yuppiemephisto · 94 pts · April 12, 2026 · 55% similar
Discussion Highlights (2 comments)
ngruhn
Is this impressive? They just ported a bunch of theorems/proofs already written in Rocq into Lean. Also Logical Foundations is just a Rocq tutorial with the basics. An absolutely amazing tutorial and probably the best resource out there. But I'm not surprised AI can do that.
akkad33
This website is asking me for permissions on my phone. Why?