[moefh]

From my understanding, while that's is technically true, given a consistent axiomatic system (like ZFC[1], the foundation of mathematics we use) there exists a diophantine equation that can't be proven to have no solutions in that system (even though it has no solutions). This mathoverflow answer[2] gives the equation and a link to the paper that shows how to calculate the constants (the numbers are huge!).

What that means in practice is that although what you wrote is true, for some diophantine equations we'd have to come up with new axioms to be able to write a proof of the inexistence of its solutions. But then, how can we be sure that the the new axioms are consistent?

[1] I'm assuming ZFC is consistent; if it's not then it can prove anything, including the existence of solutions for any equations at all

[2] https://mathoverflow.net/a/81986

[hackandthink]

Thanks.

I'm somewhat lost, but it seems to work Gödel like.

The statement is true (equation has no solution) but we can't prove it.