On: Kurt Gödel and the Mechanization of Mathematics

[xamuel]

1. The original example would be Goedel's own example, namely, the statement (formulated in the language of PA) that PA is consistent, i.e., that PA does not prove 1=0.

Less contrived examples are:

2. Goodstein's Theorem https://en.wikipedia.org/wiki/Goodstein%27s_theorem

3. A theorem stating that every computable strategy is a winning strategy in the hydra game (see https://faculty.baruch.cuny.edu/lkirby/accessible_independen...)

4. The strengthened finite Ramsey theorem, see https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor...

[strbean → xamuel]

Thanks!