Welcome This is my corner of the web where I share thoughts on software, mathematics, puzzles, life, and anything else that sparks my interest. Lean series: Learning Lean (part 1) Learning Lean (part 2) Learning Lean (part 3) Learning Lean (part 4) Why formalize mathematics - more than catching errors From Sets in…
Visit rkirov.github.io → RSS feedOn Hacker News Oct 2025 – Feb 2026
I read a good post by one of the authors of the Isabelle theorem prover, that got me thinking. The author, Lawrence Paulson, observed that most math proofs are trivial, but writing them (preferably with a proof assistant) is a worthwhile activity, for reasons similar to safety checklists - “Not every obvious statement…
Motivation I’ve been captivated by the recent movement to popularize mathematics formalization through the Lean theorem prover, and this year I’m diving deeper into learning it. For those unfamiliar with this revolution, I highly recommend watching Kevin Buzzard’s talks on YouTube for an overview of why formal…