[HN Gopher] A Formal Proof of Complexity Bounds on Diophantine E...
       ___________________________________________________________________
        
       A Formal Proof of Complexity Bounds on Diophantine Equations
        
       Author : badmonster
       Score  : 89 points
       Date   : 2025-05-23 20:09 UTC (1 days ago)
        
 (HTM) web link (arxiv.org)
 (TXT) w3m dump (arxiv.org)
        
       | badmonster wrote:
       | impressive formalization effort that bridges deep number theory
       | and formal methods
        
       | btilly wrote:
       | 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 wrote:
         | 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.
        
       | kevinventullo wrote:
       | 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 wrote:
         | _Non-negative_ integer solutions
        
         | colinhb wrote:
         | > 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 wrote:
         | An even crazier consequence was pointed out by J.P. Jones in
         | 1982. He explained:
         | 
         | "Via Godel 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
        
       | nine_k wrote:
       | Does this have any practical consequences for cryptography?
        
         | ogogmad wrote:
         | Likely not.
        
       | MJGrzymek wrote:
       | 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.
        
       ___________________________________________________________________
       (page generated 2025-05-24 23:02 UTC)