marcodavid

An even crazier consequence was pointed out by J.P. Jones in 1982. He explained:

"Via Gödel numbering, the theorems of an axiomatizable theory T become in effect an recursively enumerable set. The search for proofs becomes the search for solutions of a Diophantine equation. [...]

"Theorem. For any axiomatizable theory T and any proposition P, if P has a proof in T, then P has another proof consisting of 100 additions and multiplications of integers."

See https://www.jstor.org/stable/2273588