3 ms·

A problem with randomly searching for theorems is that it blows up exponentially, and many of the theorems you would find are probably not useful in their own r

A problem with randomly searching for theorems is that it blows up exponentially, and many of the theorems you would find are probably not useful in their own right. Another problem is that "check the for truth" is undecidable: they are what I think of when you mention "trade CPU cycles for proofs" though if you're just trying to prove random theorems they will be limited.

jerf 3y ago
"many of the theorems you would find are probably not useful in their own right" To give an example, there's an infinite array of "If X is greater than 20, X is greater than 10" theorems. Obviously useless to prove each of them, but enumeration will encounter all of these, as well as a huge number of classes of similar theorems, in the process of getting to anything interesting. You can't just "skip" them either, because they get arbitrarily complicated. I chose a really simple one to drive home the point, and because it's the sort of theorem you'll hit early, but tautologies can be arbitrarily complicated. Trying to create something that identifies them hits halting problems of their own. Rice's Theorem, which can be colloquially summarized as "any interesting property is not computable", will stop you, among other things. ("If X is a prime > 521, X does not have 21 as a factor." "If X is irrational, its fraction expansion does not have a denominator between 15 and 54." "If the absolute value of X is not equal to X, X < 932." "If the fractional component of X is greater than .5, the first digit of the fraction expansion is not 2 or 4." "The sum of two positive numbers is greater than the smallest of the two numbers number minus 273,883,192,823." "Most" theorems are really, really useless.)
- someplaceguy 3y ago
  > "If X is greater than 10, X is greater than 20" theorems I think you meant in the opposite order, i.e.: "If X is greater than 20, then X is greater than 10" :) But otherwise your point is valid.
  - jerf 3y ago
    Whoops, yes, thanks, fixed. One of those things I edited one too many times and didn't catch in the end.
  - Koshkin 3y ago
    > > "If X is greater than 10, X is greater than 20" theorems I think I have seen theorems of that sort. (Can't think of a specific example right now.)
    - someplaceguy 3y ago
      A theorem like that isn't provable (unless you're using some kind of nonstandard arithmetic). You could only prove it if you add something else, e.g. a precondition saying that X = 30.
      - Koshkin 3y ago
        Right, if it can be asserted based on some independent assumptions that a positive X must be at least 30, then from those assumptions and X > 10 it would follow that X > 20.
        carnitine 3y ago
        It also just follows from X being >= 30.
- gosub100 3y ago
  What if you narrowed down one side, like "Find a formula for solving arbitrary polynomial equations"? (I know this has been proven to not exist using human brainpower). but the idea would be: "I'm looking for a func that produces zeros to an input equation, now generate billions of tokens and evaluate them and keep the ones that minimize the search criterion". Couldn't that eventually find a useful result (for actually-solvable search spaces)? I can see how it would fall apart quickly for something like the Riemann Hypothesis, because you're searching not for an equation (well, if you found a counterexample, sure) but for a nebulous classification problem: all solutions to this equation ( this series of tokens from this language that return zero) must lie on (I can't recall if it was literally on, or "around") re(1/2). Once you try to reason with infinite sets (domain/codomain) the logic of a CPU can't help you nearly as much.
  - jerf 3y ago
    Simply generating all possible tokens is already an exponential problem. There really isn't any way around that. Analysis of them for any interesting property becomes super-exponential pretty easily. If you are going to do something more clever than "generate all tokens", then you're no longer talking about the same thing, and the analysis depends on the nature of your "more clever". Although starting with an exponential (or super exponential) process and then trying to "cut it down" to something reasonable is almost always a fool's errand anyhow. Starting yourself out in the position where you are not only behind the eight ball but have essentially already been murdered by it, and then cleverly working yourself back into a position where you've somehow won, is rarely, if ever, a good approach to solving a problem.
Pet_Ant 3y ago
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.
- gosub100 3y ago
  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).
  - Pet_Ant 3y ago
    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?
  - tromp 3y ago
    > To me, it's totally within the realm of a 1-10 billion search space, isn't it? A proof of the theorem is going to be at least a few hundred bits, which is totally out of reach of brute force search. A 10 billion search space only covers 34 bits (less than 5 ASCII symbols) in which you'll struggle to even state the theorem.

jerf 3y ago

"many of the theorems you would find are probably not useful in their own right" To give an example, there's an infinite array of "If X is greater than 20, X is greater than 10" theorems. Obviously useless to prove each of them, but enumeration will encounter all of these, as well as a huge number of classes of similar theorems, in the process of getting to anything interesting. You can't just "skip" them either, because they get arbitrarily complicated. I chose a really simple one to drive home the point, and because it's the sort of theorem you'll hit early, but tautologies can be arbitrarily complicated. Trying to create something that identifies them hits halting problems of their own. Rice's Theorem, which can be colloquially summarized as "any interesting property is not computable", will stop you, among other things. ("If X is a prime > 521, X does not have 21 as a factor." "If X is irrational, its fraction expansion does not have a denominator between 15 and 54." "If the absolute value of X is not equal to X, X < 932." "If the fractional component of X is greater than .5, the first digit of the fraction expansion is not 2 or 4." "The sum of two positive numbers is greater than the smallest of the two numbers number minus 273,883,192,823." "Most" theorems are really, really useless.)

someplaceguy 3y ago
> "If X is greater than 10, X is greater than 20" theorems I think you meant in the opposite order, i.e.: "If X is greater than 20, then X is greater than 10" :) But otherwise your point is valid.
- jerf 3y ago
  Whoops, yes, thanks, fixed. One of those things I edited one too many times and didn't catch in the end.
- Koshkin 3y ago
  > > "If X is greater than 10, X is greater than 20" theorems I think I have seen theorems of that sort. (Can't think of a specific example right now.)
  - someplaceguy 3y ago
    A theorem like that isn't provable (unless you're using some kind of nonstandard arithmetic). You could only prove it if you add something else, e.g. a precondition saying that X = 30.
    - Koshkin 3y ago
      Right, if it can be asserted based on some independent assumptions that a positive X must be at least 30, then from those assumptions and X > 10 it would follow that X > 20.
      - carnitine 3y ago
        It also just follows from X being >= 30.
gosub100 3y ago
What if you narrowed down one side, like "Find a formula for solving arbitrary polynomial equations"? (I know this has been proven to not exist using human brainpower). but the idea would be: "I'm looking for a func that produces zeros to an input equation, now generate billions of tokens and evaluate them and keep the ones that minimize the search criterion". Couldn't that eventually find a useful result (for actually-solvable search spaces)? I can see how it would fall apart quickly for something like the Riemann Hypothesis, because you're searching not for an equation (well, if you found a counterexample, sure) but for a nebulous classification problem: all solutions to this equation ( this series of tokens from this language that return zero) must lie on (I can't recall if it was literally on, or "around") re(1/2). Once you try to reason with infinite sets (domain/codomain) the logic of a CPU can't help you nearly as much.
- jerf 3y ago
  Simply generating all possible tokens is already an exponential problem. There really isn't any way around that. Analysis of them for any interesting property becomes super-exponential pretty easily. If you are going to do something more clever than "generate all tokens", then you're no longer talking about the same thing, and the analysis depends on the nature of your "more clever". Although starting with an exponential (or super exponential) process and then trying to "cut it down" to something reasonable is almost always a fool's errand anyhow. Starting yourself out in the position where you are not only behind the eight ball but have essentially already been murdered by it, and then cleverly working yourself back into a position where you've somehow won, is rarely, if ever, a good approach to solving a problem.

Pet_Ant 3y ago

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.

gosub100 3y ago
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).
- Pet_Ant 3y ago
  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?
- tromp 3y ago
  > To me, it's totally within the realm of a 1-10 billion search space, isn't it? A proof of the theorem is going to be at least a few hundred bits, which is totally out of reach of brute force search. A 10 billion search space only covers 34 bits (less than 5 ASCII symbols) in which you'll struggle to even state the theorem.