Play-testing progress

Stream: Analysis I

[Louis Cabarion]

The Lean formalization of Analysis I consists of the 12 parts listed below.

Which of these are known to have been "play-tested": that is, verified by someone successfully filling in all the sorrys?

• Chapter 2: Starting at the beginning: the natural numbers
• Chapter 3: Set theory
• Chapter 4: Integers and rationals
• Chapter 5: The Real numbers
• Chapter 6: Limits of sequences
• Chapter 7: Series
• Chapter 8: Infinite sets
• Chapter 9: Continuous functions on $\mathbb{R}$
• Chapter 10: Differentiation of functions
• Chapter 11: The Riemann integral
• Appendix A: The basics of mathematical logic
• Appendix B: The decimal system

cc @Rado Kirov

[Rado Kirov]

Chapters 2-5 and appendix A fully. Solutions at https://github.com/rkirov/analysis

[Rado Kirov]

I have been a bit side tracked recently:

• tried to contribute to SL2 finite subgroup classification with @Alex Brodbelt, but code reviews have stalled there.
• doing a weekly meetup in San Francisco to go over the exercises together. We just met for the second time yesterday and got started on 2.2 exercises. It's pretty slow going, folks don't have much time outside work to put into this, so unlikely that group will catch up.
• started trying to write a companion to Category Theory in context - https://github.com/rkirov/category-theory-in-context-lean too

That said, plan to get back to trying to finish the rest of the chapters, working through 6.1 right now.

I am kinda curious to do some experiments with current AI tools - I got beta access to aristotle, and I paid for claude code to see how many sorries they can just "vibe prove"

[Rado Kirov]

How is your progress on the exercises going? Anything particularly gnarly in chapters 6+? For me chapter 3 was the hardest because of working with foundations like custom functions and Fins. Maybe 5_epilogue too because there was little scaffolding (I should contribute some from my solution back).