With a little more work, it should be possible to—almost—solve all of mathematics: to create an oracle which, given a formal system, can tell you whether any given statement can proved within that system
...with a proof of length L or less.
Aside from the issue of the given statement, what can’t be proved?
Problems whose answers are independent of the framework you are using (The continuum hypothesis). [1]
Undecidable problems. [2]
Things which probably can’t be proved:
Things which are false, like 2+2=3. (For a given framework which meets certain requirements, it is not possible to prove that there isn’t a contradiction—within that framework.) [3]
The continuum hypothesis was advanced by Georg Cantor in 1878, and establishing its truth or falsehood is the first of Hilbert’s 23 problems presented in 1900. The answer to this problem is independent of ZFC, so that either the continuum hypothesis or its negation can be added as an axiom to ZFC set theory, with the resulting theory being consistent if and only if ZFC is consistent.
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. The halting problem is an example: it can be proven that there is no algorithm that correctly determines whether arbitrary programs eventually halt when run.
the halting problem is undecidable over Turing machines. It is one of the first cases of decision problems proven to be unsolvable. This proof is significant to practical computing efforts, defining a class of applications which no programming invention can possibly perform perfectly.
Problems whose answers are independent of the framework you are using (The continuum hypothesis). [1]
Undecidable problems. [2]
These are pretty much the same thing. The continuum hypothesis is a case where you have a single formal system in mind ( ZFC ) and have proved that the continuum hypothesis is independent of the axioms.
In the case of the halting problem, you just have a couple of extra quantifiers. For all formal systems that don’t prove a contradiction, there exists a Turing machine, such that whether the Turing machine halts or not can’t be proved from the axioms of the formal system. (Technically, the formal system needs to be R.E., which means that there is a computer program that can tell if an arbitrary string is an axiom. )
...with a proof of length L or less.
Aside from the issue of the given statement, what can’t be proved?
Problems whose answers are independent of the framework you are using (The continuum hypothesis). [1]
Undecidable problems. [2]
Things which probably can’t be proved:
Things which are false, like 2+2=3. (For a given framework which meets certain requirements, it is not possible to prove that there isn’t a contradiction—within that framework.) [3]
Footnotes
[1]
From https://en.wikipedia.org/wiki/Continuum_hypothesis:
[2]
https://en.wikipedia.org/wiki/Undecidable_problem
https://en.wikipedia.org/wiki/Halting_problem:
[3]
https://en.wikipedia.org/wiki/Kurt_G%C3%B6del#Incompleteness_theorem
These are pretty much the same thing. The continuum hypothesis is a case where you have a single formal system in mind ( ZFC ) and have proved that the continuum hypothesis is independent of the axioms.
In the case of the halting problem, you just have a couple of extra quantifiers. For all formal systems that don’t prove a contradiction, there exists a Turing machine, such that whether the Turing machine halts or not can’t be proved from the axioms of the formal system. (Technically, the formal system needs to be R.E., which means that there is a computer program that can tell if an arbitrary string is an axiom. )