6
$\begingroup$

Mind the following program:

n = 0
best = 0
while (true):
  if (hash(n) > best):
     best = hash(n)
  ++n

If you leave this program running for 10 years, when you come back you'll have a n : N such that hash(n) is really, really big. If someone ever needed a proof of ∃ n : ℕ . hash(n) > K, you could probably sell/provide it to him. In a way, as time passed, that program became incrementally smarter at proving statements of this specific shape. In a way, you could say it was generating knowledge. Obviously, the knowledge generated by that program is very specific and probably useless.

What I want to know is: is there any "generic" way to convert "computing power" in "knowledge"? In other words, is there an algorithm that, as it evolves, becomes incrementally more efficient at proving arbitrary statements?

More formally, given a function A : {0,1}* -> Theorem -> Maybe Proof (which attempts to prove a theorem given some knowledge), and an heuristic H : {0,1}* -> A -> Number (which estimates the efficiency of A at proving arbitrary statements given a specific knowledge), does there exist a P : {0,1}* -> {0,1}* such that ∀ n : ℕ . ∀ m : ℕ . n > m ⇒ H(P^n(∅)) > H(P^m(∅))?

$\endgroup$
  • 1
    $\begingroup$ I think one obvious solution would be a program that brute-forces through every (Theorem, Proof) pair and insert those that type-checks in a lookup-table. That satisfies the requisite because, as time passes, the lookup-table makes the theorem prover more efficient in average at proving arbitrary theorems. Of course that is unsatisfactory because the table would get too big, and that brute-force is way too inefficient. Ideally, such a program would have means of organizing the information it produces, including erasing redundant information. $\endgroup$ – MaiaVictor Feb 25 '17 at 20:30
  • 1
    $\begingroup$ This seems common in optimization such as linear programming or convex function minimization. Often we formalize these by asking for a solution with $\epsilon$ of optimal, and it happens that the way to achieve it is to continue optimizing until the $\epsilon$ tolerance is guaranteed to be reached. But on the other hand, I don't remember anyone pointing out this property of "a solution that gets better over time". $\endgroup$ – usul Feb 25 '17 at 20:45
  • 2
    $\begingroup$ @MaiaVictor You can of course write a program that solves as many instances of SAT as possible for 10 years... Store that in a database... And then create an API that reduces some NP-Complete problem to SAT and then queries your database... So it would be a partial NP Oracle... I bet that the NSA has already done something similar to this where they have solved SAT for some big n, where n is the number of variables; and employ that data base to solve other problems. It is actually not a question of "if" but is a question of "when" something like this will be done. $\endgroup$ – Tayfun Pay Feb 25 '17 at 21:41
  • $\begingroup$ I'm not sure that this is exactly relevant, but there exists (at least in theory) a universally optimal search algorithm called Levin Search. (see e.g. here). The algorithm essentially "learns" the optimal search algorithm out of all the possible ones. The constant factors involved are, of course, astronomical. $\endgroup$ – cody Feb 26 '17 at 19:28
3
$\begingroup$

Let's assume you're working on a toy programming language Flarp late at night and someone whispers in your ear a great deal of its particular Chaitin's Omega and you're clever enough to realize what you've got and type it down.

You could then write a special interpreter function F and a little script that enumerates Flarp programs and runs them as follows (from the wikipedia page):

Given the first n digits of Ω and a k≤n, the algorithm enumerates the domain of F until enough elements of the domain have been found so that the probability they represent is within 2−(k+1) of Ω. After this point, no additional program of length k can be in the domain, because each of these would add 2−k to the measure, which is impossible. Thus the set of strings of length k in the domain is exactly the set of such strings already enumerated.

As your algorithm ran and enumerated more and more programs, the size of programs for which you can solve the halting problem will grow as well, allowing you answer many interesting questions like Goldbach's conjecture, etc.

(obviously this answer is a bit of a joke. I'm also not an expert on any of the above and may have misrepresented things)

$\endgroup$
2
$\begingroup$

You can look at genetic programming, and perhaps neural networks, which are quite general algorithms that improve under usage.

This is quite far from proving statements, but one can imagine that in a far future, one might be able to design a complex program that becomes better at publishing math papers. Given that randomly generated gibberish sometimes gets accepted for publication, maybe we are not that far away.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.