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.

Continue reading →