A Comprehensive Survey of the Lean 4 Theorem Prover | Dark Hacker News