Terence Tao on Nostr: Continuing to make progress on my #Lean4 formalization project. Thanks to a tip from ...
Continuing to make progress on my #Lean4 formalization project. Thanks to a tip from a follower here, I was able to complete the proof that the derivative of a polynomial that splits of the reals, also splits over the reals, and as such I have finished the proof of the first non-trivial lemma of my paper (Lemma 2.1). From this I hope to derive the Newton inequalities fairly readily.
As before, it is the minor "obvious" facts that are often the hardest to formalize. Here was a surprisingly challenging proof of the result that if a polynomial \( \sum_{k=0}^n a_k z^{n-k} \) vanishes, then all of the coefficients \(a_0,\dots,a_n\) vanish. (Though I have found on the Zulip chat that many of my proofs can be condensed by a factor of 5x or more by the experts.)
As before, it is the minor "obvious" facts that are often the hardest to formalize. Here was a surprisingly challenging proof of the result that if a polynomial \( \sum_{k=0}^n a_k z^{n-k} \) vanishes, then all of the coefficients \(a_0,\dots,a_n\) vanish. (Though I have found on the Zulip chat that many of my proofs can be condensed by a factor of 5x or more by the experts.)