I found https://x.com/gm8xx8/status/1925768687618773079 to be a little more understandable summary of what was actually shown.
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.
I was just thinking about how it's an underrated open problem which pairs of (number of variables, degree) are undecidable for MRDP.
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.
Does this have any practical consequences for cryptography?
impressive formalization effort that bridges deep number theory and formal methods
A mind-blowing consequence of the MRDP theorem is that there is a multi-variate polynomial which fits on a sheet of paper with the property that the set of values of the first variable which appear in integer solutions are exactly the set of prime numbers.
https://en.wikipedia.org/wiki/Formula_for_primes#Formula_bas...