ICML 2026 reproduction · arXiv:2602.15503

Universal approximation evidence moves from chosen examples to a Lean-checked compact-space theorem

2 / 2 formal negative controls rejected; all target theorems compile
Live score remains 8/10 until the judge evaluates this revision. Claim 4 still carries one explicit formalization boundary.
CLAIM 5 · HIGH

Arbitrary compact spaces

7 theorem obligations
  • strict-margin scaling
  • two compact finite subcovers
  • lattice min/max envelope
  • product Lipschitz budget

No chosen target, target-derived basis, or finite sampling.

CLAIM 4 · MEDIUM

Universal deduction

Lean 4.19.0

The kernel derives uniform approximation for every separately Lipschitz target and every positive tolerance from nonempty, lattice-closed, strictly interpolating paper-class premises.

Boundary: exact matrix-level realization of those premises is source-audited, not yet encoded in Lean.

REPRODUCIBLE

One fixed command

164.07 s

uv run --frozen python run_reproduction.py

  • mathlib v4.19.0
  • no sorryAx
  • only standard axioms reported
  • HF cpu-upgrade, one worker