4 ms·
A Formal Proof of Complexity Bounds on Diophantine Equations
- badmonster 1y agoimpressive formalization effort that bridges deep number theory and formal methods
- deleted 1y ago[deleted]
- btilly 1y agoI found https://x.com/gm8xx8/status/1925768687618773079 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 1y agoThat 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.
- kevinventullo 1y agoA 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_based_on_a_system_of_Diophantine_equations https://en.wikipedia.org/wiki/Formula_for_primes#Formula_bas...
- sega_sai 1y agoNon-negative integer solutions
- colinhb 1y ago> is a polynomial inequality in 26 variables, and the set of prime numbers is identical to the set of positive values taken on by the left-hand side as the variables a, b, …, z range over the nonnegative integers. I hadn’t heard of this result, and my exposure to Diophantine equations is limited to precisely one seminar from undergrad, but this feels like taking von Neumann’s famous quip to its most fantastical extreme: > With four parameters I can fit an elephant, and with five I can make him wiggle his trunk.
- marcodavid 1y agoAn even crazier consequence was pointed out by J.P. Jones in 1982. He explained: "Via Gödel numbering, the theorems of an axiomatizable theory T become in effect an recursively enumerable set. The search for proofs becomes the search for solutions of a Diophantine equation. [...] "Theorem. For any axiomatizable theory T and any proposition P, if P has a proof in T, then P has another proof consisting of 100 additions and multiplications of integers." See https://www.jstor.org/stable/2273588 https://www.jstor.org/stable/2273588
- UltraSane 1y agoWhy 100?
- nine_k 1y agoDoes this have any practical consequences for cryptography?
- ogogmad 1y agoLikely not.
- MJGrzymek 1y agoI 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.