Latest Posts (19 found)
Rado's Radical Reflections 1 months ago

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 aimed at Lean language beginners that are interested in writing proofs in Lean, but still feel lost when reading Lean code. A very simplified mental model of Lean is that at the core there are two systems:

tutorial Tutorial ai AI programming Programming
0 views
Rado's Radical Reflections 2 months ago

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 works in the software industry that is adapting to using AI tools, the post was very timely and very well put. I agree with everything said, but I just can’t resist being that guy - bringing up the “you keep using that word” meme.

programming Programming
0 views
Rado's Radical Reflections 2 months ago

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 my previous post on leaning on Claude for Lean. I’ve now worked up to chapter 8.3 in Tao’s companion. The speed is great and Claude’s capabilities continue to impress (autoformalization is possible, but not my goal). I haven’t been stuck on anything so far. I’ve also upstreamed many typos to the companion repo .

data-analysis Data Analysis ai AI
0 views
Rado's Radical Reflections 3 months ago

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 started to wear off, I did not find motivation to push as hard as before. The SF Math with Lean work group kept me vaguely connected (at least in the one hour a week we meet (see retro) ) but other than that I wasn’t putting in more than a few hours a week on math and Lean.

programming Programming
0 views
Rado's Radical Reflections 3 months ago

Local Lean Workgroup Retro

I started learning formalized mathematics with Lean last year 1 , 2 , 3 , 4 . As I progressed beyond basics, it dawned on me that I need to start interacting with the broader community as Lean is rapidly evolving and beyond basic getting started guides there aren’t as many high-quality resources to learn solo. It could also be a great way to meet folks with similar interests and build more social connections. To that end I tried to start a local workgroup around Oct'25 details . I have never done anything like this before, so this is a small retro of how it went so far (in Jan'26) and what’s next.

programming Programming open-source Open Source
0 views
Rado's Radical Reflections 6 months ago

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 me when talking very deterministically about pure functions in a large unpure language like JS. Especially, after seeing JS tooling perform optimizations based on a pure annotation (like webpack) . While everyone agrees is pure, I felt there are a lot of subtle situations where disagreements might arise. What is worse than terms with imprecise meaning is terms with imprecise meaning where people using them are not aware there is imprecision.

programming Programming javascript JavaScript
0 views
Rado's Radical Reflections 7 months ago

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 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 is true.” As I have been a bit obsessed with doing formalized mathematics, this got me thinking about why I am excited to spend many hours recently writing formalized proofs in Lean for exercises from Tao’s Real Analysis (along with this recent attempt to write a companion to Riehl’s Category Theory In Context ). On a very personal level, I just like math, computers and puzzles, and writing Lean proofs feels like doing all three at once. But I do believe formalization is important beyond nerd-snipping folks like me.

programming Programming Science
0 views
Rado's Radical Reflections 8 months ago

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 - which means all proofs from the paper textbook are fully formalized in Lean, while examples and exercises are stated in Lean but left with a for me to fill in. Altogether the companions has close to 2000 sorries to fill-in.

programming Programming tutorial Tutorial
0 views
Rado's Radical Reflections 11 months ago

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 some of the basics. This summary was supposed to be my notes from finishing the rest of Mathematics in Lean and finishing chapters 2 and 3 of exercises from Terence Tao’s Analysis textbook , but also I couldn’t help also comment on the challenges and opportunties I see in doing formal mathematics with Lean.

tutorial Tutorial programming Programming
0 views
Rado's Radical Reflections 1 years ago

Thoughts on Signals in the JavaScript Ecosystem

Around 5-8 years ago when working on Angular and TypeScript rules in Bazel, I got very interested in exploring the core ideas of incremental computation, which seemed like the right way to abstractly (but still precisely) describe the similarities between build systems and UI reactivity. As an aside, incremental dataflow is a third view into the same concept, but I am least familiar with it. I wrote the following series of posts to try to pull all the different threads together. It was useful for me to put something to paper, but at the end I failed in painting a picture as clear as I wanted.

programming Programming typescript TypeScript javascript JavaScript
0 views
Rado's Radical Reflections 1 years ago

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. The online book is well-paced and well-written to connect with what an average student of mathematics already knows. The focus is on learning how to do basic mathematical proofs in Lean, and the underlying language is taught as needed for those goals, in comparison to Theorem Proving in Lean which is more of a language guide. For example, the fact that naturals are constructed as an inductive type with zero and succ constructors is shown much after one is shown how to work with them. This is aligned with how a lot of mathematics is done before one discusses foundations in a typical mathematics curriculum, which might differ from a CS one.

