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

then, after one gets some good/ adept practice on “simple problems” like Bertrands postulate, one can look at more advanced/ difficult problems such as eg Collatz or other unsolved conjectures. think this has awesome potential!

then was thinking or near-fantasizing about funding entities that would be willing to work on such a project or contribute funding. there are not a whole lot. there are elements of big data, pure research etc. and my idea is to make it a “big science” project also. a short list:

• Simons foundation
• NSF
• microsoft research
• IBM research
• macarthur foundation
• claymath institute
• Gates foundation

ofc none of these would be interested without preliminary results, and project sponsors with very significant reputation/ credibility behind them. as the old “soulcrushing/ life-whittling” expression goes, dont quit your day job.

from the current pov/ terrain this does not look on the horizon but sometimes science moves quickly in certain ways, eg the google AlphaGo research which also involved Facebook to some degree. however though notice the media and google itself are already somewhat clamoring/ pressuring Deepmind for “monetizable” applications. Google recently announced it wants to sell Boston Dynamics and rumors are partly because its executive management could not describe (“a path to”) “monetizable” products. their losing a contract with the US Military might also have been a big blow. why does all this matter? the uber-capitalist word “monetizable” is a kind of kryptonite to “basic research”.

⭐ ⭐ ⭐

following is some more collatz code that shows a rough empirical similarity with prime analysis. when 1st started looking into collatz, noticed a basic property that deviation in (the average of) sequential constant-size groups of stopping distances were increasing in a characteristic curve. possibly never did post this on this blog although its a fairly simple/ elementary observation.

recently, noticed a somewhat similar property in prime statistics. here is a juxtaposition of these two effects. the red trace is number of factors checked between consecutive primes (for the simple/ naive algorithm that just checks odd factors up to half the number, and quits early if it finds any). the green trace is average stopping distance for 100 sequential iterates. the deviations are slowly increasing for both. one wonders if there is some theory “out there” on “increasing deviations”. anyway its a glaring “non-gaussian” sign and maybe also indicative of fractal structure. for example, as far as self-similarity, changing the constant group sizes for the collatz distances leads to the same “scaled” curve shape. (note, this is two graphs superimposed and the two do not have the same vertical scale, the numeric labels correspond only the red prime trend.)

`spread2.rb`

(4/14) was curious about how the “bin sizes” would affect the prime factor counting. heres a graph of bins that are separated for n={1..7}*4 prime “distances” (ie consecutive primes). the relative comparison turns out to be a bit tricky/ involved; the curves are scaled/ normalized according to final values in the curves, a linear fit, curve averages etc. and shows the curves shift from concave upward to concave downward, and deviation (around the mean) generally decreasing.

`spread3a.rb`

the results are different with the collatz stopping distance bins for sizes {1..7}*500 and has a much stronger self-similarity aspect with apparently much smaller effect on the deviation, although some some slightly detectable narrowing.

`spread4.rb`

[b] automated thm proving for euclid’s “infinity of primes”/ CS theory SE

[c] Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints/ Liffiton, Sakallah