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 effe

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 https://www.jstor.org/stable/2273588