A Lean companion to “Analysis I”
20 points by mseri
20 points by mseri
Would feel a lot more comfortable buying this book if the author could vouch that the exercises are actually solvable.
Isn’t the main point of formalization that it reduces the chance of errors? If I buy this book, there might be an error in the book that makes the exercise unsolvable. When I, as an undergraduate, work through a beginner’s textbook to Analysis, it doesn’t make sense to require research level skills (i.e. developing new formalisms)
When I, as an undergraduate, work through a beginner’s textbook to Analysis, it doesn’t make sense to require research level skills
I think everyone would agree with you there. However proof assistants are just now breaking through into mainstream mathematics, so using them to formalize an undergraduate text is on the front lines of math these days. The project should be viewed in that light. There may be sharp edges and unforeseen difficulties, but this is also an exciting project because it is accessible to people without a Ph.D. in mathematics, which is required to contribute to most other frontier projects in math.
The page doesn’t mention it, but the book is also available as an eBook. That way, you can print it at home instead of paying $10 USD for shipping and have it get lost in the mail.