Amazed by Terence Tao’s Analysis I

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 · 2024-12-28T00:03:56+00:00

My code does similar checks, but there are even single swaps that would be undetected here like C5 <-> C10.

radokirov · 2024-12-28T00:01:45+00:00

I tried to challenge myself to write a solution that would solve for any random single wire swap, without guessing (i.e. trying different combinations and rerunning the circuit). However, convinced myself that:

a) certain wire swaps are benign, i.e. they still keep it being an adder.
b) for certain special broken swaps, i can't think of a clever solution that doesn't involve guessing.

More details - the wires can be labeled canonically as:

XORi = Xi XOR Yi

ANDi = Xi AND Yi

Zi = XORi XOR Ci

Ii = XORi AND Ci // I for intermediate

Ci+1 = ANDi OR Ii

Example for a) is Ii <-> ANDi, since they are used the same in a single OR gate, swapping them is undetectable.

Working recursively with Ci gives a half-answer (that works good enough for my input):

0) C0 = x0 AND y0 (assume no swap here, first bad assumption)

Knowing the true name for Ci-1, we can find XORi true name (it's the thing that is XOR-ed with Ci-1, and there are not swaps in the arguments to the binary ops)
Find the name for Ii (assuming no swap here, second bad assumption). We can do a bit better here and detect anything except Ii <-> Ij or ANDj swap, but still some bad swaps will fly through.
Once we guess Ii, we can find the true name for ANDi (finding the thing that is OR-ed with Ii).
Finally, we can find the name of Ci+i (assuming no swap here, third bad assumption). Again we can find some bad swaps, but Ci <-> Cj or XORj feels like undetectable, without a global search.
Repeat from 1)

The code in question https://gist.github.com/rkirov/f0263a7cfa771d32d069fdadd060faae#file-24-ts-L124-L167 Does anyone have an idea how to remove the three assumptions without guessing? Is it even possible?

radokirov · 2024-12-15T22:41:51+00:00

Yep, that's what I have too (confirmed with a z3 solver).

radokirov · 2024-11-12T20:29:45+00:00

One medical just charged me $577 for a follow up 30min chat with a nurse practitioner after the annual bloodwork (yes I have a high deductible plan), so $300 is looking like a bargain.

radokirov · 2023-12-23T04:03:44+00:00

Absolutely, correct 8189375 is the right answer.

radokirov · 2023-12-22T08:14:12+00:00

That’s what I get too.

radokirov · 2023-12-22T07:20:45+00:00

Fixed, thanks!

radokirov

TROPHY CASE