A Formal Proof of Complexity Bounds on Diophantine Equations

64 badmonster 7 5/23/2025, 8:09:01 PM arxiv.org ↗

Comments (7)

kevinventullo · 6h ago
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...

sega_sai · 3h ago
Non-negative integer solutions
btilly · 6h ago
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.

throwaway81523 · 4h ago
That sounds like the coefficients might have to be arbitrarily large. Otherwise all DE's could reduce to a finite set of them, impossible via the MRDP theorem. So it's not so easy to call that bounded complexity.
nine_k · 6h ago
Does this have any practical consequences for cryptography?
ogogmad · 3h ago
Likely not.
badmonster · 9h ago
impressive formalization effort that bridges deep number theory and formal methods