ChatGPT-assisted proof topples the 30-year-old HRT conjecture
Another classic open problem has fallen to an AI-assisted counterexample — this time in harmonic analysis, and with a proof that was, by the authors' own account, painstakingly human-verified afterward.
Mathematicians have disproved the Heil–Ramanathan–Topiwala (HRT) conjecture — a 30-year-old open problem about whether a signal's time-frequency shifts can ever cancel each other out — with an explicit counterexample that ChatGPT helped find. Markus Faulhuber, Philipp Petersen, Jordy Timo van Velthoven, and Felix Voigtlaender posted the preprint "Linear dependence of time-frequency shifts of a Schwartz function" to arXiv this month. They exhibit a nonzero, infinitely smooth Schwartz function and 12 distinct time-frequency shifts whose weighted sum vanishes exactly — disproving the conjecture even in its strongest known form. Co-author Petersen wrote on LinkedIn that the example "was found with a lot of help from ChatGPT," after which the team "rewrote, improved, and fixed a lot of arguments that seemed obvious to ChatGPT but not to us."
The HRT conjecture, posed in 1996, asks whether any finite collection of time-frequency translates of a nonzero square-integrable function must be linearly independent — a foundational question for Gabor analysis, the mathematics behind representing signals as grids of time-frequency atoms. Three decades of work had produced only positive results: Linnell's lattice theorem, the collinear cases, super-exponentially decaying functions. The new counterexample threads the needle carefully — all but one of its 12 shift points sit on a translate of a lattice, and the constructed function decays rapidly but not super-exponentially, staying just clear of every known special case.
What makes this notable beyond the result itself is how it was produced. Terence Tao, who wrote a "partial digestion" of the counterexample on his blog, notes that AI supplied the initial proof strategy and the numerical guesswork — the team found a configuration where a key matrix function was approximately rank-one, with a numerically verified operator-norm bound of 0.333032, just under the 1/3 threshold the contraction argument needs — while the final proof was written by hand. Tao calls the AI disclosure "responsible," citing a readable overview, proper discussion of the literature, and independent numerical checks; he even used AI assistance himself to understand the argument.
The pattern is now unmistakable: this summer alone, ChatGPT-assisted work produced counterexamples to the Erdős Unit Distance conjecture and the Jacobian conjecture, and now a third decades-old open problem falls to the same workflow — AI doing the inspired guesswork, humans doing the verification and exposition. That division of labor, not machine-written proofs, is looking like the real story of AI in mathematics.
What to watch: whether the construction can be shrunk below 12 shifts — Tao suspects the theoretically minimal n=4 is out of reach for this method — and whether his sketch of a fully non-numerical, Stone–Weierstrass-style variant extends the disproof.
AI found the counterexample; humans turned it into a proof. Is that the right division of labor for mathematical discovery? Tell us in the comments.
Sources: arXiv paper · Terence Tao's blog · Philipp Petersen on LinkedIn · Reddit r/math
