Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

3K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.6

Public
Terence Tao

Continuing to make progress on my 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 ∑k=0nakzn−k vanishes, then all of the coefficients a0,…,an 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.)

Showing that if a polynomial vanishes then all of its coefficients vanish. The fact that the monomials are given in descending order rather than ascending creates a surprisingly tricky obstacle to formally establishing this fact (basically one needs to encode the fact that reflection k -> n-k is injective on {0,...,n}).
Terence Tao

... and now the proof of the Newton identity

sn,k(x)sn,k+2(x)≤sn,k+1(x)2

is formalized! (If one is interested, one can find the proof at github.com/teorth/symmetric_pr .)

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"

s0,0(x)s0,2(x)≤s0,1(x)2

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

x1x2≤(x1+x22)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.

GitHubsymmetric_project/SymmetricProject/newton.lean at master · teorth/symmetric_projectContribute to teorth/symmetric_project development by creating an account on GitHub.
Oct 17, 2023, 07:08 AM·Public·Web
11boosts·31favorites
Public *
Terence Tao

OK, much of the tedium of proving "obvious" statements is coming down to not knowing the existing tools available to do this. Here is my initial proof of the obvious assertion {n∈N:n<2}={0,1} that involved significant case analysis, followed by a much shorter proof using tools in the mathlib that I realized was available the next day. I can see my Lean proofing style starting to change away from my informal proofing style because of this: one is constantly thinking "what mathlib tools are available to smooth the path forward" when deciding on proof strategies.

My initial proof that {n<2} = {0,1}, based on direct case analysis.
Simplified proof that {n < 2} = {0,1}, based on the mathlib tool that {n < succ(m)} is the set {n < m} with m inserted. (succ is the successor function succ(m)=m+1.)
Public
Terence Tao

And, embarrassingly, it was pointed out to me just now on Zulip that this fact is a total triviality in Lean.

Public
Anatole Dedecker

@tao You shouldn’t be embarrassed! The whole difficulty of using proof assistants is to find clever ways to make the proof obvious/easy for the computer, and it’s always surprising how different it is from what’s obvious/easy for humans. In this case of course it’s "obvious" for both, but for different underlying reasons.

Public
patrickstevens

@anatolededecker @tao There's never anything shameful in being unaware of a fact that can only be determined empirically! There's no possible way one could have come up with the line `by simp` merely by thinking incredibly hard; one of human culture's primary reasons to exist is precisely to solve this kind of meta-problem.

Public
Izzy Killeen

@tao It sounds like a horrible way to do mathematics tbh.

Public
Terence Tao

@ijk What I'm discovering is that this is a tool which can be used very inefficiently, but for which experts can wield in a very elegant, rapid, and/or intuitive fashion. Perhaps what is missing is a more modern user interface (possibly including AI enhancements) that encourage (both overtly and covertly) the "good" formalization practices and dissuade the "bad" or "deprecated" ones.

SearchLive feeds
About