This repository collects resolutions of a number of open problems from the COLT open-problem track, commutative ring theory, Erdős problem and an open question from a FOCS 2023 paper by the authors.
Contributor. Binghui Peng, Runzhou Tao, Steven Wang, Hantao Yu, Diyi Liu
Proof discovery. The proofs are generated by GPT-5.5 Pro via a simple prover–verifier pipeline; the papers are assembled with Claude Code, then polished and verified by the authors.
Formalization. We also formalize the commutative ring theory solutions in Lean using our agentic Lean formalization pipeline, fully automated, open source soon!
- 2026-06-28: Added write-up for Erdős Problem 477 (tiling complement) — paper.
Each problem links to its current write-up and, where available, a machine-checked Lean 4 formalization. Write-ups are uploaded gradually and may be merged into a single paper over time.
- Shuffled SGD — the SS–RS–GD inequalities (Yun, Sra, Jadbabaie, COLT 2021) — paper
- Learning measured-output quantum circuits (Kun and Reyzin, COLT 2015) - paper (Partial solution).
- Unweighted data selection for linear regression (Hanneke, Moran, Shlimovich, Yehudayoff, COLT 2025) — paper (Problem 3)
- Robust conditional probability estimation (Langford, COLT 2010) — paper
- Adversarial robustness of online leverage-score sampling (Jiang, Peng, Weinstein, FOCS 2023) — paper
- Problem 4: finite-conductor vs. quasi-coherent rings — paper, Lean
- Problem 20 (Cahen–Fontana–Frisch–Glaz) — paper, Lean
- Problem 27: integer-valued polynomials over algebras (Werner) — paper, Lean (27b)
- Problem 30(c) — paper, Lean
- Problem 477: tiling complement — paper