Hacker News new | past | comments | ask | show | jobs | submit login

> Yes, we have proofs (which probably can be proven formally!) that there are things which cannot be proven.

That is a very subtly different question than the one I was trying to ask. Or.. well.. I think it is. What I was trying to ask was if there are formally provable theories that cannot be expressed in a way that would let a computer "compute" the proof.

I think that this is not the same as proving that there are unprovable theories.

EDIT: I just noticed my phrasing was off in the original question.. gah, this reminds me of conversations with my mathematician friends IRL where I would always trip over my own sloppy use of human language. What I mean with "computing" is verification, not execution

> What I was trying to ask was if there are formally provable theories that cannot be expressed in a way that would let a computer "compute" the proof.

Do you mean "find the proof" or "verify the proof"? That difference is critical.

Theorem-provers that work to find proofs have made many strides, but as of today humans easily run rings around them. That's not to say it can never be done. Years ago good Go players could trounce machines, and that is no longer true. So: Today, most proofs cannot practically be found by a machine, but they are getting better and there's no fundamental reason computers can't be excellent at it.

Verifying proofs is something a computer is par excellence at. To verify a proof, the proof checker simply needs to verify that each step is valid. No human can compare to the ability of a computer to be picky :-).

In some systems it may not be possible to express a proof of a particular claim in a reasonably short sequence. But that would be a limitation for both humans and computers. In both cases, the answer would be the same: find a way to switch to a "different" system where it's easier to express the proof. In some sense normal math does this; people routinely define new terms, and then build on those definitions so that everything else is simpler.

I really hope machine learning will succeed in producing systems that surpass contemporary mathematicians in not only finding proofs, but also suggesting definitions and theorems to simplify a database of mathematics.

What you're talking about can be formalized via https://en.wikipedia.org/wiki/Arithmetical_hierarchy#The_ari... where your notion of "computable" likely corresponds to some set between (Sigma_1 intersect Pi_1) and (Sigma_1 union Pi_1) depending on some nuance. In any case, you can show by diagonalization that there are statements strictly outside these sets--that is, first order propositions that cannot be verified or refuted by computer.

The question was whether there are statements provable by humans but not computers, which is either trivially impossible or guaranteed, depending on whether you allow the computer to use the same axioms as the people.

It depends on how you interpret it, I interpreted it as asking if there are provable statements that can't be "computed" directly.

Uh... well... can I claim the "sorry, not a mathematician so my reasoning about these matters is quite sloppy, relatively speaking"-defense?

(The responses here have been very nice despite that though, thank you everyone!)

I cannot pretend to truly follow the actual mathematics you linked and summarized (I appreciate the attempt!), but the conclusion in the last sentence answers my intended question. Thank you!

It's a mistake though. Humans can't prove any of those propositions either.

Oh. That's kinda typical, hahaha. I guess this topic can get quite subtly and tricky, even for trained mathematicians?

> That is a very subtly different question than the one I was trying to ask. Or.. well.. I think it is. What I was trying to ask was if there are formally provable theories that cannot be expressed in a way that would let a computer "compute" the proof.

It depends on the logical system + axioms that your formally provable theory is in respect to, and "how soon" you design the computer that verifies the proof. Recall that a proof is a finite sequence of applications of rules of inference on zero or more axioms to derive a new statement that may be regarded as an axiom for applications later in the sequence, so that the last step derives the theorem.

If there are a countable number of rules of inference and a countable number of axioms, and each rule of inference has finite valence (i.e. infer from finitely many formulae-patterns as hypotheses), then yes, there is a way of encoding the rules of inferences and possible axioms of the logical system that a Turing machine (TM) will find a proof of any provable theorem (i.e. verify it), simply by enumeration of axioms in rules of inferences in the positions in a sequence that constitute the proof, while checking whether the axioms legally fit the rules of inference. (It is always possible to check in finite time whether a (finite-length) formula satisfies the pattern it needs to satisfy by a rule of inference).

On the other hand, if there are an uncountable number of rules of inference or an uncountable number of axioms, there may be a computer that cannot verify all the formally provable theories. For example, trivially, if there are an uncountable number of axioms, then the axioms admit no encoding; that is, there is no set of finite strings in a finite alphabet that is able to uniquely label all the axioms. But an axiom is itself a formally provable theorem; its proof is just introducing itself, yet that proof cannot be represented for all the axioms. (dependent on definition of proof; this example may not be so if we accept a zero sequence as a proof; but in general this illustrates the fact that there are simple theorems in some formal systems + uncountable axioms that cannot be computed).

Yet, if we know beforehand the theorem and rules of inferences and axioms used in some proof of it, and the rules of inference all have finite valence, then that proof only invokes finitely many rules of inference on finitely many axioms, such that we can encode a fragment of the logical system + axioms + expressible formulae such that the TM can verify all formally provable theorems in that fragment, including the desired theorem.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact