What the team is doing

A snapshot of the math-team's composition, what's been formalized, and what comes next.

1. The team — six entities

What started as two Claude sessions (researcher + prover) has organically grown to five Claude sessions plus you as router. The protocol scaled because the file-system-as-message-bus is direction-agnostic — adding a new role costs an extra inbox/<role>/ directory and a paragraph in ROLES.md, nothing else.

Daniel — you

Human · router · scope arbiter

Spawns sessions, assigns roles, routes urgent traffic, sets and resets scope. Earlier today: "aim the highest possible … no 6-week cap." That instruction is operative.

You are not in any inbox. You're addressed in chat directly.

researcher

Math research · prose · question decomposition

Owns shared/<topic>/notes.md across topics. Currently driving:

  • matrix-foundations (textbook-style, §1–§11 drafted)
  • ai-math-implications (T1–T7 threads + predictions retro)
  • generalization-bounds (survey.md v1 complete)

prover

Lean 4 + mathlib formalization

Owns shared/<topic>/proofs/. Shipped today:

  • §6.3 + §6.4 + §7 + §10 of matrix-foundations in Lean (no sorry)
  • EML targets 1+2 (constructive direction; overlaps tomdif/eml-lean — confirmed)

Deferred: §11 (eigenvalues / charpoly) and the Khovanskii obstruction work below.

math-researcher

Deeper math · novelty hunting · scope-check

Spun up to investigate whether T4 (Galois-theoretic obstruction to EML universality, in the Khovanskii framework) is tractable.

Currently doing the Phase 1 scope-check: surveying mathlib's coverage of monodromy / covering spaces / solvable-group machinery to decide if Tier 1 / 2 / 3 (next section) is reachable.

strategy-researcher

Strategy research · web synthesis · framing

Stitched the Tao + Buzzard + Stanford-symposium picture into "Tier 2 default, Tier 3 stretch." Found tomdif/eml-lean as prior art.

Coordinates with me (strategist) via my strategy/inbox/ + strategy/outbox/. Three messages landed today; all archived.

strategist — me

Audience-fit · distribution planning · this page

Owns strategy/2026-05-10-strategy.md and distribution/.

Built today: 9-section strategy doc (§§1–7 + §8 Khovanskii branch + §9 tier framework), the LinkedIn / whitepaper / GitHub-repo scaffolding, and the live-preview HTML pipeline that's serving this page.

↓ message flow ↓

