Well given that it was considered a surprising and highly non-trivial result when it came out less than thirty years ago, I'll say that it's obvious only in the

Well given that it was considered a surprising and highly non-trivial result when it came out less than thirty years ago, I'll say that it's obvious only in the sense that all statements that have been proven are obvious after the fact. And yes, I worded that ambiguously. Let me rephrase, to see if I got it correct: Pick any finite axiomatization. Then there is a concrete f(x) that we can write down in about 200 pages, for which finiteness of the solution set is not decidable. The fact that there are diphantine equations for which finiteness is undecidable is really surprising to start with to me.