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

@tao Dear Professor Tao, Thank you! Sorry for writing here, but I would like to clarify the steps
"We can thus take expectations and conclude that..."
and "...and hence by (27) we have...", just above Equation (44) in the logarithmically averaged Chowla paper.

Should we sum over
$k_1,...,k_P$
in the representation
$$\frac{1}{k_1{p}_1}{F}_{p_1}(x,y)+...+\frac{1}{k_P{p}_P}{F}_{p_P}(x,y)$$
$$=\frac{1}{P_H}\sum _{y^{\prime }\in Z/P_{H}Z}\frac{1}{k_1{p}_1}{F}_{p_1}(x,y^{\prime })+...+\frac{1}{k_P{p}_P}{F}_{p_P}(x,y^{\prime })$$
$$+\frac{1}{k_1{p}_1}{E}_{p_1}(x,y)+...+\frac{1}{k_P{p}_P}{E}_{p_P}(x,y),$$

where
$E_{p_1}(x,y),...,E_{p_P}(x,y)$
are the errors?

Is $E_{p_1}(x,y)+...+E_{p_P}(x,y)=O({ϵ}^2\frac{H}{\log H})$
sufficient?

@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$).

@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.