sin ∉ EML(ℝ) — the depth-k zero-count bound
barrierleano-minimal
Prove that every depth-k real EML tree has at most B(k) real zeros. Combined with sin's infinite-zero property, this closes the T01 barrier for sin.
ProgressSubstrate proved in Lean 4 (analyticity, compact-interval finite zeros, depth-1 closed). Two sorries remain in InfiniteZerosBarrier.lean (sin_not_in_eml, sin_not_in_real_EML_k).
What it needsA Wilkie-1996-style o-minimal argument formalized in Mathlib. ℝ_exp is o-minimal; the quantitative bound follows, but Mathlib lacks the structure.
SB(mul, general) = 3 — tight exact-match
superbestlower-boundlean
Show that no 2-node F16 circuit computes x·y on all of ℝ², and exhibit a 3-node witness. Close the general-domain mul cost.
ProgressResolved 2026-04-21. 4112-circuit exhaustive Python search + 3-node witness + Lean skeleton. PROVED_COUNT 27 → 28.
What it needsNative_decide for the 4112-case enumeration is blocked by noncomputable; a clean Lean-native proof would be a nice follow-up.
SB(div, general) = 3 — exp-outer cases
superbestlower-boundlean
No 2-node F16 circuit with F13 / F14 / F15 / F16 as outer node computes x/y on ℝ². Covers 1024 of 4096 total 2-node circuits.
ProgressProved 2026-04-21 in DivLowerBound3.lean (no_exp_outer_2node_div, 0 sorries). The remaining F1-F12 outer cases (3072 circuits) are certified by exhaustive Python search.
What it needsLean formalization of the F1-F12 outer cases. Python search confirms 0 matches on 14 test points.
CompletenessClassification.lean
leanformalization
A structural theorem classifying which F16 operators yield exactly-complete bases (T26, T27, T28 structural rule).
ProgressStated informally. Not started in Lean. Depends on a general completeness framework for F16-generated operator sets.
What it needsA clear Lean statement for 'a set of operators generates every elementary function'. Likely uses density arguments.
PROP 10-A — bump function in ELC
elcconstructionlean
Construct a non-trivial C^∞ bump function using only {exp, ln, +, −, ×, ÷, composition}. Proves ELC contains partition-of-unity primitives.
ProgressSketched in blind session S10. Short Lean proof estimated; would add +1 to PROVED_COUNT.
What it needsA concrete bump function expression + the supporting lemmas for compact support via e^(−1/(1−x²))-style construction.
T19 tight exact bound for |T − i|
strict-grammarnumerical
Tighten the known depth-6 approach |T − i| ≥ 4.76 × 10⁻⁶ to a provable exact lower bound at all depths.
ProgressDepth-6 exhaustive search gives the 4.76 × 10⁻⁶ bound. T19 (strict i-unconstructibility) is Lean-verified under principal-branch semantics.
What it needsA non-approximation bound — almost certainly needs a transcendence-theoretic argument (Hermite-Lindemann variants).
Lean native_decide over 4112 F16 circuits
leantooling
Convert the Python-verified exhaustive search over 4112 F16 circuits into a Lean native_decide proof.
ProgressBlocked: the F16 ops are declared noncomputable in current Lean formalization. Rewriting them as decidable would unblock native_decide.
What it needsA computable model of the F16 F1-F16 operators (using Mathlib Float or a symbolic rational approximation), plus the decision procedure.
Which algebraic cycles land inside ELC?
elcalgebraic-geometry
Characterize algebraic cycle classes whose period integrals have finite EML depth. Related to how far ELC reaches toward Hodge theory.
ProgressStated as a direction in Millennium.lean; the file explicitly flags this as not proved and requiring research-level math.
What it needsA clean statement separating the 'computable by iteration' case from 'admits finite expression'. This is an ELC-boundary-classification problem, not a Hodge-conjecture attempt.