A Formal Proof of Complexity Bounds on Diophantine Equations
arxiv.org
arxiv.org
https://en.wikipedia.org/wiki/Formula_for_primes#Formula_bas...
I hadn’t heard of this result, and my exposure to Diophantine equations is limited to precisely one seminar from undergrad, but this feels like taking von Neumann’s famous quip to its most fantastical extreme:
> With four parameters I can fit an elephant, and with five I can make him wiggle his trunk.
"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."
Any Diophantine equation can be reduced to one of at most 11 variables and degree at most around 10^63. No algorithm can decide solvability in rational numbers for this class of Diophantine equations.
Correct me if I'm wrong but I think it's guaranteed to have a finite answer, as a list of the minimal undecidable pairs. You can even throw in maximum absolute value of coefficients, though if you limit all three things that's decidable by being finite.