Source labels openChecked July 26, 2026

Open Quantum Problem 23: SIC-POVMs

Benchmark open subproblem: existence of a SIC-POVM in dimension $70$ .

Linear algebra AMS 15 AMS 47 AMS 81

Mathematical statement

Benchmark open subproblem: existence of a SIC-POVM in dimension $70$ .

Statement source: Open Quantum Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

hasSICPOVM_70

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem hasSICPOVM_70 : answer(sorry) ↔ HasSICPOVM 70 := by sorry /-- Benchmark open subproblem: existence of a SIC-POVM in dimension $71$. -/@[category research open, AMS 15 47 81]theorem hasSICPOVM_71 : answer(sorry) ↔ HasSICPOVM 71 := by sorry /-- Benchmark open subproblem: existence of a SIC-POVM in dimension $72$. -/@[category research open, AMS 15 47 81]theorem hasSICPOVM_72 : answer(sorry) ↔ HasSICPOVM 72 := by sorry /-- Benchmark open subproblem: existence of a SIC-POVM in dimension $75$. -/@[category research open, AMS 15 47 81]theorem hasSICPOVM_75 : answer(sorry) ↔ HasSICPOVM 75 := by sorry /- ## Full conjecture -/ /-- Do SIC-POVMs exist in every finite dimension? -/@[category research open, AMS 15 47 81]theorem sicPOVMs :    answer(sorry) ↔ ∀ d : ℕ, 1 ≤ d → HasSICPOVM d := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization