<p>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 <a href="https://en.wikipedia.org/wiki/Chaitin&#39;s_constant" rel="nofollow noreferrer">Chaitin's Omega</a> and you're clever enough to realize what you've got and type it down. </p>

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

<blockquote>
  <p>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.</p>
</blockquote>

<p>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.</p>

<p><em>(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)</em></p>

CC BY-SA 3.0
2017-03-01T03:52:06.260Z
2017-03-01T03:52:06.260Z
jberryman
<p>You can look at <a href="https://en.wikipedia.org/wiki/Genetic_programming" rel="nofollow noreferrer">genetic programming</a>, and perhaps neural networks, which are quite general algorithms that improve under usage.</p>

<p>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 <a href="http://thatsmathematics.com/blog/archives/102" rel="nofollow noreferrer">randomly generated gibberish sometimes gets accepted</a> for publication, maybe we are not that far away.</p>

CC BY-SA 3.0
2017-02-28T03:48:46.777Z
2017-02-28T03:48:46.777Z
Per Alexandersson
<p>Mind the following program:</p>

<pre><code>n = 0
best = 0
while (true):
  if (hash(n) &gt; best):
     best = hash(n)
  ++n
</code></pre>

<p>If you leave this program running for 10 years, when you come back you'll have a <code>n : N</code> such that <code>hash(n)</code> is really, really big. If someone ever needed a proof of <code>∃ n : ℕ . hash(n) &gt; K</code>, 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. </p>

<p>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? </p>

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

CC BY-SA 3.0
2017-02-25T20:30:39.557Z
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.
MaiaVictor
CC BY-SA 3.0
2017-02-25T20:45:16.860Z
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".
usul
CC BY-SA 3.0
2017-02-25T21:41:47.127Z
@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.
Tayfun Pay
CC BY-SA 3.0
2017-02-26T19:28:57.430Z
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](http://people.idsia.ch/~juergen/optimalsearch.html)). The algorithm essentially "learns" the optimal search algorithm out of all the possible ones. The constant factors involved are, of course, astronomical.
cody
<ds.algorithms><lo.logic><complexity-theory>
Is there an algorithm which gets incrementally "smarter" as it runs?
MaiaVictor
# Is there an algorithm which gets incrementally "smarter" as it runs?

(Asked by: username_0 on 2017-02-25)

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(∅))?

**Tags:** ds.algorithms, lo.logic, complexity-theory

> **Comments:**
> **username_0**: 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.  
> **username_1**: 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".  
> **username_2**: @username_0 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.  
> **username_3**: 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](http://people.idsia.ch/~juergen/optimalsearch.html)). The algorithm essentially "learns" the optimal search algorithm out of all the possible ones. The constant factors involved are, of course, astronomical.  

---

## 2 answers

### Answer by username_4 on 2017-03-01. Score: 3

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](https://en.wikipedia.org/wiki/Chaitin's_constant) 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)*


---

### Answer by username_5 on 2017-02-28. Score: 2

You can look at [genetic programming](https://en.wikipedia.org/wiki/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](http://thatsmathematics.com/blog/archives/102) for publication, maybe we are not that far away.


---

