Introduction: Dan Abramov

Stream: new members

[Dan Abramov]

Hi folks! My name is Dan. I have a software engineering / frontend background. I've been curious about math since I was a kid, never seriously pursuing it. A few years ago I started going through Tao's Analysis book which I really liked because of how rigorous it was — it felt like I can really "trust" the definitions because nothing was hidden or implied. I got through a lot of exercises there but felt frustrated I can't "run" them the way I do with code.

Recently, I've decided to try to pick up mathematics again, and Lean seemed like a natural way to do it. I'm worried that I'm not going to do well because of my missing mathematics background (I dropped out of uni on the first year) but I'm going to give it a fair try and see if it leads me anywhere. I'm currently going through the NNG (will probably finish today) and then planning to start Mathematics in Lean.

In the longer run, I really would love if I could gain enough context to meaningfully contribute to digitizing mathematics or at least to Lean itself or the community tooling (like NNG itself). If there are any virtual study groups or anything of the sort where I can find peers who are at a similar journey, I'd appreciate pointers. Feel free to just say hi as well. Cheers.

[Bryan Gin-ge Chen]

Welcome! Don't hesitate to ask any questions you have about math, Lean, or our community tooling here. You may have already seen the learning resources page, but If Mathematics in Lean is too tough-going, you might also try the Mechanics of Proof which is aimed for people with slightly less mathematical experience.

[Dan Abramov]

Thank you! Will see how it goes. Funnily enough, when I was going through Tao's book (and sometimes checking answers against the internet), it was mostly the mathematicians' "unindented" and dense convention of writing proofs that was difficult to me. The way I tend to write mine (pic attached) seems a lot more similar to proof checkers (though I didn't know that at the time). So I'm optimistic that hopefully it won't be too hard.

Screenshot 2025-01-31 at 17.24.28.png

[Bryan Gin-ge Chen]

Figuring out good ways of displaying proofs (informal and formalized) is definitely something a lot of people here are interested in!

[Johan Commelin]

Welcome! In terms of study groups: there might be some other Lean enthusiasts near you. There is a map here: https://leanprover-community.github.io/meet.html
There is also some activity in #Geographic locality where people organize meetups.

[Kevin Buzzard]

@Dan Abramov hi! If you want to write some more Natural Number Game then I have plenty of ideas :-) (e.g. we want a prime number world with the boss level being to prove that 2 is prime ;-) The hard part will be formally checking that 2 isn't something like 29385734958739857*459487694876, so we would need to use the theorems in inequality world and possibly add new ones (for example I'm not sure I proved a<=ab if b>=1, which will be crucial for proving 2 is prime). But if you'd appreciate something more serious then several people have had a crack at Tao's Analysis book in the past.

In my experience, what works best to start with is that you formalise some mathematics which you already understand. This gives you some feeling as to how the language works, and when you've struggled through the proofs you triumphantly post them here and you'll find that people in the community will just give you code review and by the end of it your proofs will be much shorter and more idiomatic.

[Li Xuanji]

Welcome! Do you work on react? (The name looked familiar to me :smile: )

I'm a new member myself, and one of my side projects is formalizing my undergrad analysis textbook (around the same level as Tao's textbook). The proofs end up looking really similar to the one you have there, if you're interested in a study group based on that!

This gives you some feeling as to how the language works, and when you've struggled through the proofs you triumphantly post them here and you'll find that people in the community will just give you code review and by the end of it your proofs will be much shorter and more idiomatic.

@Kevin Buzzard , is there an channel or post format for these? I would love to get some reviews about "how could I write this more clearly", instead of / in addition to "how can I solve this problem I'm having"

[Johan Commelin]

This channel is (amongst other things) for that type of questions.

[Dan Abramov]

Hi @Li Xuanji! I used to work on React, yes, though not actively anymore. I'm definitely curious about your ongoing formalization. Maybe it would make sense for me to get through the NNG, then through a few chapters of MiL (and just getting the local setup running), and then checking out the state of your side project? Is it up somewhere?

[Li Xuanji]

Yes NNG is widely regarded as a great starting point and it's how I first learned!

If you want to look ahead after NNG, I forked my work from kevin's course notes, which are much more well-annotated than mine. I do try to stick more closely to the proofs in my textbook, which forces me to learn new things. I think the course notes, MIL and MOP are all good second steps after the NNG (I've done a bit of the first two)