programming Programming
0 views
Rado's Radical Reflections 1 years ago

Learning Lean: Part 1

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 mathematics is generating such excitement in the mathematical community. The immediate benefits of formalization are well-documented: it helps catch errors in proofs and reduces the need for trust between collaborators since every step is mechanically verified. However, I believe there’s another compelling advantage that’s less frequently discussed: formalization enables a better separation of concerns in mathematical writing.

Science tutorial Tutorial programming Programming
0 views
Rado's Radical Reflections 1 years ago

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 seemed like an excellent opportunity to experiment with Cursor AI and explore more automated approaches to coding. Here’s what I discovered. After a couple of hours the AI and I produced the following analyses: The 32 tickets in the game can be categorized by their optimal paths:

data-analysis Data Analysis gaming Gaming statistics Statistics
0 views
Rado's Radical Reflections 1 years ago

Puzzles2024

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, but rather a personal reflection on the games that captured my attention. If you’re new to the puzzle genre, I recommend starting with the essential thinky games list - all of those titles are excellent.

gaming Gaming
0 views
Rado's Radical Reflections 1 years ago

Aoc2024

Advent of Code AoC is an annual programming competition that releases daily coding puzzles throughout December. For the past four years, I’ve tackled these challenges from the West Coast, where the 9 PM PST release time perfectly suits my schedule. While I compete for points on the global leaderboard (with modest success), the real joy comes from the community around it. Through Stripe’s solution-sharing Slack group, and the active r/adventofcode community, discussing creative approaches to challenging problems adds an new dimension to my favorite pastime - solving puzzles.

programming Programming
0 views
Rado's Radical Reflections 6 years ago

Incremental Computation (part 3)

Maybe you wondering why did I use TypeScript for this post. As it happens I have been working in the frond-end community in the last 8 years. My interest in incremental computation started by observing the similarities between some of the work I have done inside Angular’s “change detection” algorithms, and work I have done around integrating TypeScript’s compiler in Google’s build system . Why is incremental computation naturally appearing in UIs? As the user is interacting with an UI they are providing new inputs. Usually, these inputs are small compared with the initial input to the UI. On the other side the producing the DOM is the quintessential “expensive” computation. If it redone on each user input the UI will be unusable. So all UI frameworks attempt to solve the incremental computation problem, struggling with the fact that JS has no support for incremental computation. To make matters worse as we have seen incrementality is easier in a functional language, but JS is not well suited to that paradigm (which doesn’t stop people from trying).

programming Programming javascript JavaScript typescript TypeScript web-development Web Development
0 views
Rado's Radical Reflections 6 years ago

Incremental Computation (part 2)

We have been talking about general computation, but so far our language was very limited. We only used function calls, numbers, and simple variable binding. We will slowly add more language primitives and see how to still have full incrementality of the computation. Let’s add a single conditional statement first. What does it mean to make incremental? Say we compute the result first for some values of , , .

programming Programming
0 views
Rado's Radical Reflections 6 years ago

Incremental Computation (part 1)

Incremental computation is a way of performing computations, with the expectation of future changes in the inputs to the computiation. When those changes occur the output can be updated efficiently, at minimum faster than redoing the whole computation from scratch. This problem occurs in many programming domains - UI programming, data flow, build systems, compilers, code editors. Likely you have seen it before, but didn’t call it incremental computation. Despite its prevalence, it is rarely viewed as a common computational paradigm. It is more often referred to as an ad-hoc application of caching or memoization. In comparison, other computational paradigms like concurrent, lazy, distributed computation have better known nomenclature and techniques.

programming Programming
0 views
Rado's Radical Reflections 6 years ago

About

Hello! I’m Rado Kirov, a front-end engineer at Stripe where I maintain stripe.js . Before this, I worked at Google on front-end infrastructure, helping build core technologies like Angular, TypeScript tooling, and the Closure Compiler. I started my career in academia as a mathematician, completing a postdoc before transitioning to software engineering.

javascript JavaScript typescript TypeScript career Career
0 views