researcher ⇄ prover   via shared/inbox/<role>/
math-researcher ⇄ prover   via the same
strategy-researcher → strategist   via strategy/inbox/
strategist → strategy-researcher   via strategy/outbox/
all of them ↔ Daniel   via chat (you're the only entity not in any inbox)

2. Active research streams

StreamStateWhere
The Sheffer framework
Sheffer / Core — operator basis, terms, obstruction theory, bridge lemma DONE Sheffer/Core.lean — 0 sorry, framework abstractions all proved
Sheffer / Examples / EML — continuous, negative obstruction AXIOMATIZED · 2 of 4 Sheffer/Examples/Eml.lean — quintic-root non-expressibility. Two Path-B axioms remain: eml_preserves_solvableMonodromy (Khovanskii's lemma) and quinticRoot_has_S5_monodromy_universal (the S₅ Galois fact). The two trivial cases (const and var) have been discharged via the SolvableMonodromy infrastructure. The file has grown to ~5,800 lines: nine analytic helpers for the H1 cross-variable case-enumeration (e_minus_one_mul_exp_ge_add_one, log_exp_sub_le_abs, log_exp_exp_v_sub_const_le, log_triple_nest_witness, others) have landed; three case-enumeration sorries remain.
Sheffer / Examples / NAND — Boolean, positive completeness DONE — 0 axioms Sheffer/Examples/Nand.lean — Sheffer 1913 functional completeness proved via DNF construction.
Sheffer / Examples / PolyAct — polynomial-activation networks DONE — 0 axioms Sheffer/Examples/PolyAct.lean — fully constructive AI-architectural obstruction. Headline: x_pow_9_not_representable_at_depth_3. The cleanest single artifact the team has shipped.
Arithmetic circuit complexity foundations
VP / VNP foundations DONE Sheffer/Foundations/ArithCircuit.lean, 0 sorry, 0 axioms. ArithmeticCircuit, size, eval, toMvPolynomial, IsPolyBound, VPOver, VPOverArity, VNPOver, permanentVar. Style: Bürgisser-Clausen-Shokrollahi 1997 §5.2.
permanent ∈ VNP via Ryser's formula DONE — 0 axioms Sheffer/Foundations/PermanentVNP.lean — Ryser identity + explicit polynomial-size circuit (size $2n^2 + 5n + 2$) + headline closure all proved. 14 step-lemmas plus helpers.
Path A · monodromy infrastructure DONE Sheffer/Foundations/MonodromyGroup.lean — monodromy as a group action, covering maps, fundamental-group homomorphism. 0 sorry, 0 axiom.
Path A · multivalued analytic functions DONE Sheffer/Foundations/MultivaluedAnalytic.lean — structural backbone of Path A; covering map over single-valued domain with per-sheet value function. 0 sorry, 0 axiom.
Path A · concrete hasSolvableMonodromy IN PROGRESS Sheffer/Foundations/SolvableMonodromy.lean — replaces the opaque predicate with a concrete definition built on MultivaluedAnalytic. The const + var Path-B axioms are now discharged against this concrete predicate; the eml-preserves axiom (Khovanskii's lemma proper) is the long pole and is expected to span weeks of formalization.
Phase 4 · PolyAct ↔ VP bridge DONE Sheffer/Foundations/PolyActVP.lean — connects polynomial-activation networks to the VP complexity class. The application that ties Phase 3's foundations to the Sheffer framework's PolyAct example.
H1 · $x + y$ is not depth-3 representable over EML IN PROGRESS Case enumeration of every depth-≤2 EML term over $(x, y)$, showing none equals $x + y$. Nine analytic helpers landed (e_minus_one_mul_exp_ge_add_one, log_exp_a_plus_a_plus_one_le, exp_a_plus_abs_a_plus_two_le_exp, log_exp_sub_le_abs, log_exp_exp_v_sub_const_le, log_triple_nest_witness, others), each a candidate Verdict-A novelty. Structurally ~96% complete; three case-enumeration sorries remain (var-j sub-tree at line 5,464 in flight).
Valiant-conditional architectural bound PLANNED An architectural bound for polynomial-activation networks; the application that ties the foundations to the Sheffer framework's PolyAct example.
Foundational matrix algebra and earlier exploratory work
matrix-foundations §6.3 / §6.4 / §7 / §10 DONE Lean, no sorry MatMul.lean — the textbook formalization that started everything
generalization-bounds survey.md v1 DONE Researcher's option-(a) frame-and-survey, 6 sections + bibliography
matrix-foundations §11 (eigenvalues, charpoly) DEFERRED Out of scope under Target B direction
Junk-value falsifiability test (researcher meta-claim) DONE JunkValueTest.lean — meta-claim survived for 2 of 3 cases
Strategy doc + audience-fit + distribution planning v1 DONE strategy/2026-05-10-strategy.md §§1–10
GitHub repo + explainer site live DONE Repo pushed to dangoodface/math-team (private). Live-preview site at distribution/whitepaper/ — what you're reading right now.

3. The contribution shape

The team is building toward a single layered deliverable: arithmetic-circuit-complexity foundations in Lean, the Sheffer framework that lives on top of them, and a Valiant-conditional architectural bound for polynomial-activation networks that ties the two together. Math-researcher and prover make the tractability calls; the work is on a quality-over-speed timeline.

Tier 3

Novel obstruction theorem proved using the framework

Stretch goal · ~6+ months on top of Tier 2 · highest impact-if-proven

New mathematical result — not just formalization of an existing argument. Plausibly a Mathstodon thread that lands directly in Tao / Buzzard / Avigad's reading. Lex Publica still independent of this.

Tier 2

Khovanskii topological-Galois framework as mathlib infrastructure

Default target · ~3–6 months · closes one of Buzzard's named "holes"

EML obstruction included as worked example; the framework itself is reusable for Abel-Ruffini variants, Liouville-style transcendence, Risch-algorithm theory, future single-operator universality claims. Primary deliverable: mathlib PR (or PR series). Companion paper documents the framework. arXiv preprint when PR is in review.

Tier 1

EML-specific obstruction proof (fallback)

Fallback if Phase 1 returns infeasible · ~6 weeks · narrow contribution

Formalizes Stylewarning's informal critique in Lean, citing tomdif/eml-lean for the constructive direction. Real but narrow; not research-novel because the math is already informally known. Workshop submission becomes plausible at this tier; AI4Math @ ICML 2026 deadline May 25 might fit.

The big shift versus the original brief: mathlib PR is now the primary distribution path, not a workshop paper. A merged mathlib PR is more durable than a workshop paper and gets reviewed by the named-reviewer pool (Buzzard, Massot, Macbeth, Avigad) organically. The companion paper documents and frames the contribution; arXiv preprint is the citable artifact; LinkedIn + whitepaper become popularization layer.

4. Pending decisions

1. The eml-preserves axiom timeline. Khovanskii's lemma (eml_preserves_solvableMonodromy) is the long pole on Path A. Math-researcher's estimate is ~2–4 weeks of formalization once the H1.4 case-enumeration sorries close. Open question: ship the obstruction with this single axiom as the headline gap and discharge it as a follow-up, or hold the whole package until it's clean?
2. mathlib PR readiness. When ArithCircuit, PermanentVNP, MonodromyGroup, MultivaluedAnalytic are merge-quality (style, naming, dependencies), they're plausible mathlib contributions on their own — independent of the obstruction. Decision: spin a PR series for the foundations now, or bundle with the framework paper?
3. Tomdif outreach timing. The repo we'd cite for the constructive direction. Strategy-researcher and I think after-shape (once the framework is publicly visible); happy to revisit.
4. Methodology paper claim discipline. Strategy-researcher's recent novelty pass returned Verdict B on the multi-agent-coordination story: precedent exists (Ax-Prover, MA-LoT, HybridProver, Tao's PFR, LobsterMail). The distinct contribution narrows to "indie director + AI-only team + codified discipline + pattern catalog." Decision: write it anyway with calibrated claims, or wait until the math result is the headline and methodology is a footnote?

5. Distribution infrastructure — what's wired up today

Strategy doc strategy/2026-05-10-strategy.md — ten sections, branches for Khovanskii (§8), tier framework (§9), Target B foundations (§10)
Explainer site (this site) distribution/whitepaper/ · index + overview + math + proofs + interactive + research-report · live-preview via make serve on localhost:8080 · Pagefind search + theme toggle
Style guide (extracted from the crypto whitepaper) distribution/whitepaper/STYLE.md
Communication channels strategist ↔ strategy-researcher via strategy/inbox|outbox|archive/; researcher ↔ prover and math-researcher ↔ prover via shared/<topic>/inbox/<role>/; team event log at log.md
GitHub repo github.com/dangoodface/math-team · private
Structural-consistency audit distribution/audit.sh — verifies nav + main wrapper + cover header + current marker across all served pages; runs in CI-like fashion against the live server

6. What I'd watch this week

In rough order of signal, not work-effort: