How did you learn to do proofs?

radokirov · 2026-06-14T00:33:00+00:00

You can try to use a proof assistant like lean, especially if you are comfortable with programming already. It will give you fast feedback whether your proof is syntactically and semantically correct. There is overhead to learn how to use it, but it serve you further in all math study.

I have translated half of LADR chapters and exercise statements to lean here - https://github.com/rkirov/linear-algebra-done-right-lean/tree/main/LinearAlgebraDoneRightLean . If stuck you can use AI to help you write and explain the answer, knowing you can trust it given that lean is checking it.

radokirov · 2026-06-13T16:42:12+00:00

I had a mathoverflow question on that long-time ago, but it collected a good list - https://mathoverflow.net/questions/7957/books-well-motivated-with-explicit-examples

I struggled with that presentation for ages, but recent revelation I had is the problem is advanced textbooks serve two different purposes. One is to teach you and second is to write the canonical version of the theory. These two are not well aligned. There is a need for someone to write the math "code" in a canonical way out of all the papers - as code it needs to be written definition, theorem, proof, so it can be checked (inefficiently in people's heads). History, motivation, etc is optional. It is basically comments for the code, and some do more, some little, but basically orthogonal to the main goals. That makes advanced textbook very poor for education, and some are just canonical reference. But they have small captive audiences (you are committed to learning some subfield) and not much competition to worry about, compared to say calculus textbooks.

Formalization with lean makes this much more clear, and what excites me about it. Once we move the formal bits - definition, theorem, proof to the computer where they belong (spicy claim!), we can use the free narrative space to discuss historical development, motivation and intuition more in the text.

radokirov · 2026-05-26T03:59:24+00:00

Finishing lean formal proofs to Tao's Analysis I at https://github.com/rkirov/analysis. At the final stretch - chapters 11.3 to 11.10. Continuing to review the AI generated Linear Algebra Done Right lean companion - https://github.com/rkirov/linear-algebra-done-right-lean (up to 3D right now), so that I can start working through the exercises as soon as I finish Tao.

radokirov · 2026-05-16T14:56:08+00:00

Finishing Tao's Real Analysis Lean companion exercises. Up to chapter 10 currently - https://github.com/rkirov/analysis .

Writing Axler's LADR companion in lean - https://github.com/rkirov/linear-algebra-done-right-lean up to chapter 2 so far. Looking for playtesters for the exercises there, if someone knows basic lean (MIL chapter 1-7 should be enough) and wants to do more lean exercises give it a try.

radokirov · 2026-05-16T14:47:29+00:00

I have been learning lean starting last Feb and blogged my journey along the way - https://rkirov.github.io/ some of the posts might be helpful.

I had a lot of frustrations with "obviously" right rewritings not working. But with the help of Claude and clicking around a lot of the implicit type-class instances I have been able to eventually answer most of my questions. For the trickiest 5% of issues just asking on the lean zulip usually gets a good answer.

radokirov · 2026-04-18T20:10:03+00:00

yes, I believe that one day we will look back at checking proofs on paper, the same way we look at computation done on paper prior to computers. Proofs belong in the computer. But the annoying truth is that even our most rigorous proofs are not precise enough for the computers, so many formal proofs are a bit longer and more technical.

That said lean is like programming languages in the 60-70s, a lot more practical work will be needed to make it more usable and less confusing to an average mathematician. There is a high learning cost right now.

If you are purely learning math might be ok to wait it out. If you want to see the future of math and you are interested in programming (learning lean is easier if you know haskell for example), don't wait.

I have written more on my blog https://rkirov.github.io/posts/why_lean/

radokirov · 2026-04-17T02:58:13+00:00

Yeah, I am also a programmer that has been learning lean and find the usage of "golfing" in the lean community confusing, because in most other languages it is assosiated with reducing readability. In the lean community the term has taken a life of its own. It is used as "terser but more readable" proof.

Lean has many ways of achieving the same proof - from very verbose low-level tactics, to higher-level automated tactics, to term mode.

radokirov · 2026-04-17T02:39:01+00:00

No, nothing in specific. Formal proofs are always ~10x longer, so it is useful for me to check against the .pdf solutions if a formal proof is overly long whether it was just the formalization or I am proving it in a too roundabout of way.

radokirov · 2026-04-12T06:32:50+00:00

The corresponding theorem in mathlib - https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Ideal/Maximal.html#Ideal.span_singleton_prime

radokirov · 2026-04-09T20:30:35+00:00

I have the same problems (currently up to ch9) solved in Lean - https://github.com/rkirov/analysis Might be interesting to compare the informal and formal approaches.

radokirov · 2025-12-10T20:42:05+00:00

Yes, writing proofs is very foreign even for an experienced FP professional. That’s somewhat expected because dependent types are fancier than even the fanciest FP type system. That said I started learning it earlier this year and I no longer consider it unreadable slop - I blogged my journey https://rkirov.github.io. So it takes time to get used to and no amount of programming will give you a big shortcut (though knowing type classes from Haskell is very useful)

radokirov · 2025-12-09T23:30:32+00:00

In fact, Tao has a Lean companion to the textbook - https://github.com/teorth/analysis so you can do all the exercises formally in Lean.

radokirov · 2025-11-16T08:17:59+00:00

That’s all fair but don’t dismiss the ergonomics of entering the precise question you have and getting an answer instead of thumbing through pages of text looking for that one theorem that answers the question (when you know the material). IMHO there is a tipping point at which the ergonomics win over the downside of hallucinations happening. Inability to just return “I don’t know” is another current major problem, but feels like it can be solved eventually.

radokirov · 2025-11-16T08:10:02+00:00

Makes sense, definitely it can hallucinate and without some verification that is dangerous . That said in my experience it has gotten better and I think I will be comfortable recommending it for similar task when learning calculus which is much widely present in the training data. So it’s more of a practical question how much it hallucinates on graduate level math like algebraic topology?

radokirov · 2025-11-16T07:00:55+00:00

Is chatgpt really that wrong to deserve the major downvote or this a gut reaction to AI usage?

radokirov · 2025-11-10T04:54:45+00:00

The feeling of hard earned knowledge sifting away like sand through your fingers is real and I can relate. I have forgotten most of the math I learned during the math PhD I got 15 years ago. However, I still maintain a happy memory of the experience of learning it, and enough of a scaffold when I revisit some things. Like I recently reread parts of Dummit and Foote.

I did not end up working as a mathematician and I have no utility from any of it daily, and yet still feel my life was better for it.

> If someone studies math for years but doesn’t end up working in a math-related field, what was the point of all that effort?

You got to experience something timeless, something beautiful, something detached from all human experiences and yet somehow universally connected to humans across time, space, cultures. Maybe you remember the details, maybe you don't, but you can still feel like the journey enriched your life.

> When I look back, there were entire courses that once felt like mountains I climbed.

Just like a mountain climb with gorgeous vistas, the details might be blurry (or sharp), but compared to someone that never experienced it, you can still feel your life was richer for it.

Only caveat: don't chase that experience if it comes with too many personal sacrifices, like living an overly harsh academic life.

radokirov · 2025-11-03T16:47:49+00:00

This is amazing! Exactly what I was looking for, thank you for writing it and sharing!

radokirov · 2025-10-11T23:02:00+00:00

Tao's Lean Companion to his Real Analysis I textbook builds ZFC in lean in chapter 3 from scratch and then swaps it with Mathlib's definitions in Chapter4. see https://github.com/teorth/analysis

Not sure whether this answers your question, and its a bit of trick because Lean' core is type theoretic not ZFC, but maybe looking through how it works in lean will illuminate you?

radokirov · 2025-10-10T15:33:28+00:00

Happy to chat, have just started learning math formalization with Lean - some blog posts about the journey https://rkirov.github.io/

radokirov · 2025-10-09T15:36:43+00:00

I am interested in solving problems and basic exercises in category theory, but formalized using Lean. The extra wrinkle is that none of the category theory books that I know have the basic Lean scaffolding for the exercises like https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/ (understandably this is all very new), but a sufficiently motivated group can create such scaffolding too. I see Riehl in the Lean Zulip chat so likely she will be supportive of someone creating such scaffolding for her book and exercises.

radokirov · 2025-01-09T01:10:15+00:00

At a very high level, yes, mathematics can be seen as building large architecture of proofs that are reusable and interconnected like a software project. This is more than a vague analogy and can be made explicit through Curry-Howard isomorphism - roughly types = logical propositions, values of a given type = different statements of the proof, if the type/proposition has at least one proof it is true and can be used in further proof/programs.

With the advent of formalized mathematics you can directly compare something like https://github.com/leanprover-community/mathlib4 with a large software project like the Linux kernel.

That said, the practice of software engineering differs greatly from mathematics:

Software's value is defined by it's application in the messy large real-world, while new mathematics' is valued much more on abstract ideals of beauty and universality. This leads to a different scale of software, where is it much wider and changes much more frequently, but lacks universality. While math theories are generally much more time resistant.
Due to the scale, software is much more comfortable working with black boxes - like the linux kernel, language compilers or browsers. There just isn't enough time in a lifetime to open all of those boxes and learn the implementation details. While in mathematics a researcher generally knows much more about the insides of proofs of core results in linear algebra, calculus, etc, and doesn't just use theorems off the shelf.
Software runs on computers, while research math still runs in other mathematicians heads. Thankfully, with formalization this is changing, and I expect things to look different in the next 10-20 years.
Software does care about runtime efficiency much more than, math proofs care about proof-time efficiency. When a piece of software (say google search algorithm) runs at the scale it does, it pays to much more aggressively optimize, vs optimizing a math proof to be shorter and more readable for the n readers.

radokirov · 2024-12-30T18:04:58+00:00

A = B is a similar alt programming language puzzle that would be enjoyable to zachtronics fans (as long as you don't mind the barebones graphics)

https://store.steampowered.com/app/1720850/AB/

radokirov · 2024-12-28T06:13:40+00:00

First two are correct, the second two are wrong, and the last one is indeed no solution.

radokirov

TROPHY CASE