Randomly searching for theorems is like using monkeys with typewriters to search for a lost work of Shakespeare. Sure, you _might_ find it, but you'd never know amongst the noise. Well, it wouldn't be like monkeys with typewriters, more like monkeys with word processors and grammar check because the results will type check... but there is no way to screen out what is interesting.
I agree with monkeys+typewriters, but look at how compact the quadratic formula is. It's not a work of shakespeare. it's maybe 12 to 20 "tokens" , using a loose definition of a token. To me, it's totally within the realm of a 1-10 billion search space, isn't it?
I'm just thinking aloud, but suppose a random-math-syntax shuffler eventually produced the quadratic formula, how would you even check it? You would have to input many permutations of quadratic equation inputs and check them against the randomly-produced one. You'd quickly hit imaginary numbers, which could (falsely) signal that the QF is invalid.
Compare that to monkey-typing fizzbuzz. That seemingly could be done in a few billion iterations, no? (assume you could exclude monkeys from typing syntax errors, and only produce valid C++/java whatever).
IDK, I'm just mesmerized by the fact that the QF is so compact, yet there isn't an easily-discoverable way to derive it by brute force. (and I'm deliberately excluding AI because of how tiring the questions of the form "why can't AI do _____" are. I don't care that much about AI).
> It's not a work of shakespeare. it's maybe 12 to 20 "tokens" , using a loose definition of a token. To me, it's totally within the realm of a 1-10 billion search space, isn't it?
Even 12 tokens with only 10 different token values gives you 10¹² different candidate ‘proofs’. That already is a thousand times 10 billion.
In reality, there easily are 100 possible token values (lower and upper case alphabet, punctuation, Greek lower and upper case, dozens of symbols, a bit of Hebrew, etc), taking that number to 10²⁴.
Also, I think even just express the two solutions to ax²+bx+c=0 without any hint of a proof in twelve tokens is an insurmountable challenge.
The Pythagorean theorem is even more compact, and even more impactful. But the low hanging fruit has been already picked for centuries and how would you detect a meaningful formula if you were give a 10GB text file of various ones?
