Random column subsets of arbitrary fixed-sparsity matrices
Fix an integer $s \ge 2$ and a real $C \ge 1$, and let $r_k \le k$ and $n_k$ be positive integers with $k/r_k \to C$ and $n_k/r_k \to \infty$ as $k \to \infty$. For each $k$ let $M_k \in \{-1, 0, 1\}^{k \times n_k}$ be a deterministic matrix with exactly $s$ nonzero entries in every column, and let $I_k$ be a uniformly random $r_k$-element set of its columns. Write $(M_k)_{:I_k}$ for the $k \times r_k$ submatrix with those columns, and $\sigma_{\min}(B) = \inf_{\|x\|_2 = 1} \|Bx\|_2$. Nothing is assumed about how the supports of the columns intersect. Huang, Rudelson and Tikhomirov proved the conclusion below under an additional hypothesis that limits the number of pairs of columns whose supports share two or more rows.
Problem. Does $$\Pr\{\sigma_{\min}((M_k)_{:I_k}) > \eta\} \to 0 \quad (k \to \infty)$$ hold for every $\eta > 0$, for all such $s$, $C$, $(r_k)$, $(n_k)$ and every such sequence $(M_k)$?
Source: Huang, Rudelson and Tikhomirov (2026), Conjecture 7.1, for every C > 0; stated for C ≥ 1 and r_k ≤ k by OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- PR — Probability
- Secondary
- FA, NA
- Keywords
- OpenProblemsInNLA, smallest singular values, sparse matrices
References
@misc{huang2026,
author = {Huang, Han and Rudelson, Mark and Tikhomirov, Konstantin},
title = {Well-invertible column subsets of sparse matrices are rare},
year = {2026},
eprint = {2607.05384},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-tr07,
author = {Townsend, Alex},
title = {{TR-07}: Random column subsets of arbitrary fixed-sparsity matrices},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/randomized-and-low-rank-approximation/TR-07/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00123.
namespace RegistryProblems.OP_00123
noncomputable section
open scoped BigOperators
open Filter
abbrev Mat (k n : ℕ) := Matrix (Fin k) (Fin n) ℝ
abbrev Vec (n : ℕ) := EuclideanSpace ℝ (Fin n)
/-- Exactly s nonzero signed entries in every column. -/
def SignedSparse {k n : ℕ} (s : ℕ) (M : Mat k n) : Prop := by
classical
exact (∀ i j, M i j = -1 ∨ M i j = 0 ∨ M i j = 1) ∧
∀ j, (Finset.univ.filter fun i => M i j ≠ 0).card = s
/-- The actual selected rectangular matrix acting on its column coordinates. -/
def selectedAction {k n : ℕ} (M : Mat k n) (I : Finset (Fin n))
(x : EuclideanSpace ℝ I) : Vec k :=
WithLp.toLp 2 fun i => ∑ j : I, M i j * x j
/-- Infimum of the selected matrix's norm over its entire Euclidean unit sphere.
Lean's real infimum convention gives zero for the empty unit sphere; the
aspect-ratio hypothesis forces positive sample size eventually, so this
finite-prefix convention has no effect on the asserted limit. -/
def smallestSingular {k n : ℕ} (M : Mat k n) (I : Finset (Fin n)) : ℝ :=
sInf {y : ℝ | ∃ x : EuclideanSpace ℝ I, ‖x‖ = 1 ∧ y = ‖selectedAction M I x‖}
/-- Probability of the strict tail event under uniform sampling without replacement. -/
def subsetTail {k n : ℕ} (M : Mat k n) (r : ℕ) (η : ℝ) : ℝ := by
classical
let samples := (Finset.univ : Finset (Fin n)).powersetCard r
exact ((samples.filter fun I => η < smallestSingular M I).card : ℝ) / samples.card
/-- OP-00123: Random column subsets of arbitrary fixed-sparsity matrices -/
def _root_.RegistryProblems.Problem_OP_00123 : Prop :=
∀ (s : ℕ), 2 ≤ s → ∀ (C : ℝ), 1 ≤ C →
∀ (r n : ℕ → ℕ), (∀ k, r k ≤ k) → (∀ k, r k ≤ n k) →
Tendsto (fun k : ℕ => (k : ℝ) / (r k : ℝ)) atTop (nhds C) →
Tendsto (fun k : ℕ => (n k : ℝ) / (r k : ℝ)) atTop atTop →
∀ (M : (k : ℕ) → Mat k (n k)), (∀ᶠ k in atTop, SignedSparse s (M k)) →
∀ (η : ℝ), 0 < η →
Tendsto (fun k => subsetTail (M k) (r k) η) atTop (nhds 0)
end
end RegistryProblems.OP_00123
Formalised by OpenAI Codex AI agents (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_00123 theorem resolution : RegistryProblems.Problem_OP_00123 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00123" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00123 := 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
Complete original asymptotic target: the smallest singular value of a uniform column subset tends to zero in probability for every admissible deterministic fixed-sparsity matrix sequence. The complete proof builds locally on macOS and its transitive axiom audit passes. Fresh sandboxed Linux Comparator and default-kernel verification passed on 29 September 2026. Two independent nonauthor AI agents approved the complete final mathematical …
For every fixed column sparsity, aspect ratio, and positive singular-value threshold, we prove that a uniformly sampled proportional-size column subset of any sufficiently redundant signed sparse dictionary has a positive fraction of singular values below that threshold, except with exponentially small probability. No hypothesis is imposed on intersections of column supports. The argument combines a covariance polynomial filter, finite signed …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, TR-07/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00123, "Random column subsets of arbitrary fixed-sparsity matrices", clopen.solutions.