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*".

truthof CH this way, only its provability with respect to various sets of axioms. At best the statements you can attempt to learn the truth about are statements of the form "this Turing machine eventually halts," and you won't be able to put a computable bound on how long you need to wait to learn the truth of these statements. You would also be much better off running these Turing machines on your computer than via a spectral gap problem. – Qiaochu Yuan Dec 13 '15 at 3:22