Chapter 4 done and question about 4.4.3

Stream: Analysis I

[Rado Kirov]

Recently finished all of chapter 4 - https://github.com/rkirov/analysis. The math gets a bit harder, while the lean work gets easier. I would say I went from 5% time thinking about the math and 95% fighting with the lean type checker to maybe 20/80. Of course, I am myself getting more proficient in Lean too, so that helps, but generally the proofs are shorter.

One final question is exercise 4.4.3 ends with Is the axiom of choice required to establish this proposition?. This feels like the perfect example to show how such questions become automatable in Lean. But I think based on previous discussion practically we use .choice everywhere (even to prove LEM, which is weaker), so the fact that we just formalized everything doesn’t help us answer it? Am I correct?

[Terence Tao]

I actually plan to delete that sentence from the next edition, as the axiom of choice has not yet been formally introduced. But, yes, Lean and Mathlib are currently not optimally set up to be able to detect whether the axiom of choice is really used in a proof (also, given that proofs in Lean proceed via type theory rather than set theory, the assertion that a Lean proof uses choice is subtly different from the more conventional assertion that a proof in set theory uses choice).