Formalization complete

Stream: Analysis I

[Terence Tao]

I have finished formalizing the main content of all of the chapters of Analysis I, including the appendices, with the exception of Chapter 1 (Introduction). Chapter 1 could in principle be amenable to studying using Lean, but it doesn't fall neatly into the "sorry filling" paradigm of the Companion: the questions and topics raised in that chapter either center around trying to make an informal statement more precise (so, the exercise would to state a reasonable Lean formalization of the informal statement), or explaining why a certain informal argument does not work (so, the exercise would be to try to fill a sorry, only to see it fail at a crucial step, for instance because one of the hypotheses required for a tool one wants to use is absent). Also, despite the placement at the very start of the book, most of the content of Chapter 1 actually requires mastering the rest of the book (as well as portions of Analysis II) to properly answer. So, in the end, I could not figure out exactly how to usefully incorporate Chapter 1 into the companion, and have left it out. But I am open to suggestions on whether some Lean formalization of this chapter is still possible.

All the other chapters went relatively smoothly; there were steps that were tedious (for instance, computing explicit limits, or simplifying expressions involving exponentiation, still requires a certain amount of Mathlib lemma lookup, though Loogle is immensely useful in this regard), and some definitions required some initial thought as to how to structure their data and API, but in general the Lean framework (with its typeclass inference system, coercions, and so forth) permitted a fairly direct translation of the definitions in the textbook to Lean equivalents. Though in most cases the Mathlib version was formalized in a more frictionless fashion, and so most definitions became deprecated after the section or chapter in which they were introduced (although a few facts about sequences from Chapter 6 were more convenient to use directly to develop series in Chapter 7, rather than to appeal to their Mathlib counterparts). There were a small number of standalone lemmas that might eventually be upstreamable to Mathlib (e.g., the axiom of unique choice implemented in https://github.com/teorth/analysis/blob/main/analysis/Analysis/Tools/ExistsUnique.lean ), but I have not made this a priority.

I found this formalization to be a great way to sharpen my own Lean skills, and because of this I did not rely strongly on AI tools, even though there were places where that would have accelerated the process. The main use of AI was to use Github Copilot to autocomplete the boilerplate (particularly the way chapters are listed in README.md, lakefile.lean, and other organizational files), and to produce minor variations of an existing lemma or argument (for instance, if I wrote down a lemma to handle sums of (say) series, Copilot could quickly then provide a corresponding lemma to handle differences of series).

In general I have found a "top down" approach to formalization to be effective for complex proofs: formalize the high-level statements in the argument (e.g., as have statements) with the proofs given by sorries, and then formalize the fact that these high-level facts imply the desired conclusion. This then splits up the task of filling in the complex sorry into simpler pieces, which ideally should be rather modular and can be filled in independently of each other. One then repeats the process (using tactics such as congr, gcongr, refine, convert, apply, calc, trans to keep breaking up a goal into simpler subgoals, and "housekeeping" tactics like obtain, rcases, intro, ext, set, constructor, simp to unfold quantifiers and definitions and introduce relevant variables) until one reaches a "routine" task (e.g., verifying some algebraic identity, or computing some explicit limit) that can usually be established by some sequence of rewrites or simp lemmas from Mathlib, at which point the main task is library search. I found that the paradigm of dumping all relevant facts into the context and then using a smart tactic like linarith, tauto, aesop, simp_all, omega, order, or solve_by_elim to figure out how to conclude the goal from that pile of facts to be a convenient way to structure arguments (as compared to manually matching together the inputs and outputs of these facts in some linear order); this also made the proof more amenable to adapting to other contexts (in some cases, one could handle multiple cases of a proof at once by applying all_goals to a block of smart tactics).

I'm grateful to the various "playtesters" who have identified typos in the exercises and submitted ways to improve their pedagogy through numerous pull requests. I will continue to accept such PRs even though I do not plan to add significant additional content to the companion going forward.

[Dan Abramov]

Super exciting! I’m very grateful for this project — I’ve been going through exercises a few years ago but fell off because it was too tedious to do by hand (as a programmer I’m hooked on a short feedback loop). Then I learned Lean, and this project came full circle so I can redo the exercises again and hopefully finish the book.

With that, I was wondering — do you plan to do Analysis II?

[Terence Tao]

I don't have plans to formalize Analysis II currently. If in the future there is a critical mass of students who have largely gone through the Analysis I formalization and are interested in formalizing Analysis II, I might make it a collaborative formalization project (where the statements of the theorems are sorries to be filled). Also I expect by a year or so that AI autoformalization tools will advance significantly and make the process noticeably faster (I feel that I have acquired enough facility with Lean at this point that further manual formalization has diminising returns on my skill).

[Li Xuanji]

I'm interested in working on formalizing Analysis II :eyes:

[Rado Kirov]

Same, very thankful for this project! It is exactly what I needed to progress on my Lean learning after NNG and reading Mathematics in Lean and Theorem proving in Lean. It is well known that programming languages are best learned by programming, one has to make all the errors and learn in conversation with the compiler. I toyed with the idea of just taking some undergraduate textbook and formalizing all results and exercises, but couldn't even get started because I never knew how much is already in mathlib, what to reuse and what to define from scratch. The book is also perfect so far because is does start with axiomatic foundations for natural numbers and sets, so I am not overwhelmed by mathlib right from the get go.