Repositories/forks with exercise solutions

Stream: Analysis I

[Dan Abramov]

I'm working through the exercises in https://github.com/gaearon/analysis-solutions.

I move at a relatively slow pace, but I just finished 3.5 and hope to get to chapter 4 soon. I try to solve them manually, with some help from Claude here and there when I'm stuck. I also try to reduce them to a minimal form (not necessarily golfed, but conceptually). So if some proof is unnecessarily complicated, I'd appreciate a tip in issues. I'm maintaining my fork as a stack of commits (one commit per section) in the solutions branch that I regularly rebase on top of upstream main. Not sure how long this will stay viable but I'll try to keep stacking them to avoid accidentally diverging.

I know @Rado Kirov also has a fork in http://github.com/rkirov/analysis that I often consult. He's been using a bit more "bruteforce" approach (so not all proofs are shortest) but I found it super helpful to get unstuck and he's further ahead than me.

If you have your own fork with solutions that you'd like to share, add to this thread! I think it's useful to be able to compare them and to see if anyone got a simpler or a shorter solution to different exercises.

[Rado Kirov]

+1 encouraging more folks to share solutions online (I hope that doesn’t have bad effects for people teaching university classes using the book, then again AI can already probably solve a lot of them). I have also learned some neat tricks by looking over @Dan Abramov solutions, so it has been mutually beneficial to share solutions.

[Louis Cabarion]

Is it still the case that no one has successfully completed Section_5_epilogue.lean ("Isomorphism with the Mathlib real numbers") sorry-free? In other words, that level is not "play tested" yet. I'd love to see a solution, so please share if there is one.

[Rado Kirov]

Yes, I am on ch4.2 and going linearly. Will post here once done, but probably will be at least 3 months more :)

[Li Xuanji]

I've been playtesting it on my own branch. Not sure there's anything particularly interesting, but some thoughts:

• Proof automation - I try to use simp as much as possible and I found working through this book really useful to develop intuition about good simp lemma design. I saw that the recent v4.22 upgrade enables grind (albeit experimental), and I'm looking forward to trying that out.
• For proofs that cannot be dispatched by automation, each proof normally only has a small amount of "clever mathematical ideas" (things like case split on this proposition, or rewrite a simpler expression into a more complicated one so that some other theorem can make more progress) and then the rest is much more automation-friendly, so automation is much more fruitful than it might first seem. I find good theorem naming really important to making the code reflect the "clever mathematical idea" and also to see if a given goal state / context is true by inspection without writing a proof. Currently the Lean content of the book is IMO much harder than the math content, but I could see a future where the automation / scaffolding is good enough that this inverts, and working through books like these develop the reader's math skills without placing an unduly high prerequisite on their Lean skills.
• I think there are some interesting questions about the generality in which to state theorems / missing lemmas, e.g. many proofs about CloseSeq have the same basic idea as their Close counterpart... similarly I found the formalization of the finite segment part of exercise 5.1.1 much harder than the math proof and explored a bit how to make it easier
• Anything that I don't personally find interesting (basically anything not already listed) I tend to skip, so I have lots of sorrys, in particular I didn't work on section 3 at all - I'm just personally not that interested in learning how to reimplement / express set theory in Lean, but maybe I'm missing out...

[Rado Kirov]

Currently the Lean content of the book is IMO much harder than the math content, but I could see a future where the automation / scaffolding is good enough that this inverts, and working through books like these develop the reader's math skills without placing an unduly high prerequisite on their Lean skills.

Yep, that's my observation too, but learning Lean more deeply by doing tons of undergraduate math exercises is what I am here for. Lean is programming language and one needs to write tons of code - reminds me of this essay https://www.norvig.com/21-days.html. Also, the Lean scaffolding is improving (@Dan Abramov has sent some great PRs) by filling out example sorries and adding comments.

After chatting @Kevin Buzzard I learned about these two other resources for learning to do math in Lean by doing undergraduate math exercises:

• https://github.com/b-mehta/formalising-mathematics-notes/tree/main/FormalisingMathematics2025

• https://hrmacbeth.github.io/math2001/
  which I plan to go over too at some point. They also seem to have a large number of exercises, but Analysis1 Companion is close to 5x more sorries (if the shell script claude produced is right):

• analysis 1 companion - 2100 sorries

• formalizing math 2025 - 330 sorries
• Mathematics is Lean - 340 sorries
• mechanics of proof - 570 sorries
  The downside of course is that analysis 1 has no actual text teaching you lean, so I have to learn from reading the scaffold, asking claude and zulip, but I like the challenge so far.

[Terence Tao]

I'll be happy to accept PR's to update the various Lean resources in README.md to incorporate these links (and whatever other links you come across that would be helpful for other users of the companion).

[Rado Kirov]

The list here is already great - https://github.com/teorth/analysis?tab=readme-ov-file#general-lean-resources, might just add https://github.com/b-mehta/formalising-mathematics-notes. But the problem is AFAIKT none of the "doing math in lean" texts go far enough to cover some more advanced lean tools needed to complete all the proofs in the Lean companion.

For example, generalize_proofs is very much needed in Chapter 3, but a quick grep shows that none of MIL, mechanics of proof, or formalizing math text mentions it. Same with field_simp or push_cast that Claude just taught me yesterday, so I can complete Ch4.2

Maybe @Dan Abramov and I should write up "A Lean guide to the Lean companion to Analysis I" at some point, because text in the comments can only go so far.

[Dan Abramov]

Though not quite the same thing, I was thinking of recording a YouTube series going through the exercises (while teaching a bit of Lean and the workflow).

[Patrick Massot]

Rado, could you please open an issue in the mathematics in Lean source repository about those missing tactics, in including links to a couple of relevant Analysis 1 exercises? That would be very useful.

[Rado Kirov]

sounds good, will do it tomorrow

[Li Xuanji]

One thing I like about formalising mathematics, which I think the Analysis 1 companion could benefit from, is that the header describes all new tactics the file introduces (i.e. the first time linarith is used, the header talks about what it does), and it had a separate list of all tactics (used in the course) at the end.

Other than tactics, I imagine this could also be applied to language features and library typeclasses.

[Rado Kirov]

@Li Xuanji That's a great idea. What's stopping me from just sending the PRs to do this is while I know the tactics used by my own solutions, I can't tell whether I am using overly powerful ones or not (and even having a canonical tactic power ordering is still WIP, I think there was a Lean thread). So maybe the best path is having a few independent solvers go through the chapters, then we can pull our lists of tactics used and contribute the minimum powerful set.

@Patrick Massot filed #308 #309 #310 #311 for now and will keep doing so as I go along. Feel free to close some of those as won't do, if you don't think they can be well worked into the text.

[Patrick Massot]

Thanks! I cannot promise when we’ll have time to work on this, but be sure this will be useful at some point.

[Rado Kirov]

yeah, no worries, filing those is useful for my own book keeping too.

[Terence Tao]

I have experimentally added a "tips from past users" section to the header files for the Chapter 2-5 files (excluding those for which no sorries were to be filled), which intended to be a crowdsourced portion of the file in which users are invited to submit (as PRs) tips and other comments into the file itself (also external links to content discussing the material in the file is also welcome). The intent is to allow for a variety of perspectives and proof strategies to be represented. Users can feel free to sign their name to specific tips if desired (though in theory github already tracks authorship of contributions). If this experiment is popular I will extend it to the rest of the companion.

[Rado Kirov]

Nice, will contribute some tips after finishing ch 4.