math celebration 2016: pythagorean triples empirical attack conquest

actual U Texas Stampede supercomputer where proof was run [a2]

➡ 💡 ❗ ⭐ 😎 😀 hi all. RJLipton recently covered the amazing/ brilliant breakthrough of solving the pythagorean triples problem by empirical work namely a reduction to SAT and analysis by a supercomputer by Heule, Kullmann, Marek and its a nice pivotal trigger/ tipping point for my own writeup along with related stuff.[a] (have been waiting for opportune time to write this up since may.) proofs like these are a complex or “complicated relationship” for mathematicians (aka facebook-speak), a love-hate affair. (did the extraordinary/ breakthrough/ revolutionary/ paradigm-shifting 4-color computer proof ever win any awards? and how much despair/ handwringing and further effort has there been over it over the decades?)

the breakthrough is celebrated but mathematicians would like to see shorter proofs that are human-comprehensible, so there are mixed/ ambivalent feelings about it within the community. have written on this topic quite at length in this blog even since its beginnings, and this latest breakthrough is delightfully affirmationally crosscutting across many of this blogs categories, and think this is the tip of the iceberg of 21st century mathematics in a way not yet fully recognized. its a dramatic, vivid realization/ materialization of an idea suggested a few years ago here called “SAT induction.” think that these types of proofs will lead to new theory that is indeed human comprehensible but some of the isolated theorems will be claimed first by computer analysis before the more thorough theory catches up to integrate them.

my thinking is that there is some basic theory waiting to be uncovered to explain how infinite search problems, ie equivalent to the halting problem, are sometimes reduced to finite problems. some of this is referred to in hilberts old concept of “finitistic” mathematics. (maybe this was never proposed, but it has long seemed quite natural to me to refer to Hilberts finitism in terms of Turings algorithmic decidability and terminating computations.)

what is this general theory of finding the finitistic “core” of infinite problems? what would/ does a general framework look like? how can it be combined with AI? the glimmers of this are now seen in the pythagorean triple problem in a microcosm, waiting to be tied together & connected by some enterprising/ brilliant geniuses/ visionaries. think some of the answer can be found via “reverse engineering” established/ somewhat-toy-like problems, eg say Bertrands postulate as written about here. in another recent heralded breakthrough there seems somewhat vaguely related work in ramsey theory that is analyzing/ connecting the “finite-infinite divide”.[b18]

there is some nice new recent empirical work eg by Aaronson on the busy beaver problem.[b1][b2] theres some new attention to the LMFDB L-functions/ modular forms database which epitomizes some of the new empirical style.[b3][b4] theres continual dialog about empirical approaches esp in CS.[b5][b8][b9][b10] alas a leader in the field Borwein died at 65.[b11]

have been waiting to write on Mochizuki for years and have collected various links, there are a few refs to him in the blog.[c] it looks like the math community has not dismissed his proof so far and is continuing to engage with it. its a great study in the complementary properties of “old-school” human-focused/ virtuoso/ committee work versus computer or empirical proofs. these two styles are crosspollinating in remarkable ways in our era. math has entered an era of unprecedented complexity.

there are many neat profiles in the media of mathematicians for those who are attentive, have collected many great/ fun links on that on some of my favorites.[d] notably Simons agreed to be interviewed.[d4] numberphile is turning into a one of the top web resources for “popsci” mathematics curiosity/ inquiry, highly recommend it, really great for inquisitive/ precocious kids. (they just did a new segment on Collatz.) other highlights: NFL player Urschel[d8][d9][d10], Chaitin[d11], Conway[d7], Grothendieck[d1][d2], Gardner[d15], erdos.[3]

amid the noise/ lament of many students not engaging with math & achieving basic math literacy, there are scattered encouraging stories about the next generation of students learning math.[f]

now seems as good a time as any to include my cool list of favorite essays written by mathematicians, aka “the joy of mathematics,” there is very much great writing in this vein.[g]

2 thoughts on “math celebration 2016: pythagorean triples empirical attack conquest”

1. gentzen

Why do you want to blog on Mochizuki? Is his proof really the only proof of a famous problem that other mathematicians have issues verifying? Or is it just the only proof where mathematicians point to the impenetrable nature of the writting, without also hinting that the proof itself is probably flawed? If a mathematician of lesser fame would present an impenetrable proof of a famous problem, his proof would just get rejected based on the fact that missing clarity is a sure sign of obvious or hidden flaws in the proof itself.

Maybe one should separate the validation of his inter-universal Teichmüller theory from his proof of the ABC conjecture. Then it makes sense again that other mathematicians should try to validate his work. However, this sort of validation should check whether his theory is useful and helps to generate new mathematical answers, insights, and questions. It should not try to check whether the proof of the ABC conjecture itself is correct or not. And it should not mix up the usefulness of the theory with the correctness of the given proof. A one hit wonder still doesn’t make a great band. And some good bands never scored a number one hit, and still delivered great concerts.

1. vznvzn Post author

think you have all valid points. the Mochizuki proof attempt is notable for its vast span/ complexity, the reputation of its author, and it highlights the sociological aspects of mathematics. there are very few other efforts in math history that have triggered as much collaborative work. it shows that even great mathematicians can get caught up in “crank-like efforts”. another case study on this blog, grothendieck. its a recurring theme on the blog that sometimes the line between genius and cranks can be razor )( thin etc… also, it surely ties in with new efforts to make human proofs more amenable to computer verification also referenced a lot on this blog. etc