ℤ is Diophantine in ℚ: Glazer (Astra, Claude) and Burungale claim Mazur’s conjecture fails

Your AI and this story

Key facts

• The claim: there is a polynomial P with integer coefficients such that q ∈ ℚ is an integer iff P(q, w) = 0 for some rational tuple w. With Matiyasevich’s theorem this makes every recursively enumerable subset of ℚʳ Diophantine and gives Hilbert’s tenth problem over ℚ again, now through a definition of ℤ
• Why it is surprising: Mazur (1992, 1995) conjectured that the real closure of the rational points of any variety over ℚ has finitely many connected components, which would rule out a Diophantine definition of ℤ in ℚ. OpenAI’s 6 Oct preprint had avoided that route (see OpenAI claims Hilbert’s tenth problem over ℚ is undecidable)
• Glazer’s post (5 Nov, verbatim): ‘hello there ℤ is Diophantine in ℚ, thanx to my close friends Astra and Claude. The polynomial characterizing ℤ isn’t quite Tweet-sized; it has m=292,890,231,905 variables, is of degree d < 2^^7, and all its coefficients have absolute value < 2^^8.’ About 396k views, 2.5k likes (fxtwitter, 13 Nov)
• Repository provenance (README): ‘The November manuscript was produced by Elliot Glazer with Astra 6, Sol 6.1, and Opus 5.5, with auditing from Fable 5.1 and 5.2.’ It also preserves an 11 Oct conditional manuscript ‘produced by Sohail Farhangi with ChatGPT 6’, and credits ‘collective agentic notes’ from Stefan Baranczuk, Jose Brox, Gabe Conant, Sohail Farhangi, James Freitag, Elliot Glazer, Jennifer Park and Caroline Terry
• Shrinking polynomial (README): original 292,890,231,905 variables; Version 4, 4,973 variables of degree 4; Version 14 (9 Nov), 314 variables with every coefficient in decimal; Version 15, a quartic family in 222 variables with 2,277 monomials; Version 16 dated 11 Nov. The threshold N0 of the 222-variable family ‘remains ineffective’
• Review: Manvir Jaswal ran the 5 Nov manuscript through his Claude research system (GitHub issue #2, 6 Nov) and listed nine points, ‘none of them should affect the results’; on rechecking Version 10 he found a missing step in a new Kato (1999) Euler-system argument, which Glazer accepted (‘You are right … Our earlier review checked several hypotheses but missed this connecting argument’) and repaired in Version 11
• Verification status (README, verbatim): ‘The Lean formalization is incomplete. The accepted snapshot contains 48 helper modules; the main bounded-polynomial declaration still contains sorry. AI review and successful finite checks do not constitute independent human peer review or a completed formal proof.’ Contributors opened about 20 Lean target issues on 12–13 Nov
• Burungale (arXiv 2611.16130, submitted 12 Nov): ‘there exist an integer n ≥ 1 and a polynomial P ∈ ℤ[T, W1, …, Wn] of total degree at most four such that q ∈ ℚ is an integer if and only if P(q, w) = 0 for some w ∈ ℚⁿ. Consequently … Mazur’s conjecture on the topology of rational points fails.’ Uses quadratic twists of the congruent-number curve (Tian–Yuan–Zhang criterion in Smith’s formulation) and a height bound through quaternionic abelian surfaces; it does not use OpenAI’s 2-converse or 2-adic Fontaine–Mazur results