Zulip Chat Archive

Stream: general

Topic: Tao Analysis


Lucas Teixeira (Aug 26 2021 at 19:23):

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 (Aug 26 2021 at 20:17):

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

Kevin Buzzard (Aug 26 2021 at 21:43):

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

Scott Morrison (Aug 27 2021 at 00:47):

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 (Aug 27 2021 at 00:49):

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.


Last updated: Dec 20 2023 at 11:08 UTC