This paper is a theoretical contribution, not a practical one, similar to Solomonoff Induction. Solomonoff Induction's contribution is essentially "there exists a formal mathematical process that inductive reasoning on evidence corresponds to" which, among other things, pretty much solves epistemological puzzles like the https://en.wikipedia.org/wiki/Raven_paradox from philosophy.

Yeah, the actual performance of Solomonoff Induction is uncomputable, but to me the useful point is that "induction can be done mathematically", and then what we do heuristically in our brains can be thought of as a low-fidelity analog of that. If I'm understanding the page correctly, this is the same idea but for statements based on proofs and logical theorems. Which seems to expand the scope somewhat.

(I'm really excited about this, actually, just as a person who enjoys learning about this stuff from Wikipedia. I feel like I've vaguely thought about how Solomonoff induction would work on statements that are derived from each other (or when combined with type-checking, since type-checking is closely related to theorem-proving), but had no idea how to even ask a precise question much less make anything of it.)

That's interesting I had never heard of Solomonoff Induction until I read your comment. But how important, philosophically, is the existence of such a system, given that the brain already does exist as the "low fidelity analogue".

The limits on what computers can do are related to logical no-go theorems such as Gödel's which are about proofs -- examples of certain knowledge. But once you have accepted the fallibility or "low fidelity" of human reasoning, then all those no-go theorems are no longer relevant in the first place.

Solomonoff induction is useful because without it there's no model of induction with infinite computational resources. "Logical induction" is not useful in the same way because without it we already have such a model: simply prove/disprove the propositions.

And what if the propositions we want to reason about are self-referencing or say something about the system itself in a Godelian way? You need probabilistic reasoning for that to actually work.

Also, "simply prove/disprove the propositions" requires infinite computational resources (we don't know how long the proofs will be or if there are any). Logical induction does not.

I think the purpose of this is to predict proofs ahead of time. Which could be useful in the management of people. As they say in the intro, given a group of specialists, this algorithm can guess, on a daily basis, which of the things they are working on are more likely to be true, and which are more likely to be false. Before the proof is finished.

Its too late, we already risk fortunes (and even lives) trusting in similar methods ;):

https://en.wikipedia.org/wiki/Primality_test#Probabilistic_t...

(Primality is also a logical (analytic) truth and we are satisfied with probabilistic proofs - of course only because the risk is known and controllable.)

That's not quite correct, most prime proving algorithms are non-deterministic in their computation, but they don't necessarily produce false positives (like miller-rabin does), algorithms that only produce false negatives also exist (e.g. ECPP)

Could you elaborate on ECPP false negatives? A properly working ECPP should never give false negatives, e.g. return "prime" for a composite. Since ECPP can give a certificate unlike AKS or APR-CL, the caller could do a relatively quick check of the math.

Some proof methods:

- BPSW. Deterministic, completely correct for all 64-bit values. Purely a compositeness test above, though no counterexamples known. This matches the false-positive idea -- above 64-bit it returns one of "definitely composite" or "probably prime."

- BLS 1975 methods. Relies on partial factoring N-1 and/or N+1 so unless the input is a special form, only practical to ~100 digits. No false results if the partial factoring can be done, and even gives a certificate of primality.

- APR-CL. Deterministic. No false results. Fast and practical up to ~5000 digits (one can debate where the impractical size line is). No certificate.

- AKS. Deterministic. No certificate. No false results. Very slow, so not generally used.

- ECPP. Non-deterministic (randomness is used internally), but no false results. Generates a certificate. Primo is practical up to ~30k digits (depends on your hardware and patience, but 10k digits on modern computers is quite practical). Open source implementations aren't as efficient, but still 1k+ digits is very reasonable. It is possible an implementation might be unable to proceed for various reasons and could return "gave up - no primality decision made" in addition to the choices "definitely composite" or "definitely prime (certificate included)". That's really a limitation of the implementation or the caller's patience.