Category Archives: r&d homegrown

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.

Continue reading

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]


Continue reading

$1B EU QM computing initiative + QM theory/ applied highlights Q1 2016

nature_EU_qm➡ 💡 ❗ ⭐ 😮 😀 😎 ❤ 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.

Continue reading

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 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.

Continue reading

number theory news/ highlights: prime bias, Diffie-Hellman, Zhang-Tao, Wiles, Riemann

PrimesResearchers😮 💡 ❗ 😎 😀 ❤ hi all. big news in number theory last few months and years. this is a tribute to a few years of top breakthroughs and exciting developments. the general theme is “primes” but there are a few detours.

in a breakthru/ rare event, a new statistical property of primes was discovered related to frequency of occurrence digits in base-n expansions. it was discovered by Oliver/ Soundararajan and has led to a huge amount of media attention and notice by top scientists. some of it was uncovered with dear-to-my-heart computer empirical/ experimental approaches.[e]

yet its somewhat reminiscent of another similar discovery only ~7yrs ago in 2009 by Luque/ Lacasa.[e6]

big discoveries like this sometimes make one think that maybe we havent even “scratched the surface” of theory of primes. [a2], a long-held/featured link on this site (on main sidebar) points out connections with quantum mechanics by Sautoy, an authority on the Riemann hypothesis (Dyson/ Montgomery 1972).

speaking of Riemann, and apropos/ befitting/ in observation/ reverence of todays date, it was claimed to be proven by a Nigerian recently. and it turns out not surprisingly Nigerian mathematics is not all so different than illustrious Nigerian business ventures advertised on the internet.[g]

Continue reading