Issues

• Lean 4 kernel-checked files for the 1d [STEPS2026], 1d [AER2026], 1c [R2026] and 49a [Cla2026] entries

  teorth/optimizationproblems#309 · Filter by author maximusrufus opened on Nov 2, 2026
  1

• 21a: independent ball-arithmetic certificate Λ ≤ 0.169 via the Polymath15 criterion (not descended from the 0.1875 row)

  teorth/optimizationproblems#304 · Filter by author matthewlay6-maker opened on Oct 31, 2026

• 87a: the [Mar1978] row prints 1058.565, slightly below the bound Martinet proves

  teorth/optimizationproblems#289 · Filter by author u00dxk2 opened on Oct 29, 2026

• 46a: the 4 − 2/15 bound is credited to Bourgain's GAFA 1991 paper, which proves 31/8

  teorth/optimizationproblems#218 · Filter by author u00dxk2 opened on Oct 7, 2026

• Formal Refutation of Continuous Optimization: Truncating the ZFC Regress and Auditing Algorithmic Impunity

  teorth/optimizationproblems#211 · Filter by author frintroper opened on Oct 4, 2026

• Numerical Exploration of $C_{10c}$ bounds via SDP Relaxations (CVXPY)

  teorth/optimizationproblems#67 · Filter by author curious7-web opened on Apr 25, 2026
  1