While enjoying the reading of Nagel's book concerning Gödel's work, I asked myself various questions related to meta-mathematics. One of them is as follows:
Are there examples of theorems which can be seen as proved in the following manner?
- no "direct" or "explicit" proof is known;
- it can be proved that a proof p for this theorem should necessarily exist (it can't be that the proof p doesn't exist).
Of course the first requirement implies that the proof p by itself isn't known. I would be happy to have some examples in arithmetic if possible.