Terence Tao on Nostr: Finally managed to formalize in #Lean4 the repaired version of the arguments in ...
Finally managed to formalize in #Lean4 the repaired version of the arguments in Section 2 of my paper. It was more tedious than I expected, with each line of proof taking about an hour to formalize. In the first week of my project, the bottleneck was my own ignorance of the syntax and tools available in Lean; but currently the bottleneck was rather the tools themselves, which are not yet as advanced as the tools one might see in a computer algebra package. For instance, in one line of my paper I state that the inequality
\[ |s_n|^{-1/n} \leq \max_{k'=k,k+1}\] \[(2n)^{\frac{1}{2} \log \frac{n-1}{n-k'-1}} (|s_{k'}|/|s_n|)^{1/(n-k')} \]
can be rearranged as
\[ |s_n|^{1/n} \leq \max_{k'=k,k+1} \]\[ (2n)^{\frac{n-k'}{2k'} \log \frac{n-1}{n-k'-1}} |s_{k'}|^{1/k'},\]
assuming all denominators are non-zero. This is a reasonably quick task on pen and paper, and can also be done fairly readily in any standard computer algebra package (perhaps after treating \(\max\) operators manually). However, while Lean does have very useful automated tools for field identities and linear arithmetic, it does not currently have tools to automatically simplify complex expressions involving exponentials, and instead one has to work step by step with the laws of exponentiation (e.g., \((x^y)^z = x^{yz}\), \( x^z/y^z = (x/y)^z\), etc.) as well as the other operations appearing above. Each such law is provided by Lean, but sequencing them together is time-consuming.
One step that stumped me for a while was a numerical verification \( 2e - 2 \leq 8(e-2) \). This is immediate from a calculator, but to prove it rigorously I ended up having to use the inequality \( e \geq 1 + 1 + \frac{1}{2!} \).
\[ |s_n|^{-1/n} \leq \max_{k'=k,k+1}\] \[(2n)^{\frac{1}{2} \log \frac{n-1}{n-k'-1}} (|s_{k'}|/|s_n|)^{1/(n-k')} \]
can be rearranged as
\[ |s_n|^{1/n} \leq \max_{k'=k,k+1} \]\[ (2n)^{\frac{n-k'}{2k'} \log \frac{n-1}{n-k'-1}} |s_{k'}|^{1/k'},\]
assuming all denominators are non-zero. This is a reasonably quick task on pen and paper, and can also be done fairly readily in any standard computer algebra package (perhaps after treating \(\max\) operators manually). However, while Lean does have very useful automated tools for field identities and linear arithmetic, it does not currently have tools to automatically simplify complex expressions involving exponentials, and instead one has to work step by step with the laws of exponentiation (e.g., \((x^y)^z = x^{yz}\), \( x^z/y^z = (x/y)^z\), etc.) as well as the other operations appearing above. Each such law is provided by Lean, but sequencing them together is time-consuming.
One step that stumped me for a while was a numerical verification \( 2e - 2 \leq 8(e-2) \). This is immediate from a calculator, but to prove it rigorously I ended up having to use the inequality \( e \geq 1 + 1 + \frac{1}{2!} \).