Improved integrality of Donaldson–Thomas invariants of loop quivers (GKS Conjecture 1.3 for twist knots)

For the $m$ -loop quiver, the numerical Donaldson–Thomas invariants $\mathrm{DT}^{(m)}_n$ (Kontsevich–Soibelman/Reineke) satisfy $v_p(\mathrm{DT}^{(m)}_n)\ge v_p(n)$ for every prime $p\ge5$ , with exact defects at $p=2,3$ : $v_3\ge v_3(n)-[m\equiv2\ (3)]$ and $v_2\ge v_2(n)-[m\equiv2,3\ (4)]$ , and these bounds are attained. Hence the optimal integer with $n\mid\gamma(m)\mathrm{DT}^{(m)}_n$ for all $n$ is exactly $\gamma(m)=2^{\varepsilon_2(m)}3^{\varepsilon_3(m)}$ . Via the identification of twist-knot extremal BPS invariants with loop-quiver DT invariants, this proves the Improved Integrality Conjecture (Garoufalidis–Kucharski–Sułkowski 2015, Conj. 1.3, an observation they credit to Kontsevich) for all twist knots with optimal constants, reproducing all twelve $\gamma^\pm$ values GKS tabulated empirically. Supporting new results: a derivative theorem for Gaussian binomials at roots of unity, the first $q$ -supercongruence for DT invariants ( $\Phi_p(q)^2\mid R_n$ ), an exact necklace formula for the quantized invariants, and a self-contained proof of the signed $p=2$ Kazandzidis supercongruence.

Result: Proved(see note)
Status: Partial result
AI contribution: AI-discovered
Method: Argument
Field: Arithmetic of Donaldson–Thomas / BPS invariants
Posed by: S. Garoufalidis, P. Kucharski, P. Sułkowski
Year posed: 2015
Years open: 11y
Solved: 2026-07-31
Model: Claude Fable 5
Vendor: Anthropic
Collaborators: —
Verification: Unreviewed
Publication: Announced
Significance: 14 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

The sharp valuation bounds and optimal $\gamma(m)$ are proved for ALL loop quivers $m\ge2$ , hence for the extremal BPS invariants of all twist knots (both rows, matching every twist-knot entry of GKS Table 1). Scope limits: the $m=3$ /figure-eight divisibility $2n_r/r\in\mathbb Z$ was previously proved by Basor–Conrey–Morrison (arXiv:1703.00990), whose per- $r$ $2$ -adic characterization for $m=3$ is finer than the uniform bound; the torus-knot case of GKS Conj. 1.3 (multi-vertex quivers, $\gamma$ growing with the knot) remains open and is not claimed; the general-knot conjecture remains open. The Lean formalization covers the reduction to the classical Kazandzidis congruences, not those congruences themselves.

What the AI did

The model ran the project end to end under human direction in a single supervised session: identified the open conjecture from literature reconnaissance, built two structurally independent exact-arithmetic implementations of the refined DT invariants, mined the divisibility patterns, found and wrote complete proofs (Reineke's formula + Jacobsthal–Kazandzidis supercongruences, including a new self-contained proof of the signed $p=2$ case), wrote the paper, and produced a partial Lean 4/Mathlib formalization (no sorries; reduction to the classical congruence inputs machine-checked, sharpness and the combinatorial core unconditional). An independent AI referee agent (same model family, adversarial prompt) failed the first draft over a scope overclaim and missing prior art (Basor–Conrey–Morrison 2017 had the $m=3$ case), which were fixed before this announcement.

Verification

No independent human review, and the repository says so itself. Evidence in the repo: two structurally independent implementations (plethystic CoHA engine vs. direct cyclic-word enumeration) agreeing on all computed invariants; Theorem 1 checked numerically for $m\le10$ , $n\le120$ and the Kazandzidis inputs to $n=300$ with sharpness; and a two-round adversarial AI referee report, which is author-side and does not count as independent verification here.

The Lean was read here on 24 August 2026 rather than taken on trust. Dtformal.lean carries no sorry, no admit, no native_decide and no axiom declarations whatsoever, on Lean 4.33.0. The classical Kazandzidis congruences enter as explicit hypotheses (`KazOdd`, `Kaz2`) rather than as axioms, and those definitions are faithful to the real congruences - `KazOdd` is $p^{\kappa+v_p(NK(N-K)\binom{N}{K})}\mid\binom{pN}{pK}-\binom{N}{K}$ , and `Kaz2` carries the $(-1)^{K(N-K)}$ sign the $p=2$ case needs - so the conditional theorems are substantive rather than vacuous. `sharp_two`, `sharp_three` and `orbit_sum_zero` take no such hypothesis, matching the claim that sharpness and the combinatorial core are unconditional. Lean was not compiled here, and the output of AxiomCheck.lean is not committed to the repository.

Sources

Submitted by fruppyz on 24 Aug 2026

Improved integrality of Donaldson–Thomas invariants of loop quivers (GKS Conjecture 1.3 for twist knots)

What was actually shown

What the AI did

Verification

Sources

Discussion