Can Computers Prove Theorems?

A human only can fit only finitely much information in their memory. There are formal systems that no human could fit a description of into their mind.

Also, the way humans reason seems more like something paraconsistent than something truly self-consistent. A person can be convinced of something by some argument, and then convinced the other way.

It is true that the human mind is not an example of [thing which the incompleteness theorems show cannot exist], but this is not surprising.

I agree that you can—I've done that in Coq, though I don't have any experience with Lean.

The advantage of Agda is that everyone else does, too. This provides two things: one, there's a huge set of examples of how people have constructed their proof terms which encode best practices and are themselves designed to be as readable as possible, and two, people also build tooling which helps you to make them.

In Coq, since tactics are primary, you end up with things like Sledgehammer. This is super practical and useful for tactics management, but it's a whole culture that will take you further and further away from understanding how proof terms work.

I do agree that there is something special about the human mind not captured by formal systems (in the "set of axioms or axiom schemas + inference rules" sense). (not so much for empirical external evidence reasons, so much as for like, what I want to call "teleological reasons"? Like, my goals and values are more coherent/less nonsensical assuming that there is something special, so it makes sense (as far as my goals are concerned) for me to assume that there is something special.)

However, I'm not so sure that this something special includes anything Gödel related.

As to whether an "inconsistent system" could "make" consistent formal systems, I'm not entirely sure what you mean. A formal system (in the sense of set of axioms + inference rules) is not an agent, so I'm not sure what you mean about it "making" things. We talk about a formal system prov"ing" something, but perhaps a more clear way of saying what we mean by that, is that the system admits a proof of the thing, or that there is a proof of the thing, for/within that system.

If by a system "making" a system, we just mean that it "proves" (as in, "admits a proof") that some other system is consistent, then I see no reason that a paraconsistent system couldn't show that some other system is consistent.

Have you seen the "Logical Induction" paper by MIRI ?

If a system is inconsistent, then there is a proof that it is inconsistent. Logical induction assigns "probabilities" to different mathematical statements, and it can be shown that these probabilities converge in reasonable ways. If there is a proof of a statement in the system that the logical induction thing is working under, then the "probability" of that statement will converge to 1. Also, this statements that logical induction applies probabilities to include statements about itself.

I think that, if some particular system is self consistent, then, well, for one thing, the probability for the statement "that system is inconsistent" will not go to 1, and furthermore, that there are statements of "the probability for 'that system is inconsistent' will be below c at step t" (for t much larger than the current time step) which will (I think) go to 1.

In that sense, I think logical induction could probably do a good job at concluding that some systems are probably self consistent.

Now, I'm not totally sure of that. I don't 100% understand the logical induction results. But, yeah. Seems relevant to me.

Solomonoff induction can make eventually good predictions about any computable environment, but: While Solomonoff induction is limit computable, it isn’t computable, while logical induction is.

Logical induction can reach conclusions about what a system using a computable approximation to solomonoff induction would conclude. Actually, it can also assign probabilities to what full solomonoff induction would conclude.

Solomonoff induction cannot accurately model a world which contains agents who use solomonoff induction. Logical induction plays nicely with self reference.

Importantly, with some naive ways of attempting to do probabilistic induction on mathematical statements, if you give the system different facts in an adversarial order, you can cause it to alternate between being highly convinced that something is true, and that it is false. Logical induction solves this problem.

I don’t think solomonoff induction can be straightforwardly applied to this task. Solomonoff induction predicts what inputs it will receive, but this isn’t, I think, immediately well suited for assigning credence to mathematical statements.

I’m not sure how a halting oracle could be empirically detected? Well, I guess if one believed that “this is like a halting oracle except only for the first 3^^3 Turing machines” and the like we’re substantially less likely than “this is a halting oracle in general”, which I guess seems reasonable.

Ok, I guess I can see that, sorta.

Not sure what practical tests you have in mind though.

Solomonoff induction is optimal for, given an initial portion of a computable bitstring, predicting the rest of (or the next portion of) the bitstring.

Logical induction (my apologies for referring to “probabilistic induction”; I was speaking unclearly when I did so. What I meant to communicate by that phrase was “if you attempt to do Bayesian updating on math statements in a naive ‘just apply Bayes’ rule’ way”, as an example of something that doesn’t work) on the other hand, will assign probabilities to different statements, which it updates over time, and these different probabilities aren’t for mutually exclusive events, unlike with solomonoff induction.

Now, I don’t mean that if you had an oracle for solomonoff induction, that you couldn’t make a program using that oracle to produce something much more powerful than logical induction.

And I’m also certainly not saying that the algorithm found for logical induction is the fastest one for the problem it solves. If it was (at least, if it was for small amounts of time? Perhaps it could be asymptotically optimal for large amounts of time), I think it would be strong evidence that the human mind is special with respect to estimating the plausibility of mathematical statements! (The algorithm is very slow).

But, I do think that it is quite probably better at that task than straightforward applications of computable approximations of solomonoff induction. (Like computable approximations to solomonoff induction, logical induction also goes through an enumeration of all possible programs and eventually tries each one of them.)

By the way, this thread is getting to the point where I have to click your specific reply in order to get to the reply link; do you want to move this to email or discord or something? Totally fine if you want to keep it here of course, just wanted to offer the option.

Also, I need to read up on the thing you mentioned on randomness conservation. Sounds interesting. Sorry for not having gotten to that yet.

I’m confused by what you mean by “implies the existence of halting oracles”. Do you just mean as abstract objects? (in which case, yes, I completely agree that halting oracles exist as abstract objects. There is a fact of the matter as to whether any particular Turing machine halts, and so there is a function from Turing machines to whether the input Turing machine halts on an empty tape. Similarly for halting oracles for Turing machines which themselves have a lower halting oracle.) Or do you mean that they exist or might exist as physically implemented (err, not sure “physically” is exactly the word I mean. Like, if human souls are the only things in/“in” the universe that can solve the halting problem, I don’t think I’d call that “physically implemented”, but I don’t mean to exclude this option) things?

I’m currently skeptical of the latter, but that is approximately the question we are discussing, so maybe I’m wrong.

Are you saying that, you think it plausible that humans can (in a sense) compress strings in ways that Turing machines cannot, (or that a Turing machine with access to a human / to humans, can compress strings better than a Turing machine can alone), and that, if true, that would be evidence for humans containing/having-access-to halting oracles?

If that is what you mean (and my apologies if I’ve misunderstood you), I do agree that this would be evidence for that, yes (though I’m, of course, less convinced that access to humans as an oracle would allow a TM to compress strings better.).

[fifth letter of toboggan]mail btw: Madaco dot madaco

Edit: have started to read the Leonid Levin paper “randomness conservation inequalities” now. Quite interesting so far.