impressive formalization effort that bridges deep number theory and formal methods

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.

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

Does this have any practical consequences for cryptography?