Back

Happily, apart from the one bug previously noted, no other errors (other than very small typos) were detected in the paper. I found some mild simplifications to some steps in the proof as a consequence of formalization, but nothing particularly notable. (But this was a rather elementary paper, and I was not really expecting to glean deep mathematical insights from the formalization process.)

The Sapir-Whorf hypothesis https://en.wikipedia.org/wiki/Linguistic_relativity is controversial for natural languages, but for the specific case of proof formalization languages I think the effect is real. The Lean syntax and library of lemmas and tools certainly pushed me to plan ahead and abstract away many small lemmas to a far greater extent than I would ordinarily do; long "stream of consciousness" type arguments, which I tend to favor personally, are possible in Lean, but often not the most efficient way to proceed. I have also started noticing myself mentally converting results I read in regular mathematical literature to a sort of "Lean pseudocode", though this is probably just a version of the "Tetris effect" https://en.wikipedia.org/wiki/Tetris_effect and will likely dissipate now that my project has concluded.

A combination of automated tools, AI tools, and interactions with human Lean experts proved invaluable. GPT greatly sped up the initial learning of syntax, tools such as `exact?`, `apply?`, and Moogle https://moogle-morphlabs.vercel.app/ helped locate key lemmas, and Copilot had an often uncanny ability to autocomplete one or more lines of code at a time. But there was certainly a lot of "folklore" tips and tricks that I had to go to the Lean Zulip to get answers to. 2/3

I found that documenting all the places where I encountered some problem, and recording the solution, was helpful, not just as a text to refer to whenever encountering a similar issue in the future, but also just to organize my thoughts and consolidate my understanding of various subtle aspects of Lean. (This document can be found at https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo ).

While formalization is generally much slower than writing in Mathematical English, I found one aspect in which the formalized writing process was far superior. If, halfway during the writing of a long argument, I found it necessary to tweak some parameter or hypothesis at the very beginning of the argument, the Lean compiler would quickly identify all the other parts of the argument that might need changing, and it was a fairly quick matter to modify the proof to get back to a working state. In contrast, when performing these dozens of small edits in Mathematical English, it is all too common to introduce one or more small errors which tended to be quite tedious to detect and eradicate. In many cases, if sufficiently "smart" tactics were employed, many fewer edits would be required in Lean as compared to Mathematical English; Lean can often propagate changes in hypotheses automatically to the natural changes in conclusions through its advanced ability to fill in "holes".

Would I attempt to formalize more mathematical papers any time soon? Probably not as a solo project; it was significantly more time consuming than expected. But I particularly enjoyed the (unplanned) collaborative aspects, and I could see myself contributing to a larger Lean collaboration in the future. (3/3)

@tao Thanks for this. Your spreadsheet notes are very helpful.

@highergeometer I'm not sure that raw file sizes are that good of a measure, but my LaTeX source for the paper is 37KB uncompressed while the essential files for the project (removing newton.lean and maclaurin.lean) add up to a bit over 110KB, plus some additional tactic files that were contributed. It is not evenly distributed; the last three pages of my argument required about 45KB of Lean to formalize. The size expansion of 3x or so is significantly less than the time expansion of 20x I experienced; a reasonable goal perhaps is to have additional development tools to bring the latter factor down to more closely resemble the former.

@tao Yes, it's certainly not a measure of the formalisation effort, but it measures how close the language/libraries is to the mathematical English vernacular. One might imagine that if mathlib had already had a number of basic results you needed to prove yourself, and the tactic automation a year or two more developed, that the proof could have been even shorter. The inhomogeneity of the paper proof:formal proof ratio certainly reflects this.

The recent blog post at Xena Project about the difference between the Ramsey-theoretic formal proof of Mehta and the core of the Liquid Tensor Project also shows this changing ratio (https://xenaproject.wordpress.com/2023/11/04/formalising-modern-research-mathematics-in-real-time/, the section "5 years, 50 pages, 5 months")

@consensus This part of the argument does not require the fact that $F$ has a representation $F=\sum _p{F}_p$. Abstractly, it is asserting that if one has a bound of the form $F_1(\mathbf{X})=G_1(\mathbf{X})+O({\epsilon }^{2}Y)$ with probability $1-o(1)$ for some functions $F_1,G_1=O(Y)$ and some constant $Y$, then one automatically has $\mathbf{E}{F}_1(\mathbf{X})=\mathbf{E}{G}_1(\mathbf{X})+O({\epsilon }^{2}Y)$, by averaging the errors as you say (but the primes $p$ play no role here, and I have no idea what you mean by $k_p$).

@tao Thanks! Shouldn't we factor the logarithmic weight $\frac{1}{n}$ as $\frac{1}{k_{p}p}$ to connect $\frac{1}{k_{p}p}{F}_p(x,y)$ to the original logarithmically averaged two-point correlation?

@consensus No. The connection to the original two-point correlation was already worked out in Section 2, where it was calculated that (2.4) implies (2.17). To complete the proof, it suffices to show that (2.17) leads to a contradiction; no further discussion of the original two-point correlation is needed.