iiinova — where your digital self keeps evolving

Rado Kirov @radokirov.bsky.social · 14/09/2026

A sampler - “Pure functional languages have this advantage: all flow of data is made explicit. And this disadvantage: sometimes it is painfully explicit.”

070

Rado Kirov @radokirov.bsky.social · 14/09/2026

I highly recommend everyone that wants to learn to ignore all blog posts and just read imae.udg.edu/~villaret/mo... by Wadler. Don’t be scared by the fact that it a paper, it’s extremely well written, tons of examples.

imae.udg.edu

160

Rado Kirov @radokirov.bsky.social · 27/08/2026

How do you make sure that the spec’s implementation matches the real world one (assuming it is not in lean)? Of course we can keep asking AI to make sure that is true, but I am interested in anything more deterministic.

120

Rado Kirov @radokirov.bsky.social · 01/08/2026

Golden age for the math hobbyist. I am excited about it too.

050

Rado Kirov @radokirov.bsky.social · 08/06/2026

Not too different from the ones I write by hand. If someone writes a “clean proofs” book maybe we can all (humans and ais) learn how to write better lean proofs. The pre-scale answer was contribute to Mathlib and get mentorship through reviews, but that doesn’t scale.

120

Rado Kirov @radokirov.bsky.social · 23/05/2026

Also a cautionary tale for new would be "math proof digestors" - there were real sustainability challenges that put the journal on hiatus distill.pub/2021/distill...

distill.pub

Distill Hiatus

After five years, Distill will be taking a break.

000

Rado Kirov @radokirov.bsky.social · 23/05/2026

Not saying that AI can't help with distillation and digestion too, but given the output is much more subjective, it is unclear how much. There is a risk that the production of debt will outpace the removal even if we focus most of human effort on that.

distill.pub

Distill Hiatus

After five years, Distill will be taking a break.

110

Rado Kirov @radokirov.bsky.social · 23/05/2026

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.

youtube.com

The Future of Mathematics Symposium

YouTube video by Future of Mathematics Symposium

110

Rado Kirov @radokirov.bsky.social · 16/05/2026

soungs great, will read! Write it before you start forgetting :)

110

Rado Kirov @radokirov.bsky.social · 16/05/2026

It feels aligned with your goal, but might take it in a "too academic" direction that would alienate some readers. One interesting question is whether you would want the (AI?) author of the most popular framework 10 years from now to credit your writing (similarly to SICP still influential in PL)

110

Rado Kirov @radokirov.bsky.social · 16/05/2026

I would pay to read about the core challenges of UI programming (reactivity, modularity, responsiveness, server-client) through the lenses of how are they practically solved with React. Something like how SICP is really about computation through the lense of scheme, not just a book to learn scheme.

140

Rado Kirov @radokirov.bsky.social · 16/05/2026

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.

youtu.be

Now more than ever: building reliable software in the age of agents | Ron Minsky | Bug Bash 2026

YouTube video by Antithesis

030

Rado Kirov @radokirov.bsky.social · 12/05/2026

That’s exactly how I do Tao’s real analysis exercises in lean now - rkirov.github.io/posts/lean6/.... Convinced that this first pseudo pass is critical in committing my brain to the problem and motivates me to own the final AI solution more. Someone should give this workflow a catchy name.

rkirov.github.io

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 work...

040

Rado Kirov @radokirov.bsky.social · 11/05/2026

code scarcity for long prior to AI, but math is just starting to absorb the implications of proof abundance due to AI. Especially with formalization it is very odd to see the culture clash, because math really looks like code there.

000

Rado Kirov @radokirov.bsky.social · 11/05/2026

10-20 years on a single program and it the end it might not even compile and they have to move on. Slowly the culture becomes binary - who made it compile first. All else starts to seem secondary - intuition, communication, etc. Tao calls this the the proof scarcity world. In coding we haven’t had

100

Rado Kirov @radokirov.bsky.social · 11/05/2026

Yes, it very curious to observe in some sort of anthropological way. In theory math and coding are the same thing (Curry-Howard), but in practice we build such different cultures around it. To put it in coding perspective - imagine programming in the strictest typed language. People work for

100

Rado Kirov @radokirov.bsky.social · 10/05/2026

Yes, and you can observe this in code (as you know from formalization in some sense math and code are the same). AI doesn’t quite write code that always matches our aesthetics but 1) no fundamental reason that it can’t one day but 2) if solely based on outcomes unclear what aesthetics it will prefer

000

Rado Kirov @radokirov.bsky.social · 09/05/2026

So the directions were always driven by human aesthetics and those were shaped by understanding the proofs. So I expect an AI proof of a big problem to both deeply unsatisfying (no one is in it purely for the binary outcome), but can invigorate the aestheticly driven ones to decode and extract.

120

Rado Kirov @radokirov.bsky.social · 09/05/2026

Folks that were in it for purely for the exploration - is Riemann hypothesis true or false, can become AI engineers and contribute to the effort that way. But the other secret is actually the space of unknown mathematical truth is extremely vast and there is no objective way to prioritize.

110

Rado Kirov @radokirov.bsky.social · 09/05/2026

Good question. Maybe a fourth thing - math as an exploration program (hence his curated list of problems, giving us the map to explore). Hard to separate the ambition of the frontier explorers for the sport of it vs the collective achievement. AI will soon be the best explorer.

110

Rado Kirov @radokirov.bsky.social · 21/04/2026

The claim that google as a company was pushing angular in some orchestrated fashion is ridiculous.

040

Rado Kirov @radokirov.bsky.social · 21/04/2026

Few people know how similar that story is for angular too. It was a pet project for the director running Google’s internal CRM. It is ancient history now (lol 15 years is millenniums in js years), but at the time js developers responded well to dependency injection and data binding.

271

Reposted by Rado Kirov

Evan Martin @neugierig.org · 20/04/2026

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

neugierig.org

Tech Notes: Theseus, a static Windows emulator

An new old approach to emulation.

0144

Rado Kirov @radokirov.bsky.social · 19/04/2026

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

190

Rado Kirov @radokirov.bsky.social · 18/04/2026

Same dynamic happening in the lean community and I was having the same exact reaction. My guess there is an ethical opposition to AI and current providers (which I can kinda respect) dressed as a technical one (which is odd)

180

Rado Kirov @radokirov.bsky.social · 13/04/2026

I am guessing the “upward_filter” tactic is a sort of “tauto” in a weaker logic of filters. Would that be a reasonable thing to say?

000

Rado Kirov @radokirov.bsky.social · 13/04/2026

Also I just started learning filters for doing basic real analysis with Mathlib and that was just asking Claude if they have something to do with modal logic where. Then I saw the axioms of filters in one of the code snippets of your post. Where do I start learning about modal logic?

220

Rado Kirov @radokirov.bsky.social · 13/04/2026

My knowledge of logic is too little to funnel follow the arguments but I love embedding the lean code with the narrative. I assume this is a custom setup, but I wonder if verso can be used like that one day.

120

Rado Kirov @radokirov.bsky.social · 28/03/2026

I was faced with similar problem (much smaller audience.) Experimenting with various “proofs-of-human-work” explicitly showing the reader upfront how much time and effort when in from me (the rest is reproducible AI that everyone has similar access to) the reader can then decide whether to proceed

010

Rado Kirov @radokirov.bsky.social · 23/03/2026

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...

rkirov.github.io

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...

020

Rado Kirov @radokirov.bsky.social · 15/03/2026

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.

rkirov.github.io

TypeScript HKT Playground

020

Rado Kirov @radokirov.bsky.social · 10/03/2026

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.

rkirov.github.io

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...

010

Rado Kirov @radokirov.bsky.social · 07/03/2026

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

021

Rado Kirov @radokirov.bsky.social · 07/03/2026

If they teach it directly with AI, they are not matching their own journey and might fail to translate the right lessons. There is also a timing risk. The ai of tomorrow might not need steering. By the time you finish the course it might not be as needed.

130

Rado Kirov @radokirov.bsky.social · 07/03/2026

Big +1, steering is mandatory today and it does involve at minimum reading the code. The main problem as I see it is everyone adept at steering has learned that pre-AI mostly by writing a lot of code. But if they teach newcomers to practice without AI the same would be seen as luddites.

140

Rado Kirov @radokirov.bsky.social · 27/02/2026

Waiting til your 40s when you get all the benefits of the 30s plus a much more visceral feeling (e.g. back pain) that you don’t have much time left and you better be efficient about it :)

051

Rado Kirov @radokirov.bsky.social · 17/02/2026

Yes probably something like tikz.dev is best.

000

Rado Kirov @radokirov.bsky.social · 16/02/2026

On the flip side crafting the diagram is laborious (moving the boxes, drawing the arrows) and as such should be prime for AI boost. Isn’t there a split the difference approach where the human does the knowledge distillation into some textual description but AI generates the final diagram?

110

Rado Kirov @radokirov.bsky.social · 08/11/2025

All of this should be equivalent to visualizing lambda calculus (by Curry-Howard), which opens to more visualizations/gamifications. But which one would make the best mobile puzzle game? [1] worrydream.com/AlligatorEggs/ [2] bntr.itch.io/visual-lambda [3] github.com/prathyvsh/la...

worrydream.com

Alligator Eggs!

000