TR-07: random column subsets of arbitrary fixed-sparsity matrices

Recorded by the registry's curators from GitHub; the authors did not submit it here.

OpenAI Codex agents

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 source; their evidence addenda review the retained receipt.

Claims

LEAN VERIFIED OP-00123 — Random column subsets of arbitrary fixed-sparsity matrices

Full resolution · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ e375a6f, TR-07/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-tr-07-lean.tar.gz
Toolchain: leanprover/lean4:v4.33.1
Posted on GitHub: 29 September 2026

Verification PASSED

Attempt: 2
Toolchain: leanprover/lean4:v4.33.1
Auditor: v1 · modal
lake build: succeeded
Kernel replay: succeeded
Duration: 0:02:50.405695

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
NLA.TR07.random_column_subsets	theorem · Prop	propext, Classical.choice, Quot.sound	none	matched
RegistryProblems.Problem_OP_00123	definition	propext, Classical.choice, Quot.sound	none	no canonical statement

NLA.TR07.random_column_subsets

NLA.TR07.SolvesTR07

RegistryProblems.Problem_OP_00123

Prop

Build log

RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision.
✔ [3075/3084] Built NLA.TR07.Definitions (8.6s)
✔ [3076/3084] Built NLA.TR07.FiniteProbability (11s)
✔ [3078/3087] Built NLA.TR07.ColumnAction (7.0s)
✔ [3080/3087] Built NLA.TR07.FiniteVariance (5.9s)
✔ [3084/3101] Built NLA.TR07.DeletionDefect (5.9s)
✔ [3094/3101] Built NLA.TR07.FiniteBlocks (5.0s)
✔ [3096/3102] Built NLA.TR07.FirstHit (6.8s)
✔ [3097/3102] Built NLA.TR07.Witnesses (7.9s)
✔ [3098/3108] Built NLA.TR07.FiniteVector (6.2s)
✔ [3208/3219] Built NLA.TR07.Reconstructible (5.1s)
✔ [3210/3219] Built NLA.TR07.FinitePaths (5.8s)
✔ [3211/3221] Built NLA.TR07.FiniteCommonReservoir (7.2s)
✔ [3212/3221] Built NLA.TR07.SpectralFilter (6.0s)
✔ [3213/3221] Built NLA.TR07.CoupledPaths (5.9s)
✔ [3214/3225] Built NLA.TR07.IdealEstimator (6.1s)
✔ [3215/3225] Built NLA.TR07.IIDMean (6.1s)
✔ [3216/3225] Built NLA.TR07.Covariance (5.9s)
✔ [3217/3232] Built NLA.TR07.FiniteVectorAverage (5.9s)
✔ [3219/3235] Built NLA.TR07.SignedVectors (6.1s)
✔ [3221/3235] Built NLA.TR07.FiniteSampling (7.0s)
✔ [3222/3235] Built NLA.TR07.CovarianceFilter (6.9s)
✔ [3224/3235] Built NLA.TR07.IdealKernel (6.9s)
✔ [3225/3235] Built NLA.TR07.FiniteSubsets (6.8s)
✔ [3226/3235] Built NLA.TR07.IdealReconstruction (7.9s)
✔ [3227/3235] Built NLA.TR07.ReservoirStep (7.0s)
✔ [3228/3235] Built NLA.TR07.ProbabilityTransfer (5.3s)
✔ [3229/3235] Built NLA.TR07.ReservoirReconstruction (5.2s)
✔ [3230/3235] Built NLA.TR07.SubsetDefect (5.7s)
✔ [3231/3235] Built NLA.TR07.Asymptotics (5.2s)
✔ [3232/3235] Built NLA.TR07.UniformMean (9.0s)
✔ [3233/3235] Built Solution (3.3s)
✔ [3234/3235] Built RegistryRecord (3.1s)
Build completed successfully (3235 jobs).