A summer of AI-assisted mathematics. Language models propose and referee arguments, and a claim only counts once exact computation and a human read agree. Supervised by Profs. Dimitrov, Paquette and Wehlau.
Take an ordinary number and replace it with a formula in a new variable q that gives the number back when q = 1. For a whole number n the formula is 1 + q + q2 + ... + qn-1. Morier-Genoud and Ovsienko extended this to fractions, using continued fractions, and then to every real number, where the result is an infinite power series in q. The exact arithmetic gets large fast, so most of the work runs on software.
In Example 6.4 of On q-deformed real numbers (Experimental Mathematics, published online 2019), Morier-Genoud and Ovsienko noticed that at −√2 and −√7, the q-deformation of −x cancels against that of x, so the sum is a short finite formula instead of an infinite series. They called it a mystery. This negation question is my part of the group's working paper.
We proved one direction: if that sum is finite for a real quadratic irrational x, then x = ±√d for a positive whole number d that is not a perfect square. The closing step builds on earlier work, Theorem 3.6 of Kogiso, Miyamoto, Ren, Wakui and Yanagawa. The other direction, which d actually give a finite sum, is still open. Claude generated the proof, and we reviewed it and checked it with the process below. It is written out on paper. A Lean 4 file checks the matrix part of the argument and takes the q-side identities as assumptions.
Before the proof, I computed the sum for all 668,745 quadratic irrationals between 1 and 2 with discriminant up to 20,000 and height up to 10, each to its first 512 coefficients in exact integer arithmetic. The first pass labeled 2,061 of them finite.
A classifier trained on those labels then scored a perfect 1.000 balanced accuracy, and a one-split decision tree matched it. The split turned out to be a window artifact: for numbers very close to 1, all the structure sits past the 512th coefficient, so they looked finite. Rechecking the 2,059 suspect rows at 4,096 coefficients left 2 observed finite, √2 and √3, with 304 still undecided. Finite here means finite as far as it was computed, not proved. The only square roots of whole numbers between 1 and 2 are √2 and √3, so the census agrees with the theorem that came later.
A strong model proposes an argument. A second model referees it without seeing how it was produced. The claim then has to survive exact recomputation in qreals, a human read and a check against the literature, and where it matters the proof goes into Lean 4. Claims that fail stay on the record: a finiteness rule that held on six hand-picked cases broke at √19, and three results turned out to be already published.
18 of the 35 claims have Lean 4 files. 12 of those build with no unfinished proof steps. For 5 of the 12 the Lean statement is the full claim, and the other 7 check a narrower or conditional version of it.
qreals is the exact-arithmetic engine behind every check, a Python package on PyPI under the MIT licence. Its answers are tested against published values, identities and independent code paths, as written up in VERIFICATION.md.