[HN Gopher] A Lean companion to Analysis I
___________________________________________________________________
A Lean companion to Analysis I
Author : jeremyscanvic
Score : 147 points
Date : 2025-05-31 16:55 UTC (6 hours ago)
(HTM) web link (terrytao.wordpress.com)
(TXT) w3m dump (terrytao.wordpress.com)
| danabramov wrote:
| I'm super excited about this. Hope it gets moved to its own repo
| so it's easier to find and send to other people. I was always
| curious about math, and Tao's Analysis was the first textbook
| that really showed me how it can be constructed in a rigoruous
| way my programming brain was hoping for. Then I got a bit into
| Lean, and similarly it was very satisfying but Mathlib is a bit
| complicated to learn math concepts from. So it's nice to see a
| bridge from the book to the tool.
| dilawar wrote:
| Same here. I learnt about convergence, Cauchy seq etc. it was
| published by a local non profit publisher -- Hindustan Book
| Agency so it was super affordable too.
| practal wrote:
| I am wondering how much this "prove isomorphism to Mathlib
| equivalent" is relevant. By this I mean, would anything change if
| the isomorphism part would be left out, i.e. is it actually used
| anywhere, for example for automatically translating theorems?
| titanomachy wrote:
| If nothing else it has pedagogical value, convincing yourself
| that the set and operations you established are the "same" as
| the ones you're using for the rest of the book.
| danabramov wrote:
| I loved that from the pedagogical perspective personally.
| When I dreamed about this textbook getting formalized, I was
| worried about how unwieldy the formalization could become if
| it strayed too far from Mathlib -- but also was worried about
| losing the self-contained-ness if it just used Mathlib. This
| is a nice compromise imo.
| nextos wrote:
| It's nice to see theorem proving gain some momentum in a
| mainstream mathematics topic such as analysis.
|
| In PLT, we already had a flagship book (The Formal Semantics of
| Programming Languages by Winskel) formally verified (kind of,
| it's not a 1-to-1 transcription) using Isabelle (http://concrete-
| semantics.org) back in the mid 2010s, when tools began to be very
| polished.
|
| IMHO, if someone is interested in theorem proving, that's a
| _much_ simpler starting point. Theorems in analysis are already
| pretty hard on their own.
| cole-k wrote:
| I wouldn't be too surprised if PL proofs were simpler to start
| with. Part of what I hear people say is that they also are a
| lot more routine. Do structural induction, apply the IH to show
| an invariant holds, continue. I haven't done much theorem
| proving, nor have I done any "mathematical" (e.g. analysis)
| proofs with a theorem prover, but it makes me wonder how much
| skill transfer there is between them if "mathematical" proofs
| require a much different approach.
|
| I will also mention Software Foundations in Rocq (perhaps there
| is a Lean port). I worked through some of the first parts of it
| and found it quite pleasant.
| zozbot234 wrote:
| It will be incredibly interesting to assess how the mainstream
| "textbook" approach to the subject compares to the one taken in
| the Mathlib. In general, formalized math libraries make it
| comparatively easier to state results with a maximum degree of
| generality and to refactor proof developments for
| straightforwardness and elegance.
|
| (Refactoring is of course made easier because the system will
| always keep track of what follows logically from what. You don't
| have that when working with pen and paper, so opportunities to
| rework things are very often neglected.)
|
| It is a natural question also to ask whether it makes sense to
| teach the Mathlib, "maximum generality" version of real analysis,
| or at least something approaching that, in an academic course.
| Same for any other field of proof-based math, of course.
| krapht wrote:
| Certainly not for introductory courses. There's already too
| much on the table - how to prove, how to program, and the base
| material itself.
|
| I believe that's the experience of faculty who've tried as well
| - it's fine for advanced students, but a waste of instructional
| time for the average pupil.
| ubj wrote:
| To me, the most exciting aspect of teaching mathematics using
| Lean is the immediate feedback. If a student's proof is wrong, it
| simply won't compile.
|
| Previously, the only feedback students could receive would be
| from another human such as a TA, instructor, or other
| knowledgeable expert. Now they can receive rapid feedback from
| the Lean compiler.
|
| In the future I hope there is an option for more instructive
| feedback from Lean's compiler in the spirit of how the Rust
| compiler offers suggestions to correct code. (This would probably
| require the use of dedicated LLMs though.)
___________________________________________________________________
(page generated 2025-05-31 23:00 UTC)