Show HN: Formal Verification with Lean

Category: other

Tags: formal-verification, lean, proof-assistant

Score: 4.5/10 (Innovation: 4, Technical: 6, Documentation: 5, Utility: 3)

This is a blog post demonstrating formal verification in Lean by implementing insertion sort and proving its output is sorted. It's interesting for showing how dependent types bridge programming and proof, but is a tutorial rather than a reusable tool.

Target audience: academic researchers, functional programmers

Repository: https://www.daniellowengrub.com/blog/2026/04/30/lean · HTML · 2 stars

View on Hacker News