A famous corollary of [Matiyasevich's theorem](https://en.wikipedia.org/wiki/Diophantine_set#Matiyasevich%27s_theorem) is that there exists a Diophantine equation such that it is undecidable (under some recursively axiomatizable theory $T$, such as ZFC) whether that equation has any natural-number solutions. I will somewhat sloppily describe such a Diophantine equation as "undecidable" (with respect to $T$) for brevity.


I've never actually seen an explicit example of an undecidable Diophantine equation. The closest that I've seen is in [this answer](https://mathoverflow.net/a/81986/95043) to another Math Overflow question, which provides an example that's *almost* explicit, but contains one unspecified parameter $K$, whose value depends on the recursively axiomizable theory $T$. However, that answer claims that $K$ can be effectively computed from the axioms of $T$.


A. Are there any simpler explicit Diophantine equations that are known to be undecidable with respect to some common axiomatic system (ideally ZFC, or else ZF or ZFC + CH or something)?


B. For, say, ZFC (or a similar theory, as described in question A), which of the following mutually exclusive statements best captures how well we can actually calculate the value of $K$?


1. An explicit numerical value of $K$ has been reported in the literature.
2. We know how to calculate a valid choice of $K$ and could actually do it in the real world if we really wanted to, but doing so would be too tedious for anyone to have actually bothered to do it so far.
3. We know how to calculate a valid choice of $K$ in principle, but doing so would be impossible in practice - e.g. it would require many, many years of labor, or more computational resources than are currently available with existing supercomputers.
4. We know how to calculate a valid choice of $K$, but it isn't clear whether doing so would be feasible in practice (so it isn't clear whether case #2 or #3 above is correct).
5. We know that $K$ can be effectively computed from the axioms of $T$, but we don't know how to actually do so, so we cannot find a valid choice of parameter $K$ with our current mathematical knowledge.



How constructive is Matiyasevich's theorem?
Turning the proof that there exists a Diophantine equation encoding eg the consistency of $\mathrm{ZFC}$ into a program that actually computes the polynomial would be a bit tedious, but there should not be any significant obstacles. Whether running said program would actually yield an answer, some kind of overflow error, or whether we'd simply get too bored waiting for it to do anything at all is less clear to me.


What I am certain of is that if we do get an answer, it would be sufficiently monstrous that we couldn't gain any insight from it. (And I assume that people generally agreeing with me is the reason why people don't really try it out.)


Getting a "small" undecidable Diophantine equation will require much more work. At any stage of the encodings, one should look for ways to be more efficient.


To better understand the boundary between decidable and undecidable Diophantine equations, it is probably more promising to look at properties of the polynomials that allow for decision procedures vs those properties polynomials obtained from the Turing machine translations have.


