Royen proof of gaussian correlation inequality

hi all theres been a recent shock of awareness of the Royen proof of gaussian correlation inequality, pop-sci publicized by Wolchover for Quanta, a big milestone… this is a nearly ½-century-open problem![a] Quanta funded by Simons institute is one of the top outlets for scientific/ mathematical writing around today. a real community resource/ treasure!

the Royen proof is not exactly my area so cant write a lot on it but do note that its a key case study in dynamics of scientific peer review, and seems like it has some parallels to the ongoing mochizuki proof analysis.[b] it took over ~1½ year for “community” to begin to grasp the correctness of this proof and Wolchover has a nice historical timeline for how others began to notice/ accept it, a mapping of the spread of awareness. it did not help that Royen was somewhat isolated and did not seem to personally contact any cohorts for peer review. he published openly but it got lost in the noise. it shows how community acceptance is sometimes far from a black/ white binary decision, esp for “big problems”.

is there any way to improve peer review? its definitely a bit of an achilles heel of the scientific process. my feeling is that there is no way to improve it very much except maybe to try to increase transparency somehow. its very similar to the problem of “fake news”. how do you measure quality in content? we live in the vast Information Age but as has long been noted, theres a big difference between Information and Wisdom, and in a way peer review is the major mechanism that is designed to separate/ discriminate the two.

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.

Ramanujan film, the man who knew infinity

hi all. ramanujan is one of the great/ inspiring/ legendary characters out of the pantheon of math heroes and they just released a major hollywood movie on his life starring Dev Patel and Jeremy Irons. its been a few great years lately for geeks of all stripes such as with the facebook movie, google movie, and the Turing movie (just a few that immediately come to mind). am really enjoying this moment in the spotlight or sun. if you are curious about such things, the etymology of geek vs nerd and the relation of “semantic drift” is now documented on dictionary.com, but the short story is that what was once a stigma is now an accolade/ badge of honor.[b15] and lets face it, mathematicians are long close to the stereotypical ultimate geeks. which reminds me of old joke:

Q. how can you tell if a mathematician is extroverted?

A. he looks at your feet while talking to you.

the movie is based on a book by Kanigel now about ~¼ century old (1992).[b14] bought the book as soon as it was available but never did read it! am delighted that the public has rediscovered this great intellectual hero/ prodigy, and some aspects of his story are being played up in the modern age such as the “diversity” angle. we also have a huge mix of indian culture into the US, and indians seem to be overrepresented in the technology field, although have not seen many mention this. india is also a world powerhouse in software outsourcing, although maybe that wave while still moving/ in motion is not as strong after over a decade of very intense rampup. cities such as Bangalore and Hyderabad are miniature foreign Silicon Valleys although ofc the latter is distinctly singular worldwide.

another great ref on Ramanujan is some essays in the amazing book World of Mathematics, 1956.[b13] think may have heard 1st of ramanujan from this book found while browsing the math section of different libraries.

start on logic/ binary division/ prime finding via DFA constructions

hi all. this continues/ advances the idea of analysis of bertrands postulate via a CS/ automated thm proving approach.

was looking for some existing code around the internet just to see what has been done. years ago, built multiplication circuits in SAT in both C (early 1990s) and Perl (2000s). alas, neither code is still available. (can really tell that you are all on the edge of your seat for that, lol)

there are some interesting papers on fast modulus calculation using highly tuned hardware such as FPGAs. this turned up in a google search pointing to DTIC, Defense Technical Information Center (US military!) and without a citable link on the site, in contrast to many other papers there.[a2][a3][a4]

hmmm!

SAT induction revisited wrt Bertrands postulate, collatz vs prime similarity

hi all. was thinking really hard this week and then came up with some cool ideas about prime theorem proving and more advanced stuff. it all led back to an idea thats now over 2yrs old on this blog, “SAT induction”.[a]

there is a “hall of mirrors” type aspect of working on undecidable problems. there are many equivalent ways to formulate the same undecidable problem. its like a sort of core that crosscuts many fields, some unexpected. (lately there is some excitement that it shows up in theoretical physics etc).

however, think that there is a way out of the “going in circles” and SAT induction seems to be it.

consider what a proof of infinite primes would look like using SAT instances. the immediate idea is to use Bertrands postulate, also proved by Erdos in a surprising elementary proof. in SAT one might encode instances of the problem in the form “if there is a prime with n bits, then there is a prime with n+1 bits”. (alternative idea, very similar: “there exists a prime with n bits”.)

then one could lay out these finite instances of the infinite problem, say F_n for each n. this would lead to an array of SAT instances. (over 2 decades ago, built SAT circuits that factor numbers in binary. these circuits are similar.)

now, encode the SAT instances as graphs. and look for graph similarities between G_n and G_n+1. and then one is attempting to build graph G_n in terms of graph G_n-1. this is where the machine learning problem comes in. but for some problems, such as Bertrands postulate encoded, presumably there is not an extremely difficult solution that could be found by machine learning. one finds a systematic relation between G_n and G_n+1 and then one has to show that this also leads to the property that if F_n is satisfiable then so is F_n+1 (based on the graph relation). this reminds me of the concept of “satisfiable/ unsatisfiable core” that is being explored in SAT research, suspect it would be relevant.[c]

this is an almost radically new form of automated theorem proving that is not explored almost anywhere in the literature. and, it doesnt entirely sound like implausible/ inconceivable science fiction. there are decades of results in automated theorem proving and massive effort in the area, many different software algorithms/ packages developed and research programs (see eg wrt this problem [b]). but none come anywhere close to this.