[hackandthink]

My understanding:

There's no algorithm to decide. But for any equation we can be lucky to find a solution or a proof that there's no solution.

But this doesn't prove that there is an equation for which we'll never know if it's solvable or not.

[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.

[layer8]

See https://news.ycombinator.com/item?id=34384838, I think it disproves your last sentence — at least when assuming that all solutions and all proofs of non-existence of a solution are expressible in a shared formal language.