Just dawned on me that Tao's proof digestion (see youtube.com/live/f0hgLiq...) and Chris Olah's research debt and distillation (from the ancient 2017) - distill.pub/2017/researc... are talking about the same thing. AI in math is likely to produce tons of new mountains of research debt.

Great talk by @yminsky.bsky.social - youtu.be/rUYP4C29yCw?... Refreshing to see some balanced optimism around AI for coding and renewed interest in formal methods.

new blog post - rkirov.github.io/posts/three-...

New blog post: Theseus, a static Windows emulator An new old approach to emulation. neugierig.org/software/blo...

Normal people's midlife crisis: buy a Harley or a Corvette. Mine: formalize all of mathematics in Lean.

New beginner Lean blog post - From Painfully Explicit to Implicit in Lean - rkirov.github.io/posts/lean-i...

With AI, we are doing more validation and less writing. Validation means code reviews, testing - manual or automated. But did you know you can write actual mathematical proofs that your code is correct? I wrote about it here rkirov.github.io/posts/code-p...

Vibecoded with Claude higher-kinded types for TypeScript - rkirov.github.io/TypeScript/ (demo) and github.com/rkirov/TypeS... (code). Probably still quite buggy, but could be interesting to play around with a bit.

New blog post - Human Intuition, AI Formalization: A Real Analysis Case Study rkirov.github.io/posts/lean6/ Read about how I used Claude and Lean to work through a Real Analysis classic - Riemann's rearrangement theorem.

I asked Claude code to formalize with lean a proof for the knuth 3d hamiltonian cycles problem (odd cases for now) that also solved experimentally by claude - www-cs-faculty.stanford.edu/~knuth/paper... github.com/rkirov/claud... Read more in the human notes section in the README.

New blog post - From sets in math to types in Lean rkirov.github.io/posts/sets-v...

Leaning on AI - new blog post about using AI to learn Lean rkirov.github.io/posts/lean5/

"Is this JS function pure?" - wrote a short blog post summary of the pure JS function poll I ran in 2019 rkirov.github.io/posts/pure/

Falling in an odd rabbit-hole of visualizing logical deductions. Why isn't there a mobile friendly game for proving the ~100 core theorems of propositional and first-order logic? [1] incredible.pm [2] www.winterdrache.de/freeware/dom... [3] www.jfsowa.com/peirce/ms514...

AI boosts productivity until a breaking point where domain expertise becomes unnecessary (coding, formalizing math, etc.) - you can go straight from idea to implementation without interaction with the underlying tool. Some are betting that arrives soon enough that they don’t invest in learning.

You can’t convince me Russell wouldn’t have used Lean if he had a chance.

new blog post - Why formalize mathematics - more than catching errors rkirov.github.io/posts/why_le...

Calling Bay Area math enthusiasts interested in weekly sessions doing rigorous foundational mathematics the modern way - with computer-verified proofs in Lean. (An experiment in rigorous math education outside traditional academia)

Newest installment in my journey of learning how to do math proofs with computers rkirov.github.io/posts/lean4/.

The more I learn about logic, it dawns on me that math is sloppy about syntax (“by abuse of notation”), while software engineering is sloppy about semantics (“the purpose of a system is what it does”) and only when analyzing logical systems their interplay is explored.

Ironic that in logic "model" is the thing imbued with meaning (contrasting the syntactic meaningless moving of symbols around), while in ML "model" is the meaningless (but useful) pile of bits, while the "real world" which the ML model models is where the meaning is.

We're excited to share the Lean FRO Year 3 Roadmap today! It builds on work completed in the first two years of Lean FRO operations and will guide all #LeanLang development through July 2026. ➡️ Read the roadmap at lean-lang.org/fro/ #LeanProver #FormalMathematics #FormalVerification

New blog post on my learning formal mathematics with Lean journey - rkirov.github.io/posts/lean3/

More notes on learning math theorem proving with Lean - rkirov.github.io/posts/lean2/.

New blog post - learning how to use a dependently typed language Lean4 to write formally verified math proof rkirov.github.io/posts/lean1/

Reflections on using Cursor for a simple, but non-trivial coding task - analysis the board game Ticket to Ride: First Journey rkirov.github.io/posts/ticket/

If you are looking for puzzle game recommendations, read about the ones that I played and enjoyed in 2024 - rkirov.github.io/posts/puzzle...

New blog post - Advent of Code '24 Retro rkirov.github.io/posts/aoc2024/.