[Kevin Buzzard]

@Bhavik Mehta do you have a 2025 version of those course notes with a more recent version of Lean 4? Those notes linked to are a year old.

[Julian Berman]

https://github.com/b-mehta/formalising-mathematics-notes I believe, if my GitHub timeline helped me stalk Bhavik correctly a few weeks back.

[Derek Rhodes]

@Dan Abramov, I'm also a dropout programmer interested in math and started a similar journey. I'm still a noob, so take this with a grain of salt, yet I feel compelled to offer a word of caution. The natural numbers games will not be enough. After going through the games, I highly recommend working through The Mechanics of Proof. But still, that probably won't be enough. You might then do what I did and attack analysis. I bashed my way through the proofs up through lecture 6 of (real analysis 18.100A), but realized it's just not the right way to do it because although it is possible to build things from the ground up, as we programmers like to do, it really is a mistake. Why? Because formalization is an art in and of itself, and as far as I can tell the language used to organize Mathlib is abstract algebra. @Kevin Buzzard's course called Formalizing Mathematics is an intro to the art. I made it to the Normal Subgroups sheet before needing to retreat and now am working through a set of abstract algebra lectures on youtube. That is to say, I would recommend doing abstract algebra (knowing haskell will not suffice) before analysis because it will be easier to navigate Mathlib, which is helpful when using Mathlib definitions, instead of using what seems like a good enough definition that merely works when learning the math, which might be rewarding, but probably won't generalize as well. (To conclude this cautionary note, because of my ignorance, I now need to go back and rework my proofs from those 6 lectures I mentioned earlier so they use Mathlib definitions)

[Li Xuanji]

Yeah, I have to agree that learning Lean and the math subject you are formalising at the same time can be difficult. My analysis textbook is pretty rigorous but it skips proofs for "obvious" stuff like $\sqrt{x^2} = |x|$ or "given a sequence and a finite number $n$, there exists $M$ such that $M$ is greater than the first $n$ terms of the sequence", and most of my effort was in finding out what is Mathlib's name for the relevant theorem, or coming up with a proof from scratch, basically activities that are not "learning analysis". Luckily I did learn the math in school many years ago, but I hope in a few years Lean could improve to the point where you it could be a much more useful tool in math education. That's partly what attracted me (I'm primarily a software engineer) - I like API design / documentation and designing an API for math this is like the ultimate API design challenge.

[Julian Berman]

Yeah, I also count myself in this kind of group -- my advice is somewhat short I think, namely -- doing math + doing math in Lean is hard or frustrating at times but persistence and willingness to try a bunch of different things in the learning process, even if you abandon some when you run out of steam, are your friends, and contributing to Mathlib is definitely not out of reach. In terms of what math to do I think "follow what you end up being interested in as you learn or see more things"; the nice thing about being in a degree program is you get a tour of the common subfields, but without such a thing, you just get to play and figure it out I suppose -- I do think that your original study group question is a good one to have asked because what can be frustrating is to bump into some mathematical structure you don't know about and trying to learn about it becomes this big annoying backtracking exercise to learn whatever prerequisites you're missing. You can get around that either by talking to someone who can help you navigate or else by following some resource (as you're doing) which builds things a bit more "from scratch".

[Li Xuanji]

@Derek Rhodes definitely hear you about "you will need to go back and swap out definitions in the future", after all Mathlib has to write things in the generality it does for a reason; my hypothesis (which remains unproven!) is that for education it's best to "cut over" (e.g. switch from a non-filter definition of limits to a filter definition), at some point in the "textbook" instead of using the same generality from the start

[Derek Rhodes]

@Li Xuanji, about the "cut over", that makes a lot of sense. I bet educators have a name for that, and maybe some techniques to help facilitate those sorts of conceptual jumps.

[Dan Abramov]

A small status update for this week (mostly to hype myself up a bit and to stay accountable).

I've fully gotten through NNG and the first two chapters of MIL (Introduction and Basics). MIL has been incredibly helpful so far, it seems like learning by doing is the way to go here.

The hardest part so far has actually been not Lean itself (I think I'm getting the grasp of it) but proofs that needed picking "just the right" substitution. I spent a day on mul_inv_rev and couldn't crack the expression that was needed. Also spent a day on showing distribution laws on lattices imply each other (and didn't crack it). I've had to actually look at the solutions and retrace them step by step to see the mechanics of both proofs. This left me frustrated as I'm not sure whether I'm just not cut out for this. I do understand the mechanics in retrospect though.

Anyway, I'll keep going through MIL. I'm also thinking of picking up Formalizing Mathematics in parallel at some point, or maybe after MIL.

[Kevin Buzzard]

Distribution laws on lattices implying each other (if we're thinking about the same theorem) is a super hard question of the kind that we put on the end of undergraduate problem sheets expecting very few people to be able to do it.

There are two completely different things here; there's figuring out mathematics yourself, and there's translating mathematics which you understand the details of into lean. The first is done by professionals or students trying to learn mathematics. Trying to learn lean is a very different thing, there the art is not figuring out the math details but figuring out the best way to implement them in a programming language.

[Chris Wong]

I wonder if, for those questions, we can add some hints that help with the mathematical side.

[Chris Wong]

Proving that the Kleene algebra laws imply each other is similarly difficult. I had to fish out an old paper for the solution.

[Rado Kirov]

Hi Dan, thanks for sharing your progress (and please keep sharing to exchange notes). I am similarly trying to pick up Lean and formal math. Did you finish https://leanprover.github.io/theorem_proving_in_lean4 before MIL? I and half-way through that tutorial after NNG and STG before starting MIL and I find it good as a first tutorial to sketch the interesting language areas without getting overwhelmed. Also it makes the term vs tactics distinction very clear.

I find myself keep getting distracted by how uniquely different dependent type languages are from PL perspective before even getting into using them for math (features like implicit arguments, infinite higher kinded types/universes, etc).

[Dan Abramov]

That's an interesting approach! Personally I find that I need some exercises to stay engaged and not fall asleep so the tone of TPIL isn't quite right for me yet. I'll probably refer to it to catch up on the type system though.

[Rado Kirov]

Makes sense. There are some exercises in TPIL - https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#exercises but they are just bundled at the end of pretty long chapters and start in chapter 3.

[Dan Abramov]

Another weekly checkin / status update (hope these are okay!)

This one was noticeably more challenging but I've gotten through chapter 3 of MIL and its exercises.
Starting Chapter 4 tomorrow. No other updates really.

[Dan Abramov]

Another check-in!
I finished Chapters 4 and 5 of MIL (and their exercises).

A few thoughts/impressions so far:

• Learning by doing works great. I find it most helpful to first do MIL exercises as stated (with or without using hints), and then redo some of them completely from scratch (deleting the original scaffolding and only leaving the statements). While redoing things from scratch, I tend to bump into new stumbling blocks I haven't noticed. Stepping though existing proofs is much less helpful because it doesn't expose those gaps.
• It's not a great idea to learn new math at the same time as formalizing a result about it. If I'm stuck while formalizing and I also don't understand the mathematical argument, I get very demotivated. I've found it helpful to first gain intuition about the mathematical argument by drawing pictures. And then when the intuitive argument "makes sense", I try to formalize a strict written version of the argument. If I get stuck in formalization, I can fall back to the strict written version to pick it back up — and if I don't understand that — I can fall back to the intuitive picture to understand the argument.
• Unlike most programming I've done so far, it feels actually usefiul to break things down into smaller pieces before completing those. I.e. writing almost "inside out". For example, if I get stuck formalizing some detail, I can backtrack and formalize a sequence of "larger" steps with sorrys for each of them, and at least get those to click. So there's a lot of "zooming in" and "zooming out" that can be done at any point of the proof, and I don't have to approach it linearly.
• I find it helpful to keep my own cheat sheet of tactics.
• What's still hard: sometimes there's stuff that feels like it should be easy ("I need to get rid of / 6 on two sides of this thing!" or "x divides y, but I need it to divide 3 * y") but I spend unreasonable time on it. I'm getting better at this but just searching for the right lemma or figuring out the right way to "plug it in" is tedious. Hopefully I'll improve on this.

I plan to keep going through MIL for now since I'm just about halfway through it. So far I enjoy its mix of theory and practical exercises.

[Rado Kirov]

What's still hard: sometimes there's stuff that feels like it should be easy ("I need to get rid of / 6 on two sides of this thing!" or "x divides y, but I need it to divide 3 * y") but I spend unreasonable time on it.

I similarly (on chapter 3 of MIL so far) found it frustrating to want to apply rewritings that are trivial (at least on paper) but I don't know the name of - like ... + b = ... to ... = ... - b. I tried the following:

• (the recommended in the text) guessing the name and using symbol autocompletion
• navigating into the mathlib file with other algebraic identities and looking around.
• asking claude
• trying what github copilot suggests
• https://loogle.lean-lang.org/
• extract to a simple example (a b c: Z) : a + b = c -> a = c - b and use hint tactic.

The last one is probably the best, but sometimes it suggests "too powerful" tactics like linarith that are not as educational.

[Matt Diamond]

@Rado Kirov you could also try exact? with the simple version

[Rado Kirov]

Ah right, I think that's the best approach (at least for me)! One can even do it inline in the current proof with have : and then just delete it once they know exact name.

[Dan Abramov]

Love this idea (extracting a simplified version and then using exact?). Never occurred to me. Thanks!

[Damiano Testa]

There is also extract_goal that helps produce a standalone version of the current goal that you can then copy-paste and try to solve separately.

[Kevin Buzzard]

This "I want to turn X+b=Y into X=Y-b so I just break out of the proof and write a standalone statement of what I want and then run exact?" trick is something I use again and again and again, because I seem to be too old to accurately remember the names of the hundreds of lemmas which do these operations (I'm sure there are plenty of people here who know exactly what the lemma a + b = c -> a = c - b in additive groups is called but I certainly don't)

[Ruben Van de Velde]

I'm guessing it's something like eq_sub_of_add_eq, but there's so many variants with the additions and equalities swapped that I only get the right one by accident

[suhr]

I would guess something like add_sub_cancel ▸ congrArg (· - b), but for additive groups it's add_neg_cancel for some reason.

[llllvvuu]

the specific case removing things from a goal can often be done with congr / gcongr. removing things from a hypothesis (/ adding things to a goal) is more tedious though, and the suggestion to use exact? (on abstracted forms) is a good one. Over time you do develop spidey senses for what keywords to use in mathlib docs, how to Loogle, what broken down steps are most likely to be closable by automation, etc.

I actually think Lean livestreaming could be an interesting category as there is a lot of micro technique involved, as well as debugging strategies (e.g. convert, various set_options)

[Dan Abramov]

A little check-in. I've been slacking off in the past week due to jetlag from moving (temporarily) to Japan, but am trying to pick up the pieces now.

I made it through the Chapter 6 of MIL but found it increasingly boring. I'm not sure whether this has to do with the verbosity of defining structures, or whether it's the example itself (Building the Guassian Integers) that doesn't excite me. I'm mostly able to follow along the explanations but I feel too "checked out" to follow the actual proofs. The exercises aren't interesting (I'm supposed to fill in tiny details) and the meat of that proof makes me want to sleep. I'm not sure why it "feels" so different from the Schröder-Bernstein Theorem exercise which I enjoyed quite a lot more.

I have now started Chapter 7 but I'm again falling asleep in the first paragraphs. I think partially it's because the style of the book has changed (there was a fast theory/practice loop in the earlier chapters; this one takes more time to build things up before giving some practice). It's also gotten more abstract (I thought I would enjoy that but I'm not sure now). And the constant use of subscripts is throwing me off and feels annoying.

Okay, let's be honest, I think I hate these chapters. I'll probably have to pivot to some other material on these topics before I start hating Lean itself.

I'm lowkey wondering whether it's time to jump off MIL. It may be possible that subsequent chapters are just too much of a slog to get through if I don't already know the relevant mathematics. I suspect that to be motivated, I need to not only have some idea of, but also enjoy the mathematics involved, and this text doesn't convey much enjoyment for me to pick up by osmosis. I'm not sure what to do next though. Possibilities include:

• Trying my own project (e.g. formalizing something from Tao's Analysis book)
• Going through https://github.com/ImperialCollegeLondon/formalising-mathematics-2024/tree/main/FormalisingMathematics2024
• ???

I definitely need something to bump my level of enthusiasm, ideas welcome...

[Damiano Testa]

I would definitely try to formalise something that you like!

[Johan Commelin]

@Dan Abramov My instinctive explanation for why you don't like those later chapters is that they are written for an audience that has little programming experience, and for whom structures and typeclasses are completely new topics. Whereas you already know the whole CS side of things. So it's going to be a boring pace for you.

[Damiano Testa]

You can use the books as references for when you get stuck. And certainly zulip!

[Dan Abramov]

@Johan Commelin Yea it's a bit like the worst of both worlds — although I'm new to typeclasses, I can sort of figure that out based on the examples, however I am new to the actual structures (monoids, groups, domains, etc) but the text obviously doesn't spend time motivating or explaining them.

[Damiano Testa]

I think that most resources assume either a maths background and explain the coding side or the other way round.

[Damiano Testa]

I also think that learning both simultaneously is really hard.

[Johan Commelin]

@Dan Abramov Have you looked at Theorem Proving in Lean #tpil already?

[Dan Abramov]

Not yet! On my list.

[Johan Commelin]

But actually I think it sounds like you are ready to start on a more challenging project. Which area of maths are you most excited about? Analysis? Topology? Algebra? Combinatorics?

[Johan Commelin]

Ok, I suggest skimming through #tpil. Or just keeping it at hand, while working on a project, to reference now and then.

[Johannes Choo]

Hi Dan! We extremely briefly interacted in 2022 on then-twitter when you mentioned some interest in proof assistants. I actually have some opinions regarding the learning materials that I mentioned in a DM to an acquaintance; perhaps I should have discussed them publicly at an earlier opportunity, but this present conversation isn't so bad either:

Hey I recently tried out both MiL and The Mechanics of Proof (TMoP, https://hrmacbeth.github.io/math2001/ ), and I recommend working through The Mechanics of Proof, and skimming through (especially the latter half) MiL. In this case, the main object of working through TMoP is to become very familiar with the basic and general tactics that you use (even though TMoP uses weaker variants that you would normally use).

The main objective you should have in mind when skimming through MiL, especially the latter topical chapters, is to mentally bookmark sections and chapters to go back and refer to thoroughly when you encounter a situation that might need them. So when you encounter, say, where you need to prove that two functions are equal you look back at section 4.2 to see that you should use ext for functional extensionality, and when you want to define your own algebraic structures or have a typeclass inference issue you want to understand better you look at chapters 6 and 7. I'm still regularly referring to MiL to orient myself to the main results and style in the various topics in addition to the Mathlib 4 documentation and moogle.ai, when working on undergrad mathematics, so it seems that there's not much value in front-loading going through the topical chapters thoroughly since it's still insufficient.

[Dan Abramov]

Re: what I'm most excited about in math, I'm really not sure, and that's part of the problem — I never dived deep enough into math to know for sure what I'm into.

"Beautiful" results are what attracted me to mathematics in the first place, e.g. learning that the sum of 1/n! was e, or that you could get pi/4 from 1 - 1/3 + 1/5 - ... and so on. I'm not sure infinite sums in particular are the object of my interest (from what I understand, many of them are concrete examples of more general results that don't feel as exciting). But there's something about infinite things in general, and ways of dealing with them, that's exciting to me. I think being able to "traverse infinities" is what makes mathematics unique.

I guess anything that's a little mindbending is a good candidate. It's why I liked Schröder-Bernstein Theorem as an example. It deals with infinite and it's a bit mindbending, but once you get it, you get it. I also found this writeup about blue-eyed islanders — I doubt I have the chops to seriously attack this formalization, but just learning about the separation of Syntax and Semantics, and notions of completeness and soundness (and how they relate), was very mindbending. I had a few dreams about the relationship between ⊢ and ⊧. I hope to eventually understand the constructions necessary for the Godel theorems but I suspect this is also way off.

Regardless of what I enjoy, I think I'd have to get familiar with more basic fundamentals that show everywhere, at the very least anything covered in Tao's Analysis, as well as some basic Group theory. Even if it isn't particularly "exciting" on its own (but maybe it is?)

In the Analysis land, I feel drawn to "fancy" functions like learning about the Gamma function. It would be nice to learn about different "strange" functions and how they're connected.

[Kevin Buzzard]

For me, theorems about $\mathbb{Z}[i]$ are super-exciting because I am a professional number theorist and I find the internal structure of rings such as this one intrinsically interesting. I immediately think "is there a version of the unique factorization for $\mathbb{Z}$ which holds for this ring? What needs to be changed in order to make it work, or is it unsalvageable?" etc (answers: unique factorization is true when interpreted correctly for $\mathbb{Z}[\sqrt{-1}]$, it doesn't work for $\Z[\sqrt{-3}]$ for a fixable reason (you need to throw in $(1+\sqrt{-3})/2$) and it doesn't work for $\Z[\sqrt{-5}]$ for an entirely different and very profound reason which is only fixed by redefining your concept of number). The examples of what excite you (Schroeder-Bernstein, Goedel) leave me cold so it sounds like what's going on is that we're interested in different material. The stuff which you're finding exciting is much closer to the kind of maths which is taught in CS departments, so maybe you're reading the wrong book.

[Damiano Testa]

Do you know the books "Counterexamples in ..."? For instance topology: I always liked these kind of weird examples. I do find that they get a little repetitive after a while, but I also think that some of them could be fun formalisation projects.

[Kevin Buzzard]

Yes another thing which came out of Dan's post was "I am interested in concrete results such as $\pi/4=1/1-1/3+1/5-\cdots$ and concrete functions such as the $\Gamma$ function" whereas I suspect that many mathematicians are more interested in abstract results such as theorems about when sums converge or abstract spaces of functions.

[Kevin Buzzard]

I think my advice to Dan would be that if you're bored with or finished with the teaching material then it's time to find a project of your own. One topic which links the Gamma function and the $\pi/4$ result is the theory of hypergeometric functions, which are related to combinatorial identities and which AFAIK we don't yet have in mathlib.

[Johan Commelin]

Note that there was a thread about them a while ago: #maths > Hypergeometric functions

[Dan Abramov]

FWIW I think it's not necessarily that the math itself was boring in that example, but it was essentially glossed over (I would've liked some intuition on prime vs irreducible — it was news to me that these are different concepts and I would gladly spend a few pages just diving into different examples showing in which structures they don't coincide, in which structures one implies the other, what's a good intuition for either of them, etc). But since this isn't a math book, most of the focus was on translating an inequality into a tedious formalized form — and unlike the earlier chapter, the reader wasn't meant to fill any essential parts of the proof so it felt very non-participatory. I think this just seems like more evidence that I should get excited about the relevant math first from other sources, then try to look at formalizations of that.

[Marc Huisinga]

Regardless of which avenues you want to explore in mathematics, Theorem Proving in Lean 4 and doing some verified functional programming with Lean may also be fun avenues to explore :-)

Some of the code snippets in TPiL4 might be a little bit out of date in new Lean versions, but I'd hope that none of it has diverged too far.

[Johannes Choo]

If you are already familiar with inductive structures and induction, familiar with undergrad CS, and new to undergrad math, you might want to continue with Tao's Analysis through chapter 5 where the reals are constructed, up to chapter 8 where he shows the uncountability of the real numbers with Cantor's diagonal argument, which you might already be familiar with. Cantor's diagonal argument is a workhorse proof technique that is behind a lot of basic logical and theoretical CS results like Goedel's first incompleteness theorem and the halting problem, as well as the time hierarchy theorem.

So regarding why Schröder-Bernstein Theorem is as mindbending as it is, is because it needs to generalize to functions that are dealing with sets that are more than countably infinite, otherwise a much more mundane approach should suffice.

[Dan Abramov]

Checking in — I've decided I'm not quite ready to dive into proving something "real" yet due to missing mathematical knowledge so I've moved on from MIL to FM 2024 instead. It does start from scratch so some content feels repetitive but I'm really enjoying the practice so far and feel more fluent than before I started. I've just finished chapters 1 and 2 but I'm really excited about the later chapters. Mostly because they show how to deal with some mathematical objects I'm curious about but (unlike MIL) don't take pains to establish them from scratch (which is a little much for me right now).

[Huỳnh Trần Khanh]

lol you're literally a person I look up to. math comes in different shapes and sizes. I think for a person with a computer science background it's easiest to learn some... combinatorics. just learn to count stuff in Lean, or find the minimum or maximum value of something

[Huỳnh Trần Khanh]

maybe try high school competition math?

[Huỳnh Trần Khanh]

these problems are fun to formalize. you'll get to come up with bizarre bijections