Embed Notice

Finally completed the #Lean4 formalization of my Maclaurin-type inequality paper at https://github.com/teorth/symmetric_project . Specifically, if \(s_k\) denotes the \(k^{th}\) symmetric mean of \(n\) real numbers, the inequality
\[ |s_l|^{1/l} \leq C \max ( (l/k)^{1/2} |s_k|^{1/k} \] \[, (l/(k+1))^{1/2} |s_{k+1}|^{1/(k+1)})\]
is established for \( 1 \leq k < l \leq n\). In fact as a byproduct of the formalization I now get the explicit value \(C = 160 e^7\) for the constant \(C\).

Was surprisingly satisfied to get the blue "No goals" message in the Lean infoview.

In the end it took perhaps a hundred hours of effort, spread out over a month. It was about 20x slower to formalize this paper than it was to write it in LaTeX. Initially this was due to my own inexperience with Lean, though near the end I was hitting the limitations of existing Lean tools, as well as the speed of the Lean compiler (though this was in part due some inefficiencies in my coding). However, Lean is a living language still in development, and several helpful people provided me during this project with upgraded Lean tactics (such as an improved `positivity` tactic that could handle finite sums and products, a `rify` tactic to easily convert natural number inequalities to real number ones, and a `rw_ineq` tactic to implement the rewriting of inequalities I had noted was previously missing). These definitely helped expedite the formalization process, particularly in the last week or so. 1/3