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.
➡ 💡 ❗ ⭐ 😮 😀 😎 ❤ hi all, more signs that physics is in a golden age esp in the area of quantum computing and quantum mechanics. EU just announced a $1B initiative to fund quantum computing. this combines with two other existing/ similar projects to analyze the brain and advance graphene technology/ understanding.[a]
the Manifesto[a1] is a sign that we are in dramatic times. you will not much hear scientists ever use the word Manifesto in their entire lifetimes. (marx was a rare exception.) another word that you will rarely hear scientists use is “revolution” but they are calling quantum computing the 2nd quantum revolution. as the chinese say, may you live in interesting times.
the announcement is utterly buried in a bureacratic document[a3] under the section “What is the financial impact of the Cloud Initiative? Where will the money come from and how will it be invested?” but Nature blared it anyway.[a2] apparently those bureacrats are a little gun shy after criticism of the $1B brain initiative as too ambitious or infeasible etc.
these are other big 2015 Q1 developments/ highlights. as usual its hard to keep up with lightning fast advances in this field. even the canadian prime minister is talking about QM these days.[b1][b2] DWave seems to be further confounding its critics with real, measurable performance.[b9][b4] somewhat similar to the EU announcement, chinas Alibaba announced a major QM research initative.[b8] they are intending to start out with encryption applications and hundreds of engineers, working toward QM computing technology.
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 Fn 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 Gn and Gn+1. and then one is attempting to build graph Gn in terms of graph Gn-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 Gn and Gn+1 and then one has to show that this also leads to the property that if Fn is satisfiable then so is Fn+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.
(hi all, my favorite “haunts” in cyberspace lately seem not so busy or as engaging as in past, not sure why that is, so out of sheer lack of alternatives am going through my big link piles/ archives and finally writing up some of my big topics saved over years.)
this is a very big/ deep/ mysterious topic that have been researching and musing on for decades, almost since a teenager, starting with Hofstadters award winning/ near-legendary musings.[a5][a6] the topic also unifies many different threads/ post on this blog. (the delightful comic comes from a google image search result on the term “undecidability”… (doncha just luv AI?! which maybe even could show signs of a (great!?!) sense of humor at times?)
its one of those crosscutting areas where it can seem like very many people are inquiring into it, and almost nobody is, all at the same time. undecidability seems to be the extraordinary mathematical equivalent/ model of terra incognita aka middle age maps that stated at the edges—literally thought to be the same as the edges of the earth or even existence—“here there be dragons”.
aka (mixed metaphor overload alert…) the lynchpin. the 3rd rail (of math/ computer science). haunted house/ mansion. the bermuda triangle. UFO. (boogeyman? monster? under the bed?) or how about some great physics analogies? dark matter/ energy? black hole(s)? etc!
one might say this is a major phenomenon of the massive iceberg, where 90% (or more!) is unseen, or the elephant, in the aphorism about the blind men and the elephant. its a very big elephant in this case! that may even be the understatement of the year! which reminds me, as an old anecdote went in my high school calculus book (Finney?), talking about the self-referential derivative of ex as ex, quoting an old joke/ legend/ folklore about what the indian guru said when asked about what held the earth, and said “an elephant”, and then asked “whats below that”, replied, “its elephants all the way down!”
over the many years, have discovered there is a strong crosscutting connection between these many seemingly disparate areas of computer science in math. they are basically all united by the phenomenon of turing completeness, or the flip (dark) side, (the sheer difficulty of) undecidability. maybe in some ways have some better picture of this than others, but even my own picture is quite fragmented and cloudy at times. ie just another blind mans ramblings. (“in the kingdom of the blind, the one-eyed man is king”?)
💡 ❗ ⭐ 😎 ❤ 😀 hi all, this post spent a long time in the works/ “drawing board” building up & now finally decided to “clean house” after it all finally seemed to reach “critical mass” at least in my bookmark pile. it is difficult to time it. empirical CS/ math has been a big topic in the past on this blog.[a15][a16] this can be a controversial area for multiple reasons/ “standard objections”. there are occasional large breakthrus in this area. however, they are not widely known/ heralded and sometimes even quickly forgotten. one might imagine the momentum steadily building in this area but it seems to be very uneven in progress/ attention. over the last few years here are a few key experimental breakthrus reported but not widely appreciated:
- decrease of the gap in the Zhang twin primes proof. some of this work was done with experimental/ computer searches that found smaller gaps which were then verified/ proven mathematically. its as if numerical evidence gives theoreticians confidence to find/ nail down abstract proofs (instead of hunting for something that might not exist).
- the big-award-winning Kadison Singer proof by Spielman et al.; was aware of this proof but was not even aware myself of the empirical component until the recent writeup by Klarreich for the Simons Quanta magazine.[b] after this account, one wonders if the proof would even have been found/ possible without computer experiments! she writes: (this reminds me of binet’s formula for fibonacci numbers!)
Spielman, Marcus and Srivastava suspected that the answer was yes, and their intuition did not just stem from their previous work on network sparsification. They also ran millions of simulations without finding any counterexamples. “A lot of our stuff was led by experimentation,” Marcus said. “Twenty years ago, the three of us sitting in the same room would not have solved this problem.”
The simulations convinced them that they were on the right track, even as the problem raised one stumbling block after another. […]
A network’s electrical properties are governed by a special equation called the network’s “characteristic polynomial.” As the trio performed computer experiments on these polynomials, they found that the equations seemed to have hidden structure: Their solutions were always real numbers (as opposed to complex numbers), and, surprisingly, adding these polynomials together always seemed to result in a new polynomial with that same property. “These polynomials were doing more than we gave them credit for,” Marcus said. “We used them as a way of transferring knowledge, but really the polynomials seemed to be containing knowledge themselves.”