Posts by Tag Floating-point numbers Floats in Lean 4.33 June 19, 2026 · 10 minute read Lean Floating-point numbers Lean An underappreciated Lean feature July 14, 2026 · 11 minute read Lean Floats in Lean 4.33 June 19, 2026 · 10 minute read Lean Floating-point numbers My first verified (imperative) program July 6, 2025 · 13 minute read Lean human-eval-lean Freyd-Mitchell and Gabriel-Popescu June 21, 2025 · 1 minute read Lean mathlib Lean has iterators now June 12, 2025 · 2 minute read Lean human-eval-lean The largest divisor June 9, 2025 · 6 minute read Lean human-eval-lean human-eval-lean My first verified (imperative) program July 6, 2025 · 13 minute read Lean human-eval-lean Lean has iterators now June 12, 2025 · 2 minute read Lean human-eval-lean The largest divisor June 9, 2025 · 6 minute read Lean human-eval-lean mathlib Freyd-Mitchell and Gabriel-Popescu June 21, 2025 · 1 minute read Lean mathlib