A Formal Proof of Complexity Bounds on 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...

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

  • undefined

  • Does this have any practical consequences for cryptography?

  • impressive formalization effort that bridges deep number theory and formal methods