Comment by jerf | Hacker News Reader

Comment by jerf | Hacker News Reader

Parent Full thread

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

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.

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.

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

Whoops, yes, thanks, fixed. One of those things I edited one too many times and didn't catch in the end.

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

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.

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.

It also just follows from X being >= 30.

Reply on news.ycombinator.com