Tao Analysis

Stream: general

[Lucas Teixeira]

I remember sometime ago watching a Xena Project video that suggested formalizing Tao's Analysis using Lean. I was wondering if anyone knows if that project was ever undertaken?

[Johan Commelin]

Not that I know of. But @Kevin Buzzard has a better overview of which projects are going on.

[Kevin Buzzard]

I don't know of any analysis being developed in any places other than melon e branches

[Scott Morrison]

This could be a good exercise. Ideally every numbered lemma in Tao's Analysis (or indeed, in any high-quality "standard" textbook) would be a one-liner given what is in mathlib. Three types of contributions to mathlib that could follow from this ideal:

1. adding statements to mathlib where it's not already a one-liner from existing material
2. adding cross-references to the textbook in doc-strings. (I think having only a handful of these is not valuable, but personally I would be excited about a PR that added a cross-reference to every result in entire chapter(s) of a book like this.)

[Scott Morrison]

Historically, however, it seems very few books have been exhaustively formalised in Lean. More likely people pick an end-goal, and then when they discover something is tough to formalise they sometimes pick a bourbaki-type book to help guide the design, but still only implement from that source what is necessary for their goal.