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, Hantao Yu, Runzhou Tao, Steven Wang, Diyi Liu, Tamás Darvas

Proof discovery. The proofs are generated by GPT-5.5 Pro via a simple prover–verifier pipeline; the papers are polished and verified by the contributor.

Formalization. We also formalize the commutative ring theory solutions in Lean using our agentic Lean formalization pipeline, which is available here: (repo)

News

• 2026-07-15: Added write-up for Erdős Problem 1038 - paper.
• 2026-07-09: Open-sourced our LEAN formalization pipeline.
• 2026-07-08: Added write-up for the COLT 2025 open problem on fixed-parameter tractability of zonotope problems (paper) and minimum edge-outerplanar embeddings are poly-time computable (paper).
• 2026-06-28: Added write-up for Erdős Problem 477 (tiling complement) — paper.

Open problems answered

Each problem links to its current write-up and, where available, a machine-checked Lean 4 formalization.

Erdős problems

• Problem 477: — paper
• Problem 1038: — paper

COLT open-problem track

• 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
• Fixed-parameter tractability of zonotope problems (Froese, Grillo, Hertrich, Skutella, COLT 2025) — paper

FOCS 2023 (authors' own open question)

• Adversarial robustness of online leverage-score sampling (Jiang, Peng, Weinstein, FOCS 2023) — paper

Commutative ring theory — Glaz et al., Open Problems in Commutative Ring Theory

• 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

Graph theory open problems

• Minimum edge-outerplanar embeddings are poly-time computable - paper.