... and now the proof of the Newton identity

\[ s_{n,k}(x) s_{n,k+2}(x) \leq s_{n,k+1}(x)^2 \]

is formalized! (If one is interested, one can find the proof at https://github.com/teorth/symmetric_project/blob/master/SymmetricProject/newton.lean .)

Copilot showed an uncanny ability to anticipate some of the steps of the proof, perhaps because it "knew" about the standard proof of this identity which I was following somewhat closely. The process is now faster than it was before, though again there was an unexpected speedbump. The standard proof of the Newton identity proceeds by reduction to the case \(k=0, n=2\), which turned out to be straightforward. What was unexpectedly tedious was the verification of the "base case"

\[ s_{0,0}(x) s_{0,2}(x) \leq s_{0,1}(x)^2 \]

which expands after a "routine" unpacking of the definitions to the AM-GM inequality

\[ x_1 x_2 \leq (\frac{x_1+x_2}{2})^2. \]

Somewhat annoyingly, I had to perform this unpacking in fine detail, for instance by tediously verifying that the 1-element subsets of {0,1} were {0} and {1}. Possibly I was missing out on some of Lean's automated tools for this (perhaps by making some trivial little lemmas to feed into Lean's simplifier). In any case, it is done. Next step is to establish Maclaurin's inequality, which I anticipate to be a quick corollary of the Newton identity.