Formalizing Wheeden-Zygmund via Aristotle

Stream: PrimeNumberTheorem+

[Harald Helfgott]

Perhaps it was a matter of finding the (excellent) textbook we needed, written at the right label of detail -

Aristotle is able to formalize passages of Wheeden-Zygmund (well, two passages, so far) essentially verbatim. I've only used ChatGPT to translate well-chosen sequences of screenshots into LaTeX, which I then proofread before giving to Aristotle. What is more, Aristotle found and corrected an actual (and harmless) typo in Wheeden-Zygmund. (That is not the most surprising part, but I am still impressed.) S
Hardy Tauberian theorem.lean
Hardy's Tauberian theorem.md
See attached.

[Harald Helfgott]

In general, Wheedon-Zygmund loks like something that Aristotle (or other AIs) could formalize with great profit to the community - and possibly only relatively minor human intervention. I'm about to ask Aristotle to formalize Thm. 12.50 (Dirichlet-Jordan) in W-Z - we need that to prove a more general version of Poisson summation than the one in Mathlib.

[Terence Tao]

I guess one could plan to upstream these results directly to Mathlib, rather than funnel them through PNT+, and then use these results once upstreamed (and Mathlib is bumped) to fill in the relevant sorries at PNT+? We could have them live temporarily at PNT+ just to have the sorries filled in faster, but I'm not sure this actually saves much time in the long run.

[Kevin Buzzard]

Is Aristotle writing mathlib-ready code though? Mathlib has infamously high standards for code quality.

[Terence Tao]

Fair enough. In which case it makes sense to formalize these results within PNT+, perhaps starting directly in the Mathlib folder to emphasize the intent to upstream the results once they reach a suitable quality standard of writing.

[Harald Helfgott]

I'm still trying to coax Aristotle into formalizing the proof of Dirichlet-Jordan in W-Z. So far, it has formalized the proof of Fejer's theorem for continuous f, but, for whatever reason, it has not yet proved it for f continuous in an interval, or for f having a jump discontinuity. Let us see.