Functional Programming and Theorem Proving in Lean 4 | Heykuki News