Lf-lean: The frontier of verified software engineering
alpaylan
18 points
5 comments
March 12, 2026
Related Discussions
Found 5 related stories in 53.2ms across 3,471 title embeddings via pgvector HNSW
- Leanstral: Open-source agent for trustworthy coding and formal proof engineering Poudlardo · 407 pts · March 16, 2026 · 59% similar
- Reliable Software in the LLM Era mempirate · 102 pts · March 12, 2026 · 57% similar
- How I write software with LLMs indigodaddy · 69 pts · March 16, 2026 · 54% similar
- The unwritten laws of software engineering AntonZ234 · 16 pts · March 17, 2026 · 53% similar
- Terence Tao: Formalizing a proof in Lean using Claude Code [video] helloplanets · 51 pts · March 09, 2026 · 50% 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?