Nature just published a paper by Cubitt, Perez-Garcia and Wolf titled Undecidability of the Spectral Gap, there is an extended version on arxiv which is 146 pages long. Here is from the abstract:"Many challenging open problems, such as the Haldane conjecture, the question of the existence of gapped topological spin liquid phases, and the Yang–Mills gap conjecture, concern spectral gaps. These and other problems are particular cases of the general spectral gap problem: given the Hamiltonian of a quantum many-body system, is it gapped or gapless? Here we prove that this is an undecidable problem. Specifically, we construct families of quantum spin systems on a two-dimensional lattice with translationally invariant, nearest-neighbour interactions, for which the spectral gap problem is undecidable".
I am curious about the undecidable part. The abstract says "our result implies that there exists no algorithm to determine whether an arbitrary model is gapped or gapless, and that there exist models for which the presence or absence of a spectral gap is independent of the axioms of mathematics". "Axioms of mathematics" is kind of vague, so in the extended version they phrase it in a Gödelian manner:"Our results imply that for any consistent, recursive axiomatisation of mathematics, there exist specific Hamiltonians for which the presence or absence of a spectral gap is independent of the axioms". But still, axiomatization of which mathematics, how much mathematics do they need to construct their Hamiltonians. Is it real analysis? ZF? ZFC? I can't figure it out even from their theorem statements.
Is this a mathematical proof or something at the "physical level of rigor"? If so, does it produce "concrete" undecidable statements, or are these Hamiltonians as obscure as "I am unprovable"? Does it represent a new way of proving independence results compared to forcing, etc.? In other words, is it an advance on Gödel sentences and the continuum hypothesis?
EDIT: Cubitt gave an interview where he commented on the nature of the result informally:"It's possible for particular cases of a problem to be solvable even when the general problem is undecidable, so someone may yet win the coveted $1m prize… The reason this problem is impossible to solve in general is because models at this level exhibit extremely bizarre behaviour that essentially defeats any attempt to analyse them… For example, our results show that adding even a single particle to a lump of matter, however large, could in principle dramatically change its properties".
Best Answer
I haven't read the paper carefully, but this appears to be a standard undecidability result, of the sort of which there are dozens if not hundreds in the literature, of the same ilk as the undecidability of Wang tilings, the undecidability of the existence of solutions to Diophantine equations, the word problem for groups, and many others.
It's a formal mathematical proof which shows (Theorem 3 in the extended version) that, there is a family of Hamiltonians $H^{\Lambda(L)}(n)$ such that the set of $n$ such that $H^{\Lambda(L)}(n)$ is "gapped" is a complete computably enumerable set.
The connection to things like axiomitizations of math is then completely standard---any correct and consistent system of axioms cannot prove "$H^{\Lambda(L)}(n)$ is not gapped" for all $n$ for which this is true.