Rado Kirov
@radokirov.bsky.social
engineering at stripe. recovering academic.
I wrote a retro for my work (actually mostly Claude's) on the Jacobian autoformalization challenge - rkirov.github.io/posts/jacobi...
The Jacobian Challenge Retro
AI Disclosure: Draft was written fully by a human. Heavy use of AI for editing. In April 2026, Kevin Buzzard posed the following challenge for Lean AI autoformalization: can an AI system both define t...
rkirov.github.io
new blog post on AI usage Virtuous intellectual chores - now optional rkirov.github.io/posts/virtuo...
Virtuous intellectual chores - now optional
AI Disclosure: Draft was written fully by a human. Heavy use of AI for editing. See On AI usage for more. At this point no one doubts that AI is a tremendous capability boost for all human intellectua...
rkirov.github.io
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.
The Future of Mathematics Symposium
YouTube video by Future of Mathematics Symposium
youtube.com
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.
Now more than ever: building reliable software in the age of agents | Ron Minsky | Bug Bash 2026
YouTube video by Antithesis
youtu.be
New blog post: Theseus, a static Windows emulator An new old approach to emulation. neugierig.org/software/blo...
Tech Notes: Theseus, a static Windows emulator
An new old approach to emulation.
neugierig.org
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...
From Painfully Explicit to Implicit in Lean
Note: AI was used to edit this post. As a proof-of-human thought and input, I am also publishing the original draft which was written fully before asking AI to edit the post with me. This post is aime...
rkirov.github.io
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...
Code Proven to Work - The Math Way
This post is aimed at a general programmer and no prior knowledge of math or CS is assumed. I got nerd-sniped to write this after reading Simon’s excellent post Code proven to work. As someone who wor...
rkirov.github.io
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.
TypeScript HKT Playground
rkirov.github.io
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.
Human Intuition, AI Formalization: A Real Analysis Case Study
Human Intuition, AI Formalization: A Real Analysis Case Study Disclaimer - I wrote the core ideas; Claude helped flesh out and polish the article. See appendix for more on this. This is a follow up to...
rkirov.github.io
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.
www-cs-faculty.stanford.edu
New blog post - From sets in math to types in Lean rkirov.github.io/posts/sets-v...
From Sets in Math to Types in Lean: Subtype, Fin, Set, Finset, and Fintype
Preface: Why All Mathematicians Should Learn Lean LLMs can generate plausible-sounding proofs at unprecedented speed and scale. Some are correct, many are not, and LLMs themselves cannot reliably tell...
rkirov.github.io
Leaning on AI - new blog post about using AI to learn Lean rkirov.github.io/posts/lean5/
Leaning on AI
Leaning on AI It’s been five months since my last dedicated Lean post and as usual I have started to lose steam on Lean projects. After the thrill of discovering the world of formalized mathematics st...
rkirov.github.io
"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/
Is this JS function pure?
Is this JS function pure? In 2019, as functional programming was making the last inroads dethroning OOP, I kept hearing the mantra of “just use pure functions” in JS. Something didn’t sit right with m...
rkirov.github.io
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...
The Incredible Proof Machine
incredible.pm
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...
Why formalize mathematics - more than catching errors
Why formalize mathematics - more than catching errors 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 ma...
rkirov.github.io
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/.
Learning Lean: Part 4
It’s been 3 months since my previous post about learning Lean part 3, so it’s time to write another one. I have mostly continued to work through Tao’s Analysis book through his excellent companion - w...
rkirov.github.io
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
Lean Programming Language
Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code.
lean-lang.org
New blog post on my learning formal mathematics with Lean journey - rkirov.github.io/posts/lean3/
Learning Lean: Part 3
I am continuing to learn Lean (see part 1 and part 2). I lost some steam around March-April, but in the last two months I picked it up again. In a way it was a nice spaced repetition for relearning so...
rkirov.github.io
More notes on learning math theorem proving with Lean - rkirov.github.io/posts/lean2/.
Learning Lean: Part 2
I am continuing to learn Lean (see part 1) by going through Mathematics in Lean. These are my notes as I just finished chapters one through five. Mathematics in Lean The online book is well-paced and ...
rkirov.github.io
New blog post - learning how to use a dependently typed language Lean4 to write formally verified math proof rkirov.github.io/posts/lean1/
Learning Lean: Part 1
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 w...
rkirov.github.io
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/
Ticket to Ride: First Journey simulation authored with AI
Ticket to Ride: First Journey simulation authored with AI After playing Ticket to Ride: First Journey with my family recently, I got the urge to analyze some statistical properties of the game. This s...
rkirov.github.io
If you are looking for puzzle game recommendations, read about the ones that I played and enjoyed in 2024 - rkirov.github.io/posts/puzzle...
Puzzles2024
Puzzle games of 2024 As the year draws to a close, I want to share my favorite puzzle games from 2024. This isn’t meant to be an exhaustive review or ranking of all puzzle games released this year, bu...
rkirov.github.io