All Questions

Generally, number theoretic conjectures which are well-known and easy to explain are either obviously $\Pi^0_1$ or $\Pi^0_2$, which is to say, their truth can be decided by a single membership query ...

Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is ...