OP-00039 Solution claimed

Zauner's conjecture

Note: The solution claimed here, Radchenko and Wheeler's “Stark units for real quadratic fields and reciprocity laws” (Hexagon 2610.00186, October 2026), is a preprint its authors describe as generated by large language models and checked by them. It proves reciprocity laws for Stark units of real quadratic fields, building on their “Real quadratic fields and finite quantum dilogarithms I” (arXiv:2609.21892), and deduces the conjecture in every dimension through the construction of Appleby, Flammia and Kopp (arXiv:2501.03970), whose twisted convolution identity Appleby, Flammia and Kopp establish for every admissible tuple in arXiv:2609.39192.

Submit a result

Vectors $\phi_1, \dots, \phi_n$ spanning $\mathbb{C}^d$ form an equiangular tight frame (ETF) if $\|\phi_i\| = 1$ for all $i$, $\sum_i \phi_i \phi_i^*$ is a multiple of the identity, and $|\langle \phi_i, \phi_j \rangle|$ is the same for all $i \ne j$. An ETF in $\mathbb{C}^d$ has at most $d^2$ vectors, and one with exactly $d^2$ is a SIC-POVM. Appleby, Flammia and Kopp proposed an orbit of the Weyl–Heisenberg group and proved that it is a SIC-POVM in every dimension $d > 3$, assuming the order-1 abelian Stark conjecture for real quadratic fields and a special-value identity for the Shintani–Faddeev modular cocycle.

Problem. Prove or disprove that for every dimension $d$ there is an ETF of $d^2$ vectors in $\mathbb{C}^d$.

Source: Zauner (1999). Conjecture 24 of Randomstrasse101, in Bandeira's “Mutually Unbiased Bases, ETFs, and Zauner's Conjecture” (2025); Entry 11 of arXiv:2603.29571.

Imported from github.com/MColbrook/AIM.

The statement is adapted from randomstrasse101.math.ethz.ch, whose text is available under CC BY 4.0.

Classification

Primary: FA — Functional Analysis
Secondary: MP, NT
Keywords: equiangular tight frames, quantum information, Randomstrasse101, SIC-POVM
Literature checked: Oct. 2, 2026 by clemens-admin

References

@misc{randomstrasse2025,
  author = {Bandeira, Afonso S. and Dmitriev, Daniil and Lucca, Kevin and Nizi{\'c}-Nikolac, Petar and R{\"o}dder, Almut},
  title = {{Randomstrasse101}: Open Problems of 2025},
  year = {2026},
  eprint = {2603.29571},
  archivePrefix = {arXiv}
}

@phdthesis{zauner1999,
  author = {Zauner, Gerhard},
  title = {Quantendesigns: {G}rundz{\"u}ge einer nichtkommutativen {D}esigntheorie},
  school = {Universit{\"a}t Wien},
  year = {1999},
  note = {English translation: Quantum designs: foundations of a noncommutative design theory, Int. J. Quantum Inf. 9 (2011), 445--507}
}

@misc{appleby2025stark,
  author = {Appleby, Marcus and Flammia, Steven T. and Kopp, Gene S.},
  title = {A constructive approach to {Z}auner's conjecture via the {S}tark conjectures},
  year = {2025},
  eprint = {2501.03970},
  archivePrefix = {arXiv}
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00039.

/-- OP-00039: Zauner's conjecture -/
def Problem_OP_00039 : Prop :=
  ∀ d : ℕ, 1 ≤ d →
  ∃ Φ : Fin (d ^ 2) → EuclideanSpace ℂ (Fin d),
    (∀ i, ‖Φ i‖ = 1) ∧
      Pairwise fun i j =>
        Complex.normSq (∑ k : Fin d, star ((Φ i).ofLp k) * (Φ j).ofLp k) = ((d : ℝ) + 1)⁻¹

Formalised by The Formal Conjectures Authors (Apache-2.0); reviewed by clemens-admin.

Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.

Resolving this problem in Lean

Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.

In lakefile.toml:

[[require]]
name = "RegistryProblems"
git = "https://github.com/cthalhammer/registry-problems"
rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"

In your proof:

import RegistryProblems.OP_00039

theorem resolution : RegistryProblems.Problem_OP_00039 := by
  sorry

In preprint.toml, mapping the claim to the declaration that establishes it:

[[statements]]
label = "Theorem 1"
lean = "resolution"
latex = "..."
problem = "OP-00039"
claim = "full"

To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:

theorem disproof : ¬ RegistryProblems.Problem_OP_00039 := by
  sorry

You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.

Resolution claims

Stark units for real quadratic fields and reciprocity laws v1 Hexagon ↗ AI-Verified

Danylo Radchenko; Campbell Wheeler

We prove that every value of the arithmetic finite quantum dilogarithms constructed by Radchenko and Wheeler (arXiv:2609.21892) is an algebraic unit, and determine the Artin action for arbitrary quadratic pseudolattices. In particular, the associated Stark units belong to the predicted ray class fields and have the predicted Galois action. We use finite Fourier transforms and distribution relations to obtain Frobenius …

Full resolution · not verified · fidelity not established · posted on Hexagon 10 Oct 2026

Status history

When	Change	By	Reason
2026-10-19	Open → Solution claimed	The registry's curators	Stark units for real quadratic fields and reciprocity laws v1 recorded from Hexagon:2610.00186v1.

Citing this problem

This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.

OP-00039, "Zauner's conjecture", clopen.solutions.