Paper deep dive
VALG: An Agentic System for ML Theory Research
Dechen Zhang, Xuan Tang, Xinxiang Yin, Xingwu Chen, Jian Qian, Difan Zou
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 89%
Last extracted: 8/14/2026, 5:58:24 AM
Summary
The paper introduces VALG, an agentic system designed for Machine Learning (ML) theory research. VALG automates the workflow of theorem development by combining multi-level Verification, Adaptive formulation of learning-theory problems, and Graph-structured proof development. It manages source-relative theorem branches, maintains fixed mathematical specifications, and constructs typed proof-dependency graphs. When proof attempts fail, VALG diagnoses the obstruction (derivation, structure, or formulation) and routes accordingly, potentially creating relaxed variants. The system was evaluated on nine subproblems from five COLT 2026 open problems, producing 22 internally finalized theorem candidates, two of which fully matched the source scope.
Entities (61)
Relation Signals (21)
VALG → affiliatedwith → Northwestern Polytechnical University
confidence 95% · Xinxiang Yin3... 3Northwestern Polytechnical University
VALG → affiliatedwith → Shenzhen Loop Area Institute
confidence 95% · Dechen Zhang1,2... 2Shenzhen Loop Area Institute
VALG → affiliatedwith → The University of Hong Kong
confidence 95% · Dechen Zhang1,2... 1The University of Hong Kong
VALG → developedby → Xuan Tang
confidence 95% · We develop VALG... Xuan Tang1
VALG → developedby → Xinxiang Yin
confidence 95% · We develop VALG... Xinxiang Yin3
VALG → developedby → Xingwu Chen
confidence 95% · We develop VALG... Xingwu Chen1
VALG → developedby → Jian Qian
confidence 95% · We develop VALG... Jian Qian1
VALG → developedby → Difan Zou
confidence 95% · We develop VALG... Difan Zou1,2
VALG → developedby → Dechen Zhang
confidence 95% · We develop VALG... Dechen Zhang1,2
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Machine learning theory studies learning procedures through mathematical setups in which the data model, training protocol, oracle access, loss, metric, and randomness define the phenomenon that a theorem is meant to explain. Solving an open problem therefore requires the problem formulation, theorem target, and proof mechanism to be developed in concert. Researchers formulate hypotheses, test them through preliminary theoretical or empirical analysis, and refine both assumptions and proofs. We investigate whether this process can be organized as an autonomous agentic workflow for ML theory research. We develop VALG, an agentic system that combines multi-level Verification, Adaptive formulation of Learning-theory problems, and Graph-structured proof development. Within each source-relative theorem branch, VALG maintains a fixed mathematical specification, checks the theorem-level composition of a typed proof-dependency graph, and constructs and reviews local proofs in dependency order. When a proof attempt fails, VALG identifies whether the obstruction lies in a derivation, the proof structure, or the theorem formulation and routes the next attempt accordingly. Formulation-level obstructions initiate an explicitly related variant or relaxation, preserving the mathematical relation between the resulting theorem and the source problem. We evaluate VALG on nine subproblems from five COLT 2026 open problems. Two runs produce internally finalized theorem candidates that match the scope of their source briefs; the remaining seven yield restricted-method results, special cases, or conditional theorems. These case studies show how VALG keeps source-scope matches, relaxations, conditional results, and blocked attempts mathematically distinct. VALG is open source at this https URL.
Tags
Links
- Source: https://arxiv.org/abs/2608.13060v1
- Canonical: https://arxiv.org/abs/2608.13060v1
Trouble viewing inline? Open PDF directly →
Full Text
154,425 characters extracted from source content.
Expand or collapse full text
VALG: An Agentic System for ML Theory Research and Demonstrations on COLT 2026 Open Problems Dechen Zhang1,2 Xuan Tang1 Xinxiang Yin3 Xingwu Chen1 Jian Qian1 Difan Zou1,2 1The University of Hong Kong 2Shenzhen Loop Area Institute 3Northwestern Polytechnical University Correspondence: dzou@hku.hk August 13, 2026 Abstract Machine learning theory studies learning procedures through mathematical setups in which the data model, training protocol, oracle access, loss, metric, and randomness define the phenomenon that a theorem is meant to explain. Solving an open problem therefore requires the problem formulation, theorem target, and proof mechanism to be developed in concert. Researchers formulate hypotheses, test them through preliminary theoretical or empirical analysis, and refine both assumptions and proofs. We investigate whether this process can be organized as an autonomous agentic workflow for ML theory research. We develop VALG, an agentic system that combines multi-level Verification, Adaptive formulation of Learning-theory problems, and Graph-structured proof development. Within each source-relative theorem branch, VALG maintains a fixed mathematical specification, checks the theorem-level composition of a typed proof-dependency graph, and constructs and reviews local proofs in dependency order. When a proof attempt fails, VALG identifies whether the obstruction lies in a derivation, the proof structure, or the theorem formulation and routes the next attempt accordingly. Formulation-level obstructions initiate an explicitly related variant or relaxation, preserving the mathematical relation between the resulting theorem and the source problem. We evaluate VALG on nine subproblems from five COLT 2026 open problems spanning tensor decomposition, learning complexity, one-bit mean estimation, differential privacy, and online optimization. Two runs produce internally finalized theorem candidates that match the scope of their source briefs and address the original subproblems; the remaining seven yield restricted-method results, special cases, or conditional theorems. For each candidate, we report the problem setup, theorem statement, and progress relative to the source problem. These case studies show how VALG keeps source-scope matches, relaxations, conditional results, and blocked attempts mathematically distinct. VALG is open source. VALG: https://github.com/DechenZhang/VALG-ML-Theory-Agent/tree/main/skills COLT Problem Solutions: https://github.com/DechenZhang/VALG-ML-Theory-Agent/tree/main/case-studies 1 Introduction Machine learning theory studies learning procedures through mathematical setups that specify how data are generated, what information an algorithm can use, which loss or risk is measured, and how performance scales with problem parameters. This viewpoint is already present in classical PAC learning and statistical learning theory, where the hypothesis class, distributional model, sample size, loss, and success probability are part of the statement being studied (53; 54; 45; 55). Modern learning-theory papers often make the same structure more explicit: a result may depend on the training protocol, oracle model, randomness model, tail condition, approximation notion, or asymptotic regime. In this literature, such choices usually appear in the theorem statement itself, because they specify the learning phenomenon under study. Consequently, ML-theoretic research often proceeds as a concurrent process in which the problem setup, theorem formulation, and proof technique are discovered and refined together. This flexibility can yield scientifically useful outcomes: a well-stated relaxation, a conditional theorem, or a restricted setting can illuminate why the original problem is hard and which assumptions are essential. It also creates a risk. Once the protocol becomes adaptive, the representation approximate, the claim distribution-dependent, or the target property assumed, the resulting theorem may no longer address the original problem. This observation points to a need for systematic support: when the setup, theorem formulation, and proof technique co-evolve, a reasoning system for ML theory must track that evolution explicitly. Recent language-model systems have made substantial progress on extended reasoning. General-purpose agents combine generation, tool use, feedback, and refinement across multiple steps (65; 46; 35). Scientific-agent systems organize research into literature search, hypothesis generation, experimentation, critique, and paper writing (33; 43; 18), while research-agent benchmarks evaluate extended machine-learning tasks rather than single responses (20; 9; 59; 49). Mathematical research agents coordinate conjecture generation, long-horizon proof search, criticism, and revision in natural language, while AI4Theory systems also connect literature synthesis, theorem proving, algorithm design, and numerical experiments (16; 30; 70; 19). In parallel, formal-mathematics agents use proof assistants, retrieval, and repair loops to prove or formalize fixed statements, including complete research-paper developments and statistical learning theory libraries (64; 23; 68; 67). Together, these advances leave an ML-theory-specific pre-formalization question: how should an agentic system manage informal theorem development when both the proof and the problem formulation may require revision? To this end, we develop VALG 11 1 The name also honors four pioneers of learning theory: Leslie Valiant, whose PAC framework formalized efficient learnability (53); Dana Angluin, whose L∗L algorithm established polynomial-time exact learning of regular languages from membership and equivalence queries (2); Nick Littlestone, whose mistake-bound analysis and Winnow algorithm shaped online learning (28); and E. Mark Gold, whose identification-in-the-limit framework provided an early mathematical model of language learning (17)., an agentic system that combines multi-level Verification, Adaptive formulation of Learning-theory problems, and Graph-structured proof development within source-relative theorem branches. The task requires generating a plausible proof while tracking the theorem under consideration, every added assumption, the cause of each failed attempt, and the relation of any revised formulation to the source problem. Each branch in VALG fixes one mathematical specification and represents its proof as a typed dependency graph from primitive assumptions, through intermediate lemmas, to the target theorem. Before local proof work begins, a mechanism-aware global analysis checks the mathematical source of each hard claim, the compatibility of lemma interfaces, and the closure of recursive or limiting arguments. Proof development then proceeds from global structure to local derivations. We localize failures to a derivation, the proof graph, or the theorem formulation; only formulation-level obstructions create a new variant or relaxation. Specialized reviewers separately examine structure, rigor, citation use, and adversarial boundary cases before assigning a source-relative outcome. We evaluate VALG on nine subproblems drawn from five COLT 2026 open-problem papers: tensor ALS/GD overparameterization (3), distribution-independent deep or statistical-query learning versus linear dimension complexity (15), non-adaptive one-bit mean estimation (25), differential privacy PAC learning (38) and online optimization of Piecewise-Lipschitz functions (5). These questions remain unresolved in the source works and provide a substantive testbed beyond synthetic proof-generation tasks. Across nine runs, VALG produces 22 internally finalized theorem candidates. Two runs produce finalized theorem candidates that fully match the scope of their source subproblems; the remaining seven yield restricted-method results, special cases, or conditional theorems. For each run, we report the problem setup and finalized theorem for selected representative candidates, together with an assessment of their progress toward the corresponding open problem. Contributions. Our contributions are highlighted as follows: 1. We formulate informal ML-theory research as an agentic theorem-development problem, in which the learning setup, assumptions, theorem target, proof dependencies, and relation to the originating research question must be developed and tracked together. This formulation reflects the fact that ML theory often requires refinement of both the mathematical assumptions and the object being proved. 2. We develop VALG, which organizes this process through source-relative perspective–idea branches, fixed theorem contracts, typed proof-dependency graphs, and a sketch–global–step–assembly proof pipeline. The architecture separates open-ended problem design from contract-based proof development and assigns different review mechanisms to the two stages. 3. We introduce a hierarchical diagnosis and revision mechanism that localizes failures to the derivation, proof graph, or theorem formulation. Local failures trigger local repairs, structural failures trigger proof-architecture revisions, and only formulation-level obstructions create an explicitly source-related variant or relaxation. This allows VALG to retain the mathematical relationship between a revised theorem and the original ML-theory problem rather than silently replacing the target. 4. We apply VALG to nine subproblems drawn from five COLT 2026 open-problem papers and obtain 22 internally finalized theorem candidates. Two runs produce candidates that match the scope of their source subproblems, while the remaining seven produce restricted-method results, special cases, or conditional theorems. The case studies illustrate how an agentic system can distinguish source-scope matches from related but weaker results and unsuccessful branches when developing theory for unresolved ML problems. The retrospective focuses on branch records and their mathematical outcomes. Organization. Section 2 positions the work relative to informal mathematical-reasoning agent, formal theorem proving and research-agent benchmarks. Section 3 presents the theorem-development method, and section 4 then examines the COLT open problems and the resulting theorem candidates. The paper closes with limitations and open directions. 2 Related Work 2.1 Mathematical discovery and research agents AI for mathematics includes neural–symbolic systems for conjecture formation, geometry, and executable program search (13; 51; 41; 39), as well as more open-ended systems that combine conjecturing, computation, and symbolic solving (11; 10; 61). General scientific research agents extend this pattern across ideas, experiments, literature, and writing (33; 43; 18); mathematical research places additional weight on constructing and checking long derivations. Research-level proof agents organize natural-language mathematics around generation, criticism, and revision. Aletheia scales a generator–verifier–reviser loop across pure mathematics, while ProofCouncil and RMA distribute analysis, literature use, proof construction, criticism, and computation across specialized roles (16; 44; 69). Rethlas, QED, and the MechMath Agent Team connect informal exploration with formal checking through theorem retrieval, decomposition, and natural- or formal-language provers (22; 1; 8); the AI Co-Mathematician instead supports interactive refinement of definitions, questions, conjectures, computations, and proof directions (70). Danus addresses long-horizon coordination through parallel proof search and a shared fact graph (30). A main agent redirects workers across lines of attack, while a stateless verifier checks each natural-language claim before the claim, its proof, and its logical dependencies enter the graph. This structure lets many local contributions accumulate into a long argument and supports transitive removal when an accepted fact is later rejected. Its fact graph is close to our typed proof dependencies, although Danus terminates when a supplied target or its refutation becomes a verified fact. VALG additionally separates a proposed proof architecture from theorem-level feasibility and local derivations, and it treats a formulation-level obstruction as a reason to create an explicitly source-related theorem branch rather than to edit the target in place. The closest AI4Theory systems extend agentic research beyond pure proof: ReasFlow integrates literature synthesis, algorithm design, theorem proving, numerical experiments, and manuscript preparation, while Iteris combines proof drafts with numerical and adversarial exploration (19; 10). VALG focuses more specifically on ML-theory questions whose learning setup, assumptions, and theorem target may co-evolve. It records whether a result addresses the source question itself, a restricted method, a special case, or a conditional variant; this source-relative distinction guides both failure routing and case-study evaluation. 2.2 Formal theorem proving agents Formal theorem proving begins after a mathematical statement and its assumptions have been encoded in a proof assistant. The kernel then supplies an exact acceptance criterion for a completed proof. LeanDojo provides a programmatic Lean environment, premise annotations, and retrieval-augmented proving benchmarks, while HyperTree Proof Search combines learned proof-step proposals with structured search (64; 24). COPRA wraps a general-purpose language model in stateful backtracking search and uses proof assistant errors and retrieved lemmas as feedback (50). Subsequent systems improve formal proof search through synthetic data, proof-assistant feedback, informal planning, and reusable lemma libraries. DeepSeek-Prover and its later versions combine large-scale Lean data, reinforcement learning, tree search, and subgoal decomposition; Lean-STaR interleaves informal thoughts with tactic generation; and LEGO-Prover and DreamProver grow transferable libraries of verified lemmas across problems (62; 40; 27; 56; 66). OpenProver, OProver, Numina-Lean-Agent, and LAMP expose agentic interaction, verifier-guided repair, and tool use in Lean, while Discover and Prove separates answer discovery from formal proof for hard-mode statements (23; 34; 31; 42; 29). These methods can provide kernel-checked correctness for the encoded theorem, but they generally take the formal target as fixed; they do not decide whether a revised learning-theory formulation remains a meaningful answer to an originating research question. AI4SLT brings this formal perspective directly to machine learning theory. It combines human-designed proof strategies with AI-assisted Lean construction to develop an empirical-process library containing Gaussian concentration, Dudley’s entropy integral, and sharp least-squares regression rates (67). The formalization reveals implicit assumptions and omitted steps in standard presentations, demonstrating the value of machine-checked ML theory. Its objective is to formalize an established mathematical development; VALG instead operates earlier, when the learning setup and theorem target are still under construction, and can pass a finalized branch to such a formal verification workflow. 2.3 Autoformalization Autoformalization addresses a different interface: translating natural-language mathematics into a formal statement or proof. Early LLM-based work demonstrated statement translation into Isabelle, ProofNet paired informal undergraduate problems with Lean statements and proofs, and MMA expanded training through large-scale multilingual informal–formal pairs (60; 4; 21). A recent survey organizes this rapidly growing area by mathematical domain, model, data, and evaluation strategy (58). Recent work moves from isolated statements toward complete proofs and research libraries. ProofFlow first recovers a directed dependency graph from an informal proof and formalizes its steps as intermediate lemmas, explicitly measuring semantic and structural fidelity (7). Beyond the Library introduces an agentic pipeline that can add definitions and auxiliary lemmas missing from Mathlib when formalizing research papers, and TOMAP concentrates test-time refinement on the decomposition that supplies claims, assumptions, and dependencies to downstream formalizer and prover agents (37; 32). FormalRx diagnoses semantic misalignment by error type and location rather than returning only a binary translation score, while theory-level autoformalization argues that useful formalization must ultimately construct coherent libraries of definitions, lemmas, theorems, and their interdependencies (57; 36). LeanMarathon addresses long-horizon research-paper formalization through an evolving Lean blueprint that serves as both proof skeleton and natural-language proof graph. Four specialized agents stabilize target fidelity and discharge the resulting dependency graph from its leaves in parallel, producing complete Lean formalizations of seven target theorems from recent research papers (68). These graph- and theory-level perspectives are close to VALG’s emphasis on compositional structure. Their input, however, is an existing informal statement or proof to be translated faithfully; VALG uses a dependency graph earlier, while constructing and revising the theorem itself, and leaves proof-assistant formalization as a separate verification layer. 2.4 Benchmarks for mathematical and research agents Formal benchmarks such as miniF2F, ProofNet, and PutnamBench evaluate proving or formalizing fixed competition and undergraduate problems (71; 4; 52). Research-level evaluations instead use expert-proposed open problems, as in Aletheia’s FirstProof benchmark (16), or extract larger problem collections from the mathematical literature. RMA evaluates an agentic system on research-level problems, while ResearchMath-14K collects 14,056 questions and documents recurrent failures including fabricated references, non-attempts, and substitution of a narrower problem (69; 48). These failures motivate evaluating both mathematical validity and fidelity to the supplied research question. Research-agent benchmarks cover a broader executable workflow. MLAgentBench evaluates iterative model training, debugging, and experimental improvement; MLE-bench expands this setting to 75 offline Kaggle competitions; and RE-Bench compares agents with human experts under different time budgets (20; 9; 59). Other suites begin from published scientific work: CORE-Bench tests computational reproducibility, PaperBench asks agents to replicate complete AI papers, and ScienceAgentBench isolates expert-validated scientific coding tasks (47; 49; 12). These benchmarks measure experimentation, research engineering, reproducibility, and data analysis under fixed task specifications. Our case studies address a complementary question: whether an agent can develop a theorem and, when necessary, a related formulation while keeping each outcome mathematically tied to the original ML-theory problem. 3 VALG: ML Theory Research Agent VALG develops theorem candidates from an ML-theory research direction or question. Starting from a source problem, it maps the relevant literature, identifies distinct perspectives, develops mechanism-level ideas, formalizes each viable idea as a precise setting and goal, constructs and reviews a proof from global structure to local derivations, and reports every accepted theorem relative to the source problem. A run may return zero, one, or several accepted theorem candidates. VALG divides theorem development into a pre-proof stage for formalizing the problem setup and a proof-review stage for constructing and checking the proof. Dedicated revision loops operate at both stages because local derivations, proof structure, and theorem formulation require different repairs. Figure 1 summarizes the complete workflow. WORKFLOW 1 ⋅· IDEA DISCOVERY✓ checkpoint INPUT Research direction source question + optional research brief STAGE 01 Literature survey constraints, results, gaps STAGE 02 Perspective selection distinct, gap-grounded lenses M≤3M\!≤\!3activebranches STAGE 03 Idea generation mechanism, support, duplicate gate STAGE 04 Formalization objects, assumptions, exactly one goal theorem contract for branch m ✓ ✓ ✓ ✓ 2 ⋅· SPLIT THEORY PROOF ⋅· repeated for every active branch PRODUCE ⋅· STAGE 01 Proof sketch typed dependency DAG REVIEW ⋅· STAGE 02 Sketch review early viability gate PRODUCE ⋅· STAGE 03 Global proof whole-theorem diagnostic REVIEW ⋅· STAGE 04 Global review viability + obstruction localization retry: sketch / idearetry: global / sketch / idea PRODUCE ⋅· STAGE 05 Step proofs S1,…,SkS_1,…,S_k in dependency order REVIEW ⋅· STAGE 06 Step reviews fresh independent review for every SiS_i PRODUCE ⋅· STAGE 07 Proof assembly accepted steps → self-contained manuscript retry: step / dependency / sketch REVIEW ⋅· STAGE 08 Specialized final reviews structural ∣ rigor ∣ citation ∣ adversarial REVIEW ⋅· STAGE 09 Aggregate final review sole controller-facing verdict ACCEPT ⋅· STAGE 10 Finalize accepted branch verify gates; copy setting, manuscript, and final review retry: assembly / step / sketch / ideascore ≥7≥ 7, no blockersFAILURE-LOCALIZED ROUTINGReviewers diagnose; the controller selects the smallest valid producer retry. ASSEMBLY flaw → 07 LOCAL STEP step/dependency → 05 PROOF STRUCTURE diagnostic → 03 graph/interface → 01 THEOREM CONTRACT failure → new idea Budget escalation: local unit → sketch → new idea → branch failure CONTROLLER INVARIANTSGATESvalidate artifacts before useWORKERS22 run-scoped; 12+2k12+2k per branchRUN MODEinteractive pauses; autopilot proceedsBoth modes enforce coverage, budgets,and accepted-copy verification. Figure 1: The VALG workflow. Workflow 1 creates active perspective branches; Workflow 2 is shown for one branch. Teal, amber, and green denote producers, independent reviewers, and accepted output, respectively. Solid arrows show validated forward flow. A finalized branch does not stop the remaining branches. 3.1 Workflow 1: Pre-Proof Stage Theorem proving in pure mathematics often begins with well-defined problem setup, including formalized assumptions, mathematical objects and targets. However, an ML-theory research question is often less settled. It may specify a learning phenomenon but leave open which model subclass, data distribution, algorithmic mechanism, performance metric, or asymptotic regime makes a theorem both true and informative. Workflow 1 therefore treats problem formulation as an explicit research task rather than an implicit prerequisite for proof search. The workflow begins with a source question and, when available, an accompanying research brief. Guided by the literature survey, it organizes exploration around a two-level perspective-idea hierarchy. A perspective provides a broad research lens, whereas an idea fully specifies a concrete problem setup sufficient for downstream formalization and theorem proving. Steps of Workflow 1 are summarized as follows. 1. Literature survey. The literature worker maps the relevant settings, results, proof techniques, and evidence-supported gaps. Different from conventional literature survey in auto research, ML-theory research • should separate empirical evidence from theoretical foundations to discover research gaps in explaining empirical phenomenon; • should determine applicable theoretical testbeds to study theoretical research question. We therefore separate existing literature into direct theoretical sources, foundational theoretical frameworks and empirical practice, while preserving the constraints that define the source direction. 2. Two-level perspective-idea structure. • Breadth-focus perspective selection. The perspective selector to select a small set of distinct, gap-grounded perspectives and launches them as parallel research branches, where a perspective is defined as a coherent, literature-supported research lens, represented by the normalized tuple (analysis target,model class,data assumption,regime,algorithm).(analysis target,\ model class,\ data assumption,\ regime,\ algorithm). Such characterization for perspective distinguishes a meaningful research direction, such as the desired theoretical guarantee, model and data setting, learning regime, or algorithmic family. It needs not fix every aspect of the eventual theorem; rather, it defines a broad search region and leaves appropriate choices open for refinement during idea generation. • Depth-focus idea generator. Within each perspective branch, an distinct idea generator proposes a concrete mechanism and candidate result using the upstream perspective as an explicit anchor. Ideas that are unsupported by the literature or duplicate ideas already proposed in another branch are rejected. Each generated idea must be a field-wise specialization of its upstream perspective: it may make the analysis target, model class, data assumption, regime, or algorithm more specific, but it may not broaden any of these choices or contradict the perspective. This separation keeps exploration broad without spending all proof effort on a single interpretation, while giving each surviving branch a focused mechanism and theorem target. 3. Formalization. For each viable, nonduplicate idea, the formalizer fixes the notation, primitive assumptions, quantifiers, regime, and exactly one mathematical goal. The resulting setting is the theorem contract passed to Workflow 2. Human-expert interactive mode. We remark that early failures are expected: • research gaps from literature survey may not be valuable in research level; • perspectives may be too narrow, too broad, or redundant; • ideas may depend on assumptions that make the resulting theorem unacceptable. Because these decisions are scientific as well as formal, Workflow 1 places a human-expert checkpoint after each stage. In interactive mode, the expert may approve the artifact, edit it, or request a new search or generation with human-expert feedback. Autopilot mode proceeds with approval by default, but retains the same source-direction fidelity and branch-coverage constraints. In either mode, only a checked and formalized branch enters proof development. 3.2 Workflow 2: Proof-Review Stage Following Workflow 1, Workflow 2 develops mathematical proofs based on the provided formalized setting and goal. Our initial approach relied on monolithic proof generation, which entangles theorem-level architecture, local derivations, and final exposition. This method suffered from one severe limitation: the resulting proofs were too compact to effectively review or understand. Drawing on recent progress in natural-language mathematical reasoning, where systems typically generate a proof plan, tackle each step individually, and then assemble the final proof (1; 22; 16), we introduced a similar sketch-step-assembly decomposition to make local claims individually addressable. This decomposition, however, revealed a second gap: a structurally coherent dependency graph does not guarantee that every node is derivable from its assigned inputs, nor does it ensure that its conclusion possesses the precise form and quantitative strength required downstream. To resolve this, we inserted a theorem-level global diagnostic between the sketching and local proof phases, ultimately structuring Workflow 2 as a four-stage sketch-global-step-assembly pipeline. 3.2.1 Proof Stage 1. Proof sketch. The sketch worker represents the proposed argument as a directed acyclic dependency graph. Source nodes encode primitive assumptions, internal nodes encode lemma-sized claims, and the unique sink is the target theorem. Each node records its exact claim, dependencies, permitted assumptions, intended proof tool, and required output interface. 2. Global proof. The global-proof worker expands the accepted graph into a whole-theorem diagnostic. For every node, it traces the available inputs, identifies the mechanism or cited result that could establish the claim, and checks whether the output has the form and strength required by downstream nodes. At theorem level, it audits quantitative dependence, probability and convergence modes, object compatibility, closure arguments, boundary behavior, and the composition of local interfaces. Global proof is crucial as proof dependency graph consistency does not ensure theorem-level composability and local-derivation feasibility. For example, an upstream guarantee for a surrogate object may not imply the guarantee required for the original target downstream. The global diagnostic identifies these cross-step mismatches, specifies each step’s admissible inputs and required output, and guides step workers for full local derivations. 3. Proof step. A dedicated step worker converts one graph obligation into proof evidence using the formal setting, accepted dependency results, and the global diagnostic as context. It may introduce local lemmas, but must state and prove them before deriving the exact assigned claim, without strengthening assumptions or weakening the required output. 4. Proof assembly. Once all required steps are accepted, the assembler reconciles notation and composes their claims into a self-contained LaTeX theorem manuscript. This stage verifies that the accepted local interfaces yield the stated theorem in one coherent presentation. 3.2.2 Review Stage We would like to highlight a key difference between Workflow 1 and Workflow 2 in review mechanisms because they govern different kinds of decisions. Human-expert checkpoints versus agent reviewers • Workflow 1 uses human-expert checkpoints because evaluating literature gaps and selecting research perspectives and theorem formulations require open-ended judgments about research value that depend strongly on human expertise. • Workflow 2 begins from a fixed theorem contract. This contract allows reviewers distinct from the producers to assess each proof artifact against explicit, stage-specific obligations of goal alignment, assumption fidelity, logical soundness, and derivational rigor before the controller authorizes its downstream use. Because both the target and the evaluation criteria are fixed, this contract-based review is better suited to specialized agent reviewers than the open-ended decisions in Workflow 1. Hence, within Workflow 2, we place a distinct sketch reviewer checks proof architecture after the sketch worker, a distinct global reviewer checks theorem-level feasibility after the global proof worker and a distinct step reviewer checks local derivations after the proof step worker. This separation prevents producer self-validation and exposes defects at the same level of abstraction at which they arise. Below we show the key rubrics of both sketch and step reviewers. Key rubrics • Proof-sketch review (/proof-sketch-review). 1. Goal fidelity. Check exact-goal or target-spec alignment, including quantifiers, regimes, probability or convergence modes, normalization, and exposed rate dependence. 2. Graph and coverage. Verify an acyclic graph of stable, lemma-sized steps with legal earlier dependencies, allowed assumptions, intended proof tools, output targets, and explicit blockers for unresolved high-risk obligations. 3. Provenance and interfaces. Trace assumptions, derived invariants, and cited tools to legal sources; trace every generated output from producer to consumers and through any required current-notation or residual-to-target bridge. 4. Viability gates. Check mechanism witnesses, baseline and entry behavior. • Proof-step review (/proof-step-review). 1. Local-unit audit. Check every local lemma statement and derivation against the exact sketch-row claim, allowed assumptions, and accepted dependencies. 2. Hidden-claim and provenance audit. Scan for independent subclaims; trace assumptions, constants, rates, events, and notation; restate cited results in current notation with all hypotheses discharged; stress quantifiers, modes, and boundary cases. 3. Target assembly. Verify that named local results, checked citations, and accepted dependencies jointly establish the exact target claim without strengthening assumptions or weakening the required output. For assembly worker, which is the first stage where all accepted components, notation, citations, and connecting implications must jointly establish the exact theorem, however, the substantial review task motivates us to separate review into independent, multi-angle reviews (1): dependency and coverage errors (structural), invalid derivations (rigor), misapplied external results (citation), and hidden boundary-case failures (adversarial). Each reviewer is therefore tied to a specific assembly-level risk, rather than being an arbitrary addition. Finally, an aggregate reviewer reconciles them into the sole controller-facing final-review verdict and identifies the smallest admissible repair target. Key rubrics • Structural review (/proof-review-structural). 1. Check the assembled claim against the setting, close every dependency, trace every required sketch step into an accepted proof and the public appendix. 2. Reject independent mathematics introduced during assembly. 3. The public LaTeX must remain self-contained, paper-ready, and explicit about its assumptions and theorem-style references. • Rigor review (/proof-review-rigor). 1. Inspect the actual derivations rather than labels or environment counts. 2. Audit quantifier order, constants and parameter dependence, probability and convergence modes, assumption provenance, explicit-rate specialization bridges, interchanges, and boundary cases. 3. Compare every used step’s proof obligations with its appendix proof body. • Citation review (/proof-review-citation). 1. Verify that each cited or internal result exists and supports the exact conclusion used, translate its objects and notation into the current setting, and discharge every hypothesis in the claimed regime. 2. Check BibTeX keys and internal label–reference pairs. • Adversarial review (/proof-review-adversarial). 1. Attack the weakest claims with concrete assumption-minimal, boundary, degenerate, and extreme regimes. 2. Test hidden assumption strengthening, unsupported scope or convergence-mode upgrades, unproved derived invariants, and failed baseline reductions. 3. Treat verified breaks and unresolved high-risk candidate counterexamples as blocking. 3.3 Revision Loops A failed proof attempt may expose a defect in a local derivation, a dependency interface, the proof architecture, or the theorem formulation itself. In ML-theory research, it may also show that the initial problem setup requires an additional condition or a revised assumption before a valid theorem is possible. VALG therefore uses a hierarchy of revision loops that routes each diagnosis to the smallest stage capable of repairing it. This hierarchical structure, along with its corresponding review routing mechanisms, is organized as follows: proofassembly→proofstep \ assembly→\ proof\ step →proofsketch→idea \ sketch globalproof \ proof ↗ 3.0pt$ $ • proof-sketch review: ACCEPTED, REVISE_SKETCH, or IDEA_FAIL; • global-proof review: ACCEPTED, REVISE_GLOBAL, REVISE_SKETCH, or IDEA_FAIL; • proof-step review: ACCEPTED, REVISE_STEP, BLOCKED_BY_DEPENDENCY, or REVISE_SKETCH; • aggregate final review: ACCEPTED, PROOF_ASSEMBLY_FLAW, PROOF_STEP_FLAW, PROOF_SKETCH_FLAW, or IDEA_FAIL. In every case, the failed review identifies the smallest repair target, the controller selects the responsible stage subject to its retry budget 22 2 If a stage’s retry budget is exhausted, the controller escalates the issue by routing it to a higher-level stage that still has remaining budget., and the selected producer uses the accepted upstream context, the failed attempt, and the validated diagnosis to change only the implicated part. Figure 2 summarizes this controlled revision cycle. 1 CURRENT ATTEMPT Attempt a Evaluate one stage result against its stated target and accepted inputs. 2 INDEPENDENT REVIEW Diagnose the failure Identify the failure type and the smallest mathematical object that must change. 3 CONTROLLER ROUTING Select the repair level Validate the diagnosis and route one scoped retry to the responsible stage. 4 SELECTED PRODUCER Construct Attempt a+1a+1 Revise only the implicated mathematical component. 5 FRESH REVIEW Check the revision Repeat the required independent review or human checkpoint before downstream use. Accepted Advance the revised result downstream blocking: return to Step 3 Figure 2: Controlled revision in VALG. An independent review identifies the smallest repair target, the controller routes the diagnosis to the responsible stage, and the selected producer revises only the implicated part. The revised attempt must pass a fresh independent review or human checkpoint before downstream use. 4 COLT 2026 Case Studies We evaluate VALG on nine subproblems drawn from five COLT 2026 open-problem papers (25; 3; 5; 38; 15). Each subproblem is run independently from a research brief extracted from its source description, using GPT-5.6-sol at maximum reasoning effort. Finalized theory candidates have been checked through independent multi-perspective LLM reviewing and roughly audited by human33 3 The correctness of the proof may also need to be verified by more experts, especially the authors of these open-problem papers. . Table 1 reports every perspective branch represented in the archived runs. Within a run, VALG may develop several perspective branches (with maximum budget 3) in parallel. For each perspective branch, the idea generator prioritizes a source-faithful candidate aimed at fully resolving the subproblem. If no such ideas are viable, it will then attempt to propose an idea with partial-progress type, i.e., a relaxed problem setup. After the first idea is proposed, subsequent idea variants are opened only after explicit controller routing, such as an idea-level review failure, or escalation after lower-level retry budgets are exhausted. See Section 3.3 for illustration of the revision rules. Table 1: Perspective-level search and evaluation summary. Problem Subproblem Persp. Ideas tried Branch outcome Elapsed (h) Progress Rank P1: Tensor ALS Upper bound 1 7 Idea 7 76 6.50 1 2 14 Exhausted – 0.00 2 Lower bound 1 2 Idea 2 8 2.25 2 2 2 Idea 2 11 3.00 1 3 3 Idea 3 38 3.00 3 P2: 1-bit mean estimation Non-adaptive 1 1 Idea 1 13 10.00 2 2 2 Interrupted – 0.00 3 3 1 Idea 1 9 10.00 1 P3: Deep vs. linear learning SGD 1 3 Idea 3 12 2.75 2 2 2 Idea 2 10 2.25 3 3 2 Idea 2 12 5.25 1 SQ 1 3 Idea 3 15 2.75 2 2 2 Idea 2 8 3.00 1 3 2 Idea 2 9 2.25 3 P4: Private PAC learning Sample complexity 1 3 Idea 3 48 6.50 1 2 4 Idea 4 91 6.25 2 3 1 Idea 1 28 5.25 3 Class existence 1 5 Idea 5 28 3.00 2 2 2 Idea 2 25 5.50 1 3 6 Exhausted – 0.00 3 P5: Online optimization Polynomial 1 1 Idea 1 12 5.75 2 2 1 Idea 1 24 7.00 1 Pfaffian 1 1 Idea 1 30 10.00 1 2 1 Idea 1 40 10.00 2 3 1 Idea 1 31 6.75 3 Progress P∈[0,10]P∈[0,10] is evaluated against the original paper’s subproblem by a distinct agent. Rank is computed within each subproblem from 0.40×0.40\,× progress, 0.40×0.40\,× mathematical soundness, and 0.20×0.20\,× technical novelty by a distinct agent. Exhausted indicates that the branch consumed its configured idea-variant budget without finalizing a theory, whereas Interrupted indicates that execution ended before finalization by human. A dash denotes unavailable elapsed time. We would like to remark that progress is computed as P=minC+B+H,applicable capP= \C+B+H,applicable cap\, where “applicable cap” is a hard ceiling triggered by a fundamental mismatch with the original problem. For example, P≤3P≤ 3 if the theorem assumes a central unresolved property, P≤7P≤ 7 if it proves only one direction of a characterization or omits a central quantifier, regime, or rate. C∈[0,4]C∈[0,4] measures closure of the paper-level target contract, B∈[0,3]B∈[0,3] measures improvement over the paper’s baseline, and H∈[0,3]H∈[0,3] measures how much of the central open burden is discharged. A score of P=10P=10 denotes exact target coverage. Regarding mathematical soundness, S=minM,D,AS= \M,D,A\ is a weakest-link assessment of intrinsic mathematical validity, verification of theorem-critical dependencies, and audit completeness. For technical novelty, N measures the originality and proof-critical role of the technical mechanism relative to prior work. Results show that two of nine subproblems are fully solved while the remaining seven subproblems are partially solved. For each subproblem, we report the most informative branches and state their progress relative to the corresponding source problem. Proof details are available at https://github.com/DechenZhang/VALG-ML-Theory-Agent/tree/main/case-studies/colt-2026. 4.1 How much overparametrization is needed for ALS in tensor decomposition? Open question. Let T=∑j=1raj⊗bj⊗cj∈ℝn×n×nT= _j=1^ra_j b_j c_j ^n× n× n where aj,bja_j,b_j and cjc_j are obtained by adding mutually independent (0,ρ2In/n)N(0,ρ^2I_n/n) perturbations, with ρ=1/poly(r)ρ=1/poly(r), to deterministic factor columns. Consider an optimization problem minimizing the least-squares objective minxi,yi,zi∈ℝn,i∈[k]‖T−∑i=1kxi⊗yi⊗zi‖F2. _x_i,y_i,z_i ^n,\ i∈[k] \|T- _i=1^kx_i y_i z_i \|_F^2. The open question of 3 asks what is the smallest value of k=k(r)k=k(r) so that alternating least squares (ALS) or another iterative algorithm such as GD converges from random initialization to the global optimum with high probability. 4.1.1 Subproblem 1: Upper Bound Open question. Does some iterative method, with r<k=o(r2)r<k=o(r^2) components, return in poly(n,r,log(1/ϵ))poly(n,r, (1/ε)) time a decomposition satisfying ‖T−∑i=1kxi⊗yi⊗zi‖F≤ϵ‖T‖F \|T- _i=1^kx_i y_i z_i \|_F≤ε\|T\|_F with high probability over the smoothed instance? Perspective 1. Formalized setting and preliminaries. Fix integers r≥3,nr≥ 3,n and let q∗=1/4096q_*=1/4096. For deterministic A¯,B¯,C¯∈ℝn×r A, B, C ^n× r with nonzero columns, define u¯j=a¯j/‖a¯j‖2 u_j= a_j/\| a_j\|_2 and cyclically v¯j,w¯j v_j, w_j; write U¯=[u¯j] U=[ u_j], V¯=[v¯j] V=[ v_j], W¯=[w¯j] W=[ w_j] and λ¯j=‖a¯j‖2‖b¯j‖2‖c¯j‖2 λ_j=\| a_j\|_2\| b_j\|_2\| c_j\|_2. For a unit-column matrix M=[mj]M=[m_j], write q(M)=max∑ℓ≠j|⟨mj,mℓ⟩|,q¯=maxM∈U¯,V¯,W¯q(M).q(M)= _j _ ≠ j| m_j,m_ |, q= _M∈\ U, V, W\q(M). Independently over columns and modes, draw gj(A),gj(B),gj(C)∼(0,ρ2In/n)g_j^(A),g_j^(B),g_j^(C) (0,ρ^2I_n/n), set aj=a¯j+gj(A)a_j= a_j+g_j^(A) and cyclically bj,cjb_j,c_j, and form T=∑j=1raj⊗bj⊗cj=∑j=1rλjuj⊗vj⊗wj,T= _j=1^ra_j b_j c_j= _j=1^r _ju_j v_j w_j, where U=[uj]U=[u_j], V=[vj]V=[v_j], W=[wj]W=[w_j] are the normalized realized factors and λj=‖aj‖2‖bj‖2‖cj‖2 _j=\|a_j\|_2\|b_j\|_2\|c_j\|_2. Put qreal=maxq(U),q(V),q(W)q_ real= \q(U),q(V),q(W)\ and Γ=maxjλj/minjλj = _j _j/ _j _j. The proposed procedure uses k=⌈Crankr5/3(logr)5/2⌉,Lburn=⌈Cburnlogr⌉,Lcert=⌈Ccertlogr⌉,τr=q∗2104r.k= C_ rankr^5/3( r)^5/2 , L_ burn= C_ burn r , L_ cert= C_ cert r , _r= q_*^210^4r. For each slot i and mode M∈U,V,WM∈\U,V,W\, draw mutually independent raw vectors ξi(M)∼(0,In) _i^(M) (0,I_n), independently of the smoothing, and initialize (pi0,qi0,si0)(p_i^0,q_i^0,s_i^0) by normalizing the corresponding raw triple. For h=(p,q,s)h=(p,q,s), it repeatedly makes the simultaneous old-state Jacobi commit (h)=(T(⋅,q,s)‖T(⋅,q,s)‖2,T(p,⋅,s)‖T(p,⋅,s)‖2,T(p,q,⋅)∥T(p,q,⋅)∥2).J(h)= ( T(·,q,s)\|T(·,q,s)\|_2, T(p,·,s)\|T(p,·,s)\|_2, T(p,q,·)\|T(p,q,·)\|_2 ). After LburnL_ burn commits it inspects the states through t=Lburn+Lcertt=L_ burn+L_ cert and stores the first one for which maxMminσ∈±1‖hM−σM(h)‖2≤τr _M _σ∈\± 1\\|h_M- _M(h)\|_2≤ _r. Only states with nonzero contractions and a valid certificate proceed. Certified triples are filtered at 0.850.85 of the largest score |⟨T,p⊗q⊗s⟩|| T,p q s |. Form a graph on the remaining triples, joining two vertices when their modewise absolute correlations are all at least 1−64q∗1-64q_*. The proposal is accepted only if this graph has exactly r connected components. The minimum-displacement representative of each component, with score as tie-break, gives an equal-norm best-scalar seed. For representative (pa,qa,sa)(p_a,q_a,s_a) with θa=⟨T,pa⊗qa⊗sa⟩≠0 _a= T,p_a q_a s_a ≠ 0, this seed is xa0=|θa|1/3pa,ya0=|θa|1/3qa,za0=sgn(θa)|θa|1/3sa.x_a^0=| _a|^1/3p_a, y_a^0=| _a|^1/3q_a, z_a^0=sgn( _a)| _a|^1/3s_a. A zero score aborts the run. Here ⊙ denotes the columnwise Khatri–Rao product. The three designs Z0⊙Y0Z^0 Y^0, Z0⊙X0Z^0 X^0, and Y0⊙X0Y^0 X^0 are frozen before any solve. Three Moore–Penrose least-squares landing proposals are computed from that same seed and committed synchronously. The run aborts if any committed active column is zero; otherwise the proposals are rebalanced once without changing their rank-one products. Cyclic U/V/WU/V/W ALS then updates the r active columns; the other k−rk-r columns stay zero. Each run stops at relative residual ϵε or after ⌈Cstoplog(8κ02/ϵ)⌉ C_ stop (8 _0^2/ε) sweeps. For raw proposal vectors ξi(M) _i^(M), set mU,j=ujm_U,j=u_j, mV,j=vjm_V,j=v_j, mW,j=wjm_W,j=w_j and Zij(M)=⟨mM,j,ξi(M)⟩Z_ij^(M)= m_M,j, _i^(M) and tr=(10/9)logrt_r= (10/9) r. The analysis uses the target-slot event ℰij=⋂Mtr≤|Zij(M)|≤tr+tr−1∩⋂ℓ≠j⋂M,N|Ziℓ(M)Ziℓ(N)|≤1918logr,E_ij= _M\t_r≤|Z_ij^(M)|≤ t_r+t_r^-1\∩\! _ ≠ j _\M,N\ \|Z_i ^(M)Z_i ^(N)|≤ 1918 r \, where M,NM,N range over distinct pairs from U,V,W\U,V,W\. Technical assumptions. Assumption 4.1 (Bounded deterministic base scales). Every base-column norm lies in [κ0−1,κ0][ _0^-1, _0], where 1≤κ0≤rdκ1≤ _0≤ r^d_κ for a fixed finite dκd_κ. Assumption 4.2 (Cumulative Gram interference). q¯≤q∗/4 q≤ q_*/4. Assumption 4.3 (Near-balanced deterministic weights). maxjλ¯j/minjλ¯j≤1+1/800 _j λ_j/ _j λ_j≤ 1+1/800. Assumption 4.4 (Independent Gaussian smoothing). The 3r3r perturbations have the independent laws above, with 0<ρ≤10<ρ≤ 1 and ρ−1≤rdρ^-1≤ r^d_ρ for a fixed finite dρd_ρ. Assumption 4.5 (Scale-aware smoothing and dimension margin). For δsm∈(0,1) _ sm∈(0,1), κ0ρ≤q∗128,r(κ0ρ+κ02ρ2)log(9r2/δsm)n≤q∗32. _0ρ≤ q_*128, r( _0ρ+ _0^2ρ^2) (9r^2/ _ sm)n≤ q_*32. Assumption 4.6 (Strictly subquadratic proposal rank). The displayed k satisfies r<k≤nr<k≤ n. Assumption 4.7 (Independent proposal and restart randomness). Conditional on the once-drawn tensor, proposal triples are independent across slots, modes, and completed runs, and independent of smoothing; restarts reuse the tensor but not proposal randomness. Assumption 4.8 (Accuracy and separate confidence levels). 0<ϵ,δsm,δinit<10<ε, _ sm, _ init<1, with the latter two controlling the smoothed instance and conditional restarts, respectively. Main theory. Theorem 4.1 (Conditional strictly subquadratic recovery). Universal positive choices of Crank,Cburn,Ccert,Cstop,CrepC_ rank,C_ burn,C_ cert,C_ stop,C_ rep make the following true under Assumptions 4.1–4.8. There is a smoothing event EsmE_ sm of probability at least 1−δsm1- _ sm on which every realized column has norm at least (2κ0)−1(2 _0)^-1, qreal q_ real ≤q∗, ≤ q_*, Γ ≤1.01, ≤ 1.01, λmin((V⊙W)⊤(V⊙W)) _ ((V W) (V W)) ≥1−q∗2, ≥ 1-q_*^2, λmin((U⊙W)⊤(U⊙W)) _ ((U W) (U W)) ≥1−q∗2, ≥ 1-q_*^2, λmin((U⊙V)⊤(U⊙V)) _ ((U V) (U V)) ≥1−q∗2. ≥ 1-q_*^2. Conditional on any fixed instance in EsmE_ sm, uniformly in i,ji,j, Prprop(ℰij)=Θ(r−5/3(logr)−3/2), _ prop(E_ij)= \! (r^-5/3( r)^-3/2 ), with universal comparison constants. Hence the displayed k=o(r2)k=o(r^2) gives one-run simultaneous target coverage with probability at least 26/2726/27. On coverage, certification, unlabeled clustering, synchronized landing, and cyclic refinement return at most k terms with relative Frobenius residual at most ϵε. With J=max1,⌈Creplog(1/δinit)⌉J= \1, C_ rep (1/ _ init) \ independent completed runs, conditional success is at least 1−δinit1- _ init, so joint success is at least (1−δsm)(1−δinit)(1- _ sm)(1- _ init). Every tape terminates, and the dense arithmetic work is polynomial in n,r,κ0,ρ−1,log(1/ϵ),log(1/δinit)n,r, _0,ρ^-1, (1/ε), (1/ _ init). Discussion. This is partial progress. It preserves the smoothed CP model, the strictly subquadratic rank k=Θ(r5/3(logr)5/2)k= (r^5/3( r)^5/2), arbitrary relative accuracy, polynomial time, and nested high-probability success. Its partiality comes from added bounded-scale, weak-interference, weight-balance, and smoothing/dimension assumptions. The chosen mechanism is a certified proposal, synchronized-landing, and cyclic-ALS pipeline with independent restarts. Technical role and remaining barrier. The source setting leaves two technical barriers. First, arbitrary base geometry can make the smoothed components indistinguishable and prevent the proposal estimates from remaining uniform across components. Second, independently proposed mode estimates do not automatically enter compatible target spans. Bounded scales and near-balanced weights control component magnitudes, weak interference separates components, and the smoothing/dimension margin preserves these properties after perturbation; together they close the proposal recurrences. Certification and synchronized landing then align the three modes before cyclic ALS refinement. The remaining problem is to prove the same rank, accuracy, running-time, and probability guarantees for arbitrary source-admissible base triples without the added structural assumptions. 4.1.2 Subproblem 2: Lower Bound Open question. Is there a universal c>0c>0 such that, for r<k≤r1+cr<k≤ r^1+c, ALS, gradient descent, or another iterative method converges with constant probability to a strictly positive objective value? Perspective 1. Formalized setting and preliminaries. Let r,n,kr,n,k be positive integers, let q>0q>0, and set ρ=r−qρ=r^-q. For arbitrary deterministic A¯,B¯,C¯∈ℝn×r A, B, C ^n× r, independently smooth their columns by (0,ρ2In/n)N(0,ρ^2I_n/n) to obtain T=∑j=1raj⊗bj⊗cj.T= _j=1^ra_j b_j c_j. For X,Y,Z∈ℝn×kX,Y,Z ^n× k, set S(X,Y,Z)=∑ixi⊗yi⊗ziS(X,Y,Z)= _ix_i y_i z_i and F(X,Y,Z)=12‖T−S(X,Y,Z)‖F2F(X,Y,Z)= 12\|T-S(X,Y,Z)\|_F^2. Here T(m)T_(m) is the mode-m matricization and ⊙ is the Khatri–Rao product. For each M∈cALS,cGDM∈\cALS,cGD\, draw an independent Gaussian triple GxM,GyM,GzMG_x^M,G_y^M,G_z^M with iid (0,1/n)N(0,1/n) entries. Let QM=orth(GxM)Q_M=orth(G_x^M), where orthorth is a fixed measurable choice of orthonormal basis for the column space, M=range(GxM)S_M=range(G_x^M), and ℋM=M⊗ℝn⊗ℝn,PℋM=(QMQM⊤)⊗In⊗In.H_M=S_M ^n ^n, P_H_M=(Q_MQ_M ) I_n I_n. The methods share T but have independent starts. The constrained sequential ALS method initializes at its Gaussian triple and, in X,Y,ZX,Y,Z order, uses Xt+1 X_t+1 =QcALSQcALS⊤T(1)Ktx((Ktx)⊤Ktx)†, =Q_ cALSQ_ cALS T_(1)K_t^x((K_t^x) K_t^x) , Ktx K_t^x =Zt⊙Yt, =Z_t Y_t, Yt+1 Y_t+1 =T(2)Kty((Kty)⊤Kty)†, =T_(2)K_t^y((K_t^y) K_t^y) , Kty K_t^y =Zt⊙Xt+1, =Z_t X_t+1, Zt+1 Z_t+1 =T(3)Ktz((Ktz)⊤Ktz)†, =T_(3)K_t^z((K_t^z) K_t^z) , Ktz K_t^z =Yt+1⊙Xt+1. =Y_t+1 X_t+1. Thus only XtX_t is constrained to its fixed initialization span. All three displayed updates are Moore–Penrose minimum-norm solves, including when a design Gram is singular. The constrained GD method writes Xt=QcGDCtX_t=Q_ cGDC_t and fQ(C,Y,Z)=F(QcGDC,Y,Z)f_Q(C,Y,Z)=F(Q_ cGDC,Y,Z). Initialize at (C0,Y0,Z0)=(QcGD⊤GxcGD,GycGD,GzcGD),(C_0,Y_0,Z_0)=(Q_ cGD G_x cGD,G_y cGD,G_z cGD), and, testing j=0,1,2,…j=0,1,2,… in increasing order, choose the first dyadic ηt=2−j _t=2^-j satisfying, for ut=(Ct,Yt,Zt)u_t=(C_t,Y_t,Z_t), fQ(ut−ηt∇fQ(ut))≤fQ(ut)−ηt2∥∇fQ(ut)∥F2,f_Q(u_t- _t∇ f_Q(u_t))≤ f_Q(u_t)- _t2\|∇ f_Q(u_t)\|_F^2, and take that step. Both methods iterate the displayed updates from their specified starts. Write StM=S(XtM,YtM,ZtM)S_t^M=S(X_t^M,Y_t^M,Z_t^M) and FM(t)=F(XtM,YtM,ZtM)F_M(t)=F(X_t^M,Y_t^M,Z_t^M). The gradient norm is the combined Frobenius norm of the C,Y,ZC,Y,Z blocks. Technical assumptions. Assumption 4.9 (Fixed ambient dimension). n≥8r5/4n≥ 8r^5/4. Assumption 4.10 (Superlinear algorithmic rank). r<k≤r5/4r<k≤ r^5/4; equivalently, the exponent is α=1/4α=1/4. Assumption 4.11 (Uniform arbitrary deterministic bases). The deterministic base triple is unrestricted, and the claim is pointwise uniform over all such triples. Assumption 4.12 (Independent Gaussian smoothing). q>0q>0 is fixed, ρ=r−qρ=r^-q, and the 3r3r smoothing vectors are mutually independent with covariance (ρ2/n)In(ρ^2/n)I_n. Assumption 4.13 (Shared target and independent starts). The two initialization triples are mutually independent and independent of smoothing, while both methods use the same realized T. Main theory. Theorem 4.2 (Fixed-span positive limiting objective). Under Assumptions 4.9–4.13, with probability at least 1/41/4 over smoothing and both starts, simultaneously for M∈cALS,cGDM∈\cALS,cGD\, ‖(I−PℋM)T‖F2≥34‖T‖F2,FM(t)≥38‖T‖F2for every t≥0,\|(I-P_H_M)T\|_F^2≥ 34\|T\|_F^2, F_M(t)≥ 38\|T\|_F^2 every t≥ 0, and FM(t)F_M(t) has a finite scalar limit satisfying limt→∞FM(t)≥38‖T‖F2. _t→∞F_M(t)≥ 38\|T\|_F^2. The statement holds for every admissible r,n,kr,n,k and is pointwise uniform in the deterministic base triple. Discussion. This is partial progress. It preserves arbitrary base factors, the smoothed tensor model, Gaussian initialization, every r<k≤r5/4r<k≤ r^5/4, and the goal of a strictly positive limiting loss with constant probability. The main change is algorithmic: cALS and cGD constrain one factor to its initialization span. The result also assumes n≥8r5/4n≥ 8r^5/4 and uses specified minimum-norm ALS and Armijo-GD updates. Technical role and remaining barrier. The source algorithms present a trajectory-control barrier: an unconstrained update can leave the initialization span, so the proof loses the fixed subspace used to obstruct exact recovery. Constraining the X factor keeps every represented tensor in the fixed space M⊗ℝn⊗ℝnS_M ^n ^n. With constant probability, the target has a nonzero component orthogonal to this space, which forces positive loss. The dimension condition gives k/n≤1/8k/n≤ 1/8 and hence a constant-probability orthogonal-residual witness, while the specified descent rules ensure that the loss converges. The remaining problem is to prove, under the same smoothed model, dimension condition, and rank window, the corresponding constant-probability positive-limit result for unconstrained sequential minimum-norm ALS and full-variable Armijo GD. Returning to the full source contract additionally requires removing or justifying the dimension restriction n≥8r5/4n≥ 8r^5/4. Perspective 2. Formalized setting and preliminaries. Fix κ≥1κ≥ 1, q>0q>0, and positive integers n,r,kn,r,k, and put ρ=r−qρ=r^-q. For deterministic A¯,B¯,C¯∈ℝn×r A, B, C ^n× r with nonzero columns, let A~,B~,C~ A, B, C be their column-normalized versions. Independently over j and modes, draw ξja,ξjb,ξjc∼(0,ρ2In/n) _j^a, _j^b, _j^c (0,ρ^2I_n/n), set aj=a¯j+ξjaa_j= a_j+ _j^a, bj=b¯j+ξjbb_j= b_j+ _j^b, and cj=c¯j+ξjcc_j= c_j+ _j^c, and form T=∑j=1raj⊗bj⊗cjT= _j=1^ra_j b_j c_j. For X,Y,Z∈ℝn×kX,Y,Z ^n× k, let T^(X,Y,Z)=∑i=1kxi⊗yi⊗zi,ℒ(X,Y,Z)=‖T−T^(X,Y,Z)‖F2. T(X,Y,Z)= _i=1^kx_i y_i z_i, (X,Y,Z)=\|T- T(X,Y,Z)\|_F^2. Write T^t=T^(Xt,Yt,Zt) T_t= T(X_t,Y_t,Z_t) and use the standard mode matricizations and Khatri–Rao product below. From an iid (0,1/n)N(0,1/n) initialization, compute the three minimum-norm least-squares candidates in parallel from the old iterate: Utx U_t^x =Zt⊙Yt, =Z_t Y_t, Xt+1ls X_t+1 ls =T(1)Utx((Utx)⊤Utx)†, =T_(1)U_t^x((U_t^x) U_t^x) , Uty U_t^y =Zt⊙Xt, =Z_t X_t, Yt+1ls Y_t+1 ls =T(2)Uty((Uty)⊤Uty)†, =T_(2)U_t^y((U_t^y) U_t^y) , Utz U_t^z =Yt⊙Xt, =Y_t X_t, Zt+1ls Z_t+1 ls =T(3)Utz((Utz)⊤Utz)†. =T_(3)U_t^z((U_t^z) U_t^z) . Set (Xt+1raw,Yt+1raw,Zt+1raw)(X_t+1 raw,Y_t+1 raw,Z_t+1 raw) to the componentwise averages of the old factors and these candidates. For each positive-norm component triple, replace all three norms by their geometric mean; if a norm is zero, replace the triple by (0,0,0)(0,0,0). This gauge preserves the represented tensor. The method is unconstrained half-relaxed parallel ALS. Let ΛA=(A¯⊤A¯)−1A¯⊤ _A=( A A)^-1 A , and define ΛB,ΛC _B, _C analogously and Q=ΛA⊗ΛB⊗ΛCQ= _A _B _C. Put pi,t=(ΛAxi,t)⊗(ΛByi,t)⊗(ΛCzi,t),Dr=∑j=1rej⊗3,Ct=∑i=1kpi,t,t=spanpi,t:i∈[k],p_i,t=( _Ax_i,t) ( _By_i,t) ( _Cz_i,t), D_r= _j=1^re_j 3, C_t= _i=1^kp_i,t, _t=span\p_i,t:i∈[k]\, Pt=ProjtP_t=Proj_S_t, Δ0=distF(Dr,0) _0=dist_F(D_r,S_0), and Eρ=QT−DrE_ρ=QT-D_r. These definitions give the exact identity Q(T−T^t)=Dr+Eρ−Ct,Ct∈t.Q(T- T_t)=D_r+E_ρ-C_t, C_t _t. The spaces tS_t evolve adaptively, and both coefficient and ambient tensor spaces use Frobenius geometry. For LP<δ/4L_P<δ/4 and ζ<δ/4ζ<δ/4, define 2(δ,LP,ζ,CT) C_2(δ,L_P,ζ,C_T) by four clauses: 1. Δ0≥δ‖Dr‖F=δr _0≥δ\|D_r\|_F=δ r; 2. ∑t≥0‖Pt+1−Pt‖op≤LP _t≥ 0\|P_t+1-P_t\|_ op≤ L_P; 3. ∑t≥0‖T^t+1−T^t‖F<∞ _t≥ 0\| T_t+1- T_t\|_F<∞; 4. ‖Eρ‖F≤ζ‖Dr‖F\|E_ρ\|_F≤ζ\|D_r\|_F and ‖T‖F≤CT‖Dr‖F\|T\|_F≤ C_T\|D_r\|_F, where CT=CT(κ,q)C_T=C_T(κ,q) is independent of r,n,kr,n,k and the base triple. The event 2 C_2 is an outcome-dependent certificate. Its role is transparent: the projector-path clause preserves the initial coefficient deficit at every time, distF(Dr,t)≥(δ−LP)‖Dr‖F,dist_F(D_r,S_t)≥(δ-L_P)\|D_r\|_F, while the same-target identity, the smoothing clause, and ‖Q‖op≤κ6\|Q\|_ op≤κ^6 give the all-time physical residual bound ‖T−T^t‖F≥δ−LP−ζκ6CT‖T‖F.\|T- T_t\|_F≥ δ-L_P-ζκ^6C_T\|T\|_F. The unsquared finite-variation clause makes (T^t)t( T_t)_t Cauchy, so the objective has a finite limit. Technical assumptions. Assumption 4.14 (Ambient dimension). n≥Cdim(κ,q)r4logrn≥ C_ dim(κ,q)r^4 r. Assumption 4.15 (Full superlinear rank window). r<k≤r5/4r<k≤ r^5/4. Assumption 4.16 (Well-conditioned deterministic bases). Every base-column norm and every singular value of each column-normalized base matrix lie in [κ−1,κ][κ^-1,κ]. Assumption 4.17 (Independent Gaussian smoothing). ρ=r−qρ=r^-q, and the 3r3r smoothing vectors have the independent Gaussian law above. Assumption 4.18 (Independent Gaussian initialization). All 3nk3nk initial factor entries are iid (0,1/n)N(0,1/n) and independent of smoothing. All probabilities refer to the joint law conditional on the deterministic base triple. Main theory. Theorem 4.3 (Conditional positive limiting loss). Under Assumptions 4.14–4.18, let r0∈ℕr_0 and Cdim,δ,LP,ζ,CT>0C_ dim,δ,L_P,ζ,C_T>0 depend only on (κ,q)(κ,q), with LP<δ/4L_P<δ/4 and ζ<δ/4ζ<δ/4, and define ϵ=(δ−LP−ζκ6CT)2>0.ε= ( δ-L_P-ζκ^6C_T )^2>0. For every r≥r0r≥ r_0, admissible n,kn,k and base triple, the displayed half-relaxed trajectory satisfies the deterministic event inclusion 2(δ,LP,ζ,CT)⊆limt→∞ℒ(Xt,Yt,Zt) exists and is finite,limt→∞ℒ(Xt,Yt,Zt)≥ϵ‖T‖F2. C_2(δ,L_P,ζ,C_T) \ array[]l _t→∞L(X_t,Y_t,Z_t) exists and is finite,\\[2.84526pt] _t→∞L(X_t,Y_t,Z_t)≥ε\|T\|_F^2 array \. The inclusion is pointwise under the joint smoothing-and-initialization law conditional on the base triple. In the separate deterministic zero-smoothing baseline with n≥rn≥ r and orthonormal base columns, QT=DrQT=D_r, Eρ=0E_ρ=0, ‖Q‖op=1\|Q\|_ op=1, and ‖T‖F=‖Dr‖F\|T\|_F=\|D_r\|_F; the first three applicable certificate clauses imply limt→∞ℒ(Xt,Yt,Zt)≥(δ−LP)2‖T‖F2. _t→∞L(X_t,Y_t,Z_t)≥(δ-L_P)^2\|T\|_F^2. Discussion. This is partial progress. It preserves the smoothed CP loss, Gaussian initialization, every r<k≤r5/4r<k≤ r^5/4, and the target of a positive relative limiting loss. The decisive change is that the conclusion is conditioned on the trajectory certificate 2(δ,LP,ζ,CT) C_2(δ,L_P,ζ,C_T), which requires an initial deficit, controlled motion of the adaptive span, controlled smoothing and scale, and finite tensor variation. The theorem also uses well-conditioned bases, a high-dimensional regime, and half-relaxed balanced parallel ALS. Technical role and remaining barrier. The source setting leaves two trajectory barriers: the adaptive coefficient span can rotate until it absorbs the initial deficit, and the represented tensor is not known to converge. The certificate controls projector motion to preserve the deficit, uses the smoothing and scale bounds to transfer that deficit to a physical residual, and imposes finite tensor variation to make the trajectory Cauchy. Well-conditioning controls the coefficient-to-tensor transfer, while the dimension regime and modified dynamics support the certificate conditions. These clauses yield a positive limiting loss. The immediate missing proposition is to prove that, for suitable constants depending only on (κ,q)(κ,q), Pr[2(δ,LP,ζ,CT)]≥p0(κ,q)>0 [ C_2(δ,L_P,ζ,C_T)]≥ p_0(κ,q)>0 uniformly over the admitted parameters and bases. Even this would establish only the restricted well-conditioned, high-dimensional, half-relaxed balanced parallel-ALS result. Returning to the source problem additionally requires a constant-probability positive-limit theorem without those geometric, dimensional, and algorithmic restrictions. Perspective 3. Formalized setting and preliminaries. Fix κ≥1κ≥ 1, q≥4q≥ 4, and positive integers n,r,kn,r,k, and put ρ=r−qρ=r^-q. For deterministic A¯,B¯,C¯∈ℝn×r A, B, C ^n× r with nonzero columns, write A¯∘,B¯∘,C¯∘ A , B , C for their column-normalized versions. Independently over j and modes, draw ξja,ξjb,ξjc∼(0,ρ2In/n) _j^a, _j^b, _j^c (0,ρ^2I_n/n) and set aj=a¯j+ξjaa_j= a_j+ _j^a, bj=b¯j+ξjbb_j= b_j+ _j^b, and cj=c¯j+ξjcc_j= c_j+ _j^c. With A=[aj]A=[a_j], B=[bj]B=[b_j], and C=[cj]C=[c_j], write T=∑j=1raj⊗bj⊗cj=(A⊗B⊗C)Dr,Dr=∑j=1rej⊗3,F(X,Y,Z)=‖T−∑i=1kxi⊗yi⊗zi‖F2.T= _j=1^ra_j b_j c_j=(A B C)D_r, D_r= _j=1^re_j 3, F(X,Y,Z)= \|T- _i=1^kx_i y_i z_i \|_F^2. Let G balance every component with three positive norms to their geometric mean, preserving its rank-one product, and leave a component with a zero factor unchanged. Apply G to an iid (0,1/n)N(0,1/n) initialization and after every simultaneous full-batch gradient step, where θt=(Xt,Yt,Zt) _t=(X_t,Y_t,Z_t): X~t+1=Xt−η∇XF(θt),Y~t+1=Yt−η∇YF(θt),Z~t+1=Zt−η∇ZF(θt),η=(nkr)−12. X_t+1=X_t-η _XF( _t), Y_t+1=Y_t-η _YF( _t), Z_t+1=Z_t-η _ZF( _t), η=(nkr)^-12. This defines balanced full-variable gradient descent. On the full-rank event, set αi,t=A†xi,t _i,t=A x_i,t and define βi,t,γi,t _i,t, _i,t analogously, and set α¯i,0=n/rαi,0 α_i,0= n/r\, _i,0, with the same convention for β¯i,0,γ¯i,0 β_i,0, γ_i,0. Put D^0=∑iαi,0⊗βi,0⊗γi,0,δ0=18, D_0= _i _i,0 _i,0 _i,0, _0= 18, and let 0 S_0 be the span, over i∈[k]i∈[k], of ℝr⊗βi,0⊗γi,0,αi,0⊗ℝr⊗γi,0,αi,0⊗βi,0⊗ℝr.R^r _i,0 _i,0, _i,0 ^r _i,0, _i,0 _i,0 ^r. Replacing the fixed coordinates by their barred versions leaves this tangent span unchanged. With κ1=2κ2 _1=2κ^2, define ℰinit_normE_ init\_norm as the intersection of: 1. ‖M‖op≤κ1\|M\|_ op≤ _1 and σmin(M)≥κ1−1 _ (M)≥ _1^-1 for M=A,B,CM=A,B,C; 2. all eigenvalues of the three normalized pair Grams [β¯i,0⊗γ¯i,0]i⊤[β¯i,0⊗γ¯i,0]i[ β_i,0 γ_i,0]_i [ β_i,0 γ_i,0]_i and its cyclic analogues lie in [r−20,r20][r^-20,r^20]; 3. some unit W0⟂0W_0 S_0 satisfies ⟨Dr−D^0,W0⟩F≥δ0‖Dr‖F D_r- D_0,W_0 _F≥ _0\|D_r\|_F; 4. maxi,m∈x,y,z‖mi,0‖2≤2 _i,m∈\x,y,z\\|m_i,0\|_2≤ 2. The normalized pair Grams equal (n/r)2(n/r)^2 times their raw counterparts. For θ=(X,Y,Z)θ=(X,Y,Z), define dbal(θ,θ′)2=‖X−X′‖F2+‖Y−Y′‖F2+‖Z−Z′‖F2,Epath=∑t≥0dbal(θt+1,θt),d_ bal(θ,θ )^2=\|X-X \|_F^2+\|Y-Y \|_F^2+\|Z-Z \|_F^2, E_ path= _t≥ 0d_ bal( _t+1, _t), and CCP(κ,R)=κ13(1+3R)C_ CP(κ,R)= _1^3(1+3R). The sole trajectory certificate is E⋆=min1,δ016CCP(κ,3),path=Epath≤E⋆.E_ = \1, _016C_ CP(κ,3) \, _ path=\E_ path≤ E_ \. Technical assumptions. Assumption 4.19 (Well-conditioned deterministic bases). Every base-column norm and every singular value of each column-normalized base matrix lie in [κ−1,κ][κ^-1,κ]. Assumption 4.20 (Smoothed dimension regime). q≥4q≥ 4 is fixed, r is sufficiently large, and n≥C(κ,q)r4logrn≥ C(κ,q)r^4 r. Assumption 4.21 (Universal superlinear rank window). r<k≤⌊r5/4⌋r<k≤ r^5/4 . Assumption 4.22 (Independent Gaussian smoothing). All smoothing vectors have the independent law (0,r−2qIn/n)N(0,r^-2qI_n/n) and are independent of initialization. Assumption 4.23 (Gaussian initialization). Before balancing, all entries of X0raw,Y0raw,Z0rawX_0 raw,Y_0 raw,Z_0 raw are iid (0,1/n)N(0,1/n). Assumption 4.24 (Fixed balanced gradient-descent protocol). The protocol uses the simultaneous full-batch update, step size η=(nkr)−12η=(nkr)^-12, and map G specified above. Main theory. Theorem 4.4 (Conditional positive-loss certificate). Under Assumptions 4.19–4.24, there are r0(κ,q)r_0(κ,q) and C(κ,q)C(κ,q) such that, uniformly over every r≥r0(κ,q),n≥C(κ,q)r4logr,r<k≤⌊r5/4⌋,r≥ r_0(κ,q), n≥ C(κ,q)r^4 r, r<k≤ r^5/4 , and every admissible deterministic base triple, Pr(ℰinit_norm)≥1−r−10. (E_ init\_norm)≥ 1-r^-10. With ϵ0(κ)=(1516δ0)2κ1−12>0, _0(κ)= ( 1516 _0 )^2 _1^-12>0, on ℰinit_norm∩pathE_ init\_norm _ path the balanced iterates converge in dbald_ bal to a finite θ∞ _∞ and limt→∞F(θt)=F(θ∞)≥ϵ0(κ)‖T‖F2>0. _t→∞F( _t)=F( _∞)≥ _0(κ)\|T\|_F^2>0. Consequently, if ℱ+F_+ is this convergence-and-positive-limit event, Pr(ℱ+)≥(1−r−10)Pr(path∣ℰinit_norm). (F_+)≥(1-r^-10) (C_ path _ init\_norm). Probabilities are under the joint smoothing-and-initialization law conditional on the deterministic base triple. Discussion. This is partial progress. It preserves the smoothed CP loss, Gaussian initialization, every r<k≤⌊r5/4⌋r<k≤ r^5/4 , simultaneous all-factor gradient steps, and the target of a positive relative limiting loss. The decisive added condition is the finite-path event pathC_ path. The analyzed dynamics additionally use well-conditioned bases, a high-dimensional regime, a tiny fixed step, and product-preserving balancing after every step. Technical role and remaining barrier. The source setting leaves a global trajectory barrier: a tiny step controls each update locally but does not bound the total motion, accumulated nonlinear error, or convergence of the iterates. The finite-path event bounds this total motion, keeps the balanced iterates in the region where the initial tangent-deficit witness survives, and controls the accumulated Taylor remainder. Well-conditioning transfers this witness to physical loss, while product-preserving balancing controls factor scales along the finite path. This yields convergence to a positive limiting loss. The immediate missing proposition is to prove that, for some p0(κ,q)>0p_0(κ,q)>0, Pr(path∣ℰinit_norm)≥p0(κ,q) (C_ path _ init\_norm)≥ p_0(κ,q) uniformly over the admitted parameters and bases. Even this would establish only the restricted well-conditioned, high-dimensional, tiny-step balanced method. Returning to the source problem additionally requires removing these geometric, dimensional, step-size, and balancing restrictions. 4.2 Is Interaction Necessary for Order-Optimal 1-bit Mean Estimation? Open question. Consider one-dimensional mean estimation over the nonparametric distribution family (k,λ,σ)=D:μ(D):=X∼D[X]∈[−λ,λ],X∼D|X−μ(D)|k≤σk,D(k,λ,σ)= \D:μ(D):=E_X D[X]∈[-λ,λ],\ E_X D|X-μ(D)|^k≤σ^k \, where k>1k>1 and λ≥σ>0λ≥σ>0 are known to the learner. A 1-bit communication protocol observes independent samples X1,…,Xn∼DX_1,...,X_n D only through binary messages Yt=Xt∈AtY_t= 1\X_t∈ A_t\, where At⊂ℝA_t is measurable. In a fully non-adaptive protocol, all sets A1,…,AnA_1,...,A_n are fixed before any messages are observed, possibly using public or private randomness. Threshold and interval queries correspond to AtA_t being a half-line or an interval, respectively. We say that a protocol is (ϵ,δ)(ε,δ)-accurate over (k,λ,σ)D(k,λ,σ) if its output μ μ satisfies supD∈(k,λ,σ)ℙ|μ^−μ(D)|>ϵ≤δ. _D (k,λ,σ)P\| μ-μ(D)|>ε\≤δ. The adaptive 1-bit minimax sample complexity is known: rk(λ,σ,ϵ,δ)=logλσ+σ2ϵ2log1δ,k>2,σ2ϵ2logσϵlog1δ,k=2,(σϵ)k/(k−1)log1δ,1<k<2.r_k(λ,σ,ε,δ)= λσ+ cases σ^2ε^2 1δ,&k>2,\\[4.49997pt] σ^2ε^2 σε 1δ,&k=2,\\[4.49997pt] ( σε )^k/(k-1) 1δ,&1<k<2. cases The open question of 25 asks whether fully non-adaptive arbitrary 1-bit quantizers can achieve the adaptive minimax rate? 4.2.1 Subproblem 1: Order-Optimal Non-Adaptive 1-Bit Mean Estimation Open question. Fix k>1k>1. Do there exist constants ck,Ck>0c_k,C_k>0 such that, for all λ≥σ>0λ≥σ>0, all 0<ϵ≤ckσ0<ε≤ c_kσ, and all δ∈(0,1/2)δ∈(0,1/2), there is a fully non-adaptive 1-bit protocol that is (ϵ,δ)(ε,δ)-accurate over (k,λ,σ)D(k,λ,σ) using at most n≤Ckrk(λ,σ,ϵ,δ)n≤ C_kr_k(λ,σ,ε,δ) samples? Perspective 1. Formalized setting and preliminaries. Fix k>1k>1, known λ≥σ>0λ≥σ>0, accuracy ϵ>0ε>0, and confidence δ∈(0,1/2)δ∈(0,1/2). For a law D on ℝR, define (k,λ,σ):=D:μ(D)=DX∈[−λ,λ],D|X−μ(D)|k≤σk.D(k,λ,σ):= \D:\ μ(D)=E_DX∈[-λ,λ], _D|X-μ(D)|^k≤σ^k \. This is the unrestricted central-k-moment class. The target sample complexity is rk(λ,σ,ϵ,δ):=logλσ+σ2ϵ2log1δ,k>2,σ2ϵ2logσϵlog1δ,k=2,(σϵ)k/(k−1)log1δ,1<k<2.r_k(λ,σ,ε,δ):= λσ+ cases σ^2ε^2 1δ,&k>2,\\[4.49997pt] σ^2ε^2 σε 1δ,&k=2,\\[4.49997pt] ( σε )^k/(k-1) 1δ,&1<k<2. cases Split the indices in advance into localization and refinement blocks. Localization uses the fully non-adaptive balanced-code construction of 26 at confidence δ/4δ/4: it uses precommitted Borel union-of-cell queries and returns a center c defined for every transcript. Write NlocN_ loc for the number of localization queries. For finite constants Lk,Cloc,kL_k,C_ loc,k depending only on k, its theorem-level contract is Pr|c−μ(D)|≤Lkσ≥1−δ4,Nloc≤Cloc,k(1+logλσ+log4δ). \|c-μ(D)|≤ L_kσ\≥ 1- δ4, N_ loc≤ C_ loc,k (1+ λσ+ 4δ ). The refinement bank is also fixed before communication. For k-only constants γk∈(0,1) _k∈(0,1) and bk≥1b_k≥ 1, set h0=γkϵ,H∗=bkσ(σϵ)1/(k−1),J=⌈log2H∗h0⌉,hj=2jh0.h_0= _kε, H_*=b_kσ ( σε )^1/(k-1), J= _2 H_*h_0 , h_j=2^jh_0. For 0≤j<J0≤ j<J, give the fine levels hj≤σh_j≤σ weights hj/σh_j/σ and the coarse levels hj>σh_j>σ weights (hj/σ)2−k(h_j/σ)^2-k; normalize within each nonempty group and give each nonempty group equal total mass. Denote the resulting level probabilities by pjp_j. With =0,1/4,1/2,3/4S=\0,1/4,1/2,3/4\, define Qj,a(x)=ahj+hj⌊x−ahjhj⌋,Fj,a,b=Qj,a−Qj+1,b.Q_j,a(x)=ah_j+h_j x-ah_jh_j , F_j,a,b=Q_j,a-Q_j+1,b. Independently for every refinement sample i, draw Li∼(p0,…,pJ−1)L_i (p_0,…,p_J-1), Ai,Bi∼iidUnif()A_i,B_i iid Unif(S), and Ui∼Unif[−1,2]U_i Unif[-1,2], all before any response, and transmit Yi=FLi,Ai,Bi(Xi)hLi≥Ui.Y_i=1\! \ F_L_i,A_i,B_i(X_i)h_L_i≥ U_i \. At decoding time, choose the unique aj(c)∈a_j(c) such that c/hj−aj(c)∈[3/8,5/8)\c/h_j-a_j(c)\∈[3/8,5/8), and form Zi(c)=48hLipLi(Ai,Bi)=(aLi(c),aLi+1(c))×[Yi−FLi,Ai,Bi(c)hLi≥Ui]. splitZ_i(c)&= 48h_L_ip_L_i1\(A_i,B_i)=(a_L_i(c),a_L_i+1(c))\\\[-1.99997pt] & × [Y_i-1\! \ F_L_i,A_i,B_i(c)h_L_i≥ U_i \ ]. split Choose a positive integer s and an odd positive integer q, both as functions of the public parameter tuple, partition the refinement indices in advance into q blocks of size s, and output μ^=c+median1≤g≤q(1s∑i∈GgZi(c)). μ=c+median_1≤ g≤ q ( 1s _i∈ G_gZ_i(c) ). Localization supplies the decoder-side shift, centering, and importance weights, while all queries remain precommitted. Technical assumptions. Assumption 4.25 (Parameter domain). The exponent k>1k>1 is fixed and known, λ≥σ>0λ≥σ>0 are known, δ∈(0,1/2)δ∈(0,1/2), and 0<ϵ≤ckσ0<ε≤ c_kσ, where ck∈(0,1)c_k∈(0,1) depends only on k. Assumption 4.26 (Unrestricted central moment class). The samples have a common law D∈(k,λ,σ)D (k,λ,σ). Assumption 4.27 (Independent samples and precommitted seeds). All samples are independent with common law D. The sample split, median blocks, localization randomness, and every refinement seed are mutually independent where appropriate and fixed before the first response bit. Main theory. Theorem 4.5 (Order-optimal noninteractive one-bit mean estimation). Under Assumptions 4.25– 4.27, one may take ck=e−1c_k=e^-1, γk=1/8 _k=1/8, choose bkb_k as a function only of k, and choose s and the odd q as functions of the public tuple (k,λ,σ,ϵ,δ)(k,λ,σ,ε,δ). The resulting Borel query bank is fixed before the first response, uses exactly one bit from each of n=Nloc+qsn=N_ loc+qs independent samples, and satisfies, for a finite CkC_k depending only on k, n≤Ckrk(λ,σ,ϵ,δ),supD∈(k,λ,σ)PrD,protocol|μ^−μ(D)|>ϵ≤δ.n≤ C_kr_k(λ,σ,ε,δ), _D (k,λ,σ) _D,\,protocol\| μ-μ(D)|>ε\≤δ. The probability is unconditional over both sample blocks and all protocol randomness, the horizon is deterministic, and the loss is absolute error on ℝR. Discussion. This theorem matches the source problem’s full scope over the unrestricted central-k-moment class. Together with the known one-bit minimax lower bound, its rate is order-optimal. Both query banks are precommitted, and localization is a decoder-side operation. Perspective 3. Formalized setting and preliminaries. For k>1k>1 and known λ≥σ>0λ≥σ>0, define (k,λ,σ)=D:μ(D)=DX∈[−λ,λ],D|X−μ(D)|k≤σk.D(k,λ,σ)=\D:μ(D)=E_DX∈[-λ,λ],\ E_D|X-μ(D)|^k≤σ^k\. This is the unrestricted central-k-moment class. Its three-regime target rate is rk(λ,σ,ϵ,δ)=logλσ+σ2ϵ2log1δ,k>2,σ2ϵ2logσϵlog1δ,k=2,(σϵ)k/(k−1)log1δ,1<k<2.r_k(λ,σ,ε,δ)= λσ+ cases σ^2ε^2 1δ,&k>2,\\[3.99994pt] σ^2ε^2 σε 1δ,&k=2,\\[3.99994pt] ( σε )^k/(k-1) 1δ,&1<k<2. cases Split the samples in advance into localization and refinement blocks. The first uses the coding-based fully non-adaptive localizer of 26 at confidence δ/4δ/4. Let RlocR_ loc be a public localization seed, independent of all samples and fixed before any response bit. The localizer uses precommitted Borel queries ℬi(Rloc)B_i(R_ loc) and an always-defined decoder output c=loc(Rloc,(Xi∈ℬi(Rloc))i∈Iloc).c= Dec_ loc (R_ loc,(1\X_i _i(R_ loc)\)_i∈ I_ loc ). For finite constants Lk,Cloc,kL_k,C_ loc,k depending only on k, the localizer satisfies Pr|c−μ(D)|≤Lkσ≥1−δ4,Nloc:=|Iloc|≤Cloc,k(1+logλσ+log4δ). \|c-μ(D)|≤ L_kσ\≥ 1- δ4, N_ loc:=|I_ loc|≤ C_ loc,k (1+ λσ+ 4δ ). For k-only ak,bk>0a_k,b_k>0, let h0 h_0 =akσ, =a_kσ, H∗ H_* =bkσ(σ/ϵ)1/(k−1), =b_kσ(σ/ε)^1/(k-1), S S =⌈log2(H∗/h0)⌉, = _2(H_*/h_0) , hs h_s =2sh0, =2^sh_0, ps p_s =hs2−kZS, = h_s^2-kZ_S, ZS Z_S =∑s=0Shs2−k. = _s=0^Sh_s^2-k. On the dyadic grid, set Ps,j=[jhs,(j+1)hs)P_s,j=[jh_s,(j+1)h_s), ms,j=(j+1/2)hsm_s,j=(j+1/2)h_s, and Js,j=Ps,j−1∪Ps,j∪Ps,j+1J_s,j=P_s,j-1∪ P_s,j∪ P_s,j+1. Define the rings ℛ0,j=J0,j,ℛs,j,b=Js,j∖Js−1,2j+b(s≥1),R_0,j=J_0,j, _s,j,b=J_s,j J_s-1,2j+b (s≥ 1), and color indices by s,ℓ=j:j≡ℓ(mod4)J_s, =\j:j≡ 4\. Half-open cells fix all boundary ties. For each refinement sample i, independently precommit Li∼(p0,…,pS)L_i (p_0,…,p_S), Ci∼Unif0,1,2,3C_i Unif\0,1,2,3\, Ui∼Unif[−1,1]U_i Unif[-1,1], and a countable independent Rademacher mask (ρi,s,j)( _i,s,j). If Li=s≥1L_i=s≥ 1, also precommit independent Ti∼Unifcoord,massT_i Unif\coord,mass\ and Bi∼Unif0,1B_i Unif\0,1\; at s=0s=0, take Ti=coordT_i=coord. With ψs,j,coord(x)=(x−ms,j)/(2hs) _s,j,coord(x)=(x-m_s,j)/(2h_s) and ψs,j,mass(x)=1 _s,j,mass(x)=1, define Fi(x)=∑j∈0,Ciρi,0,jx−m0,j2h0ℛ0,j(x),Li=0,∑j∈s,Ciρi,s,jψs,j,Ti(x)ℛs,j,Bi(x),Li=s≥1.F_i(x)= cases _j _0,C_i _i,0,j x-m_0,j2h_01_R_0,j(x),&L_i=0,\\[8.99994pt] _j _s,C_i _i,s,j _s,j,T_i(x)1_R_s,j,B_i(x),&L_i=s≥ 1. cases Each refinement sample transmits the single bit Yi=Fi(Xi)≥UiY_i=1\F_i(X_i)≥ U_i\. The decoder computes Yi0=0≥UiY_i^0=1\0≥ U_i\ and ΔYi=Yi−Yi0 Y_i=Y_i-Y_i^0. After the complete transcript arrives, choose j0(c)=minargminj∈ℤ|c−m0,j|,m0(c):=m0,j0(c),j_0(c)= *argmin_j |c-m_0,j|, m_0(c):=m_0,j_0(c), and set for s≥1s≥ 1 js=⌊j0(c)/2s⌋,bs=js−1−2js,ms=ms,js,ds=ms−m0(c),j_s= j_0(c)/2^s , b_s=j_s-1-2j_s, m_s=m_s,j_s, d_s=m_s-m_0(c), with κs=jsmod4 _s=j_s 4. The decoder retains and reweights the precommitted bits through Wi(c)=16h0p0Ci=κ0ρi,0,j0(c)ΔYi,Li=0,16psCi=κs,Bi=bsρi,s,js[4hsTi=coord+2dsTi=mass]ΔYi,Li=s≥1.W_i(c)= cases 16h_0p_01\C_i= _0\ _i,0,j_0(c) Y_i,&L_i=0,\\[8.99994pt] 16p_s1\C_i= _s,B_i=b_s\ _i,s,j_s [4h_s1\T_i=coord\+2d_s1\T_i=mass\ ] Y_i,&L_i=s≥ 1. cases Finally, for k-only αk,βk>0 _k, _k>0, preassign Gδ=2⌈αklog8δ⌉+1,Bref=⌈βkσkZSϵ2⌉,G_δ=2 _k 8δ +1, B_ ref= _k σ^kZ_Sε^2 , equal-size median blocks and output μ^=m0(c)+median1≤g≤Gδ(1Bref∑i∈GgWi(c)). μ=m_0(c)+median_1≤ g≤ G_δ ( 1B_ ref _i∈ G_gW_i(c) ). Localization selects the reconstruction path in the decoder, while all queries remain precommitted. Technical assumptions. Assumption 4.28 (Parameter domain). k>1k>1 is fixed and known, λ≥σ>0λ≥σ>0 are known, δ∈(0,1/2)δ∈(0,1/2), and 0<ϵ≤ckσ0<ε≤ c_kσ, for a positive k-only constant ck<1c_k<1. Assumption 4.29 (Unrestricted central-moment class). The common law belongs to the unrestricted class (k,λ,σ)D(k,λ,σ). Assumption 4.30 (Independent observations and seeds). Both sample blocks are i.i.d. from D. All localization and refinement seeds are mutually independent where appropriate and independent of the observations. Assumption 4.31 (Precommitted protocol). The split, all seeds and masks, and the median blocks are fixed before any bit is observed. Every query is Borel and independent of earlier messages. The localization output enters the decoder after collection of the full transcript. Main theory. Theorem 4.6 (Order-optimal fully non-adaptive one-bit mean estimation). Under Assumptions 4.28– 4.31, for every fixed k>1k>1 there are k-only constants ck,Ck,ak,bk,αk,βk>0c_k,C_k,a_k,b_k, _k, _k>0 such that the protocol above is well defined and, for all admissible public parameters, uses one bit per independent sample at the deterministic horizon n=Nloc+GδBrefn=N_ loc+G_δB_ ref with n≤Ckrk(λ,σ,ϵ,δ),supD∈(k,λ,σ)PrD,protocol|μ^−μ(D)|>ϵ≤δ.n≤ C_kr_k(λ,σ,ε,δ), _D (k,λ,σ) _D,\,protocol\| μ-μ(D)|>ε\≤δ. The guarantee is unconditional over all observations and protocol randomness, and uses absolute error on ℝR. It retains the exact three regimes displayed above, including the single log(σ/ϵ) (σ/ε) factor at k=2k=2, with all constants depending only on k. Discussion. This theorem matches the source problem’s full scope over the unrestricted moment class. Together with the known one-bit minimax lower bound, its rate is order-optimal. The masked multiscale bank is fully precommitted, and localization selects the reconstruction path in the decoder. 4.3 Is the Power of Deep Learning over Linear Models Inherently Distribution Dependent? Open question. 6 defined the dimension complexity dc(ℋ)dc(H) of a binary hypothesis class ℋ⊆±1H \± 1\^X as the smallest dimension d s.t. there exists a feature map φ:→ℝd :X ^d allowing linear representation of ℋH (i.e. s.t. ∀h∈ℋ∃w∈ℝd∀xh(x)=sign(⟨w,φ(x)⟩) _h _w ^d _xh(x)=sign( w, (x) )). Using dimension complexity (dc(ℋ)dc(H)) to measure the smallest shared feature dimension in which a hypothesis class is linearly realizable, the open question of 15 asks whether distribution-independent SQ learning implies low dimension complexity, and whether anything learnable with (S)GD on a (benign) neural network under any input distribution is also learnable with a linear model. 4.3.1 Subproblem 1: Learning with SGD over Neural Networks Open question. Is there a constant C such that for all ℋ⊆±1H \± 1\^X over =±1nX=\± 1\^n, and ϵ<1/4ε<1/4, if there exists a fully connected ReLU network with S parameters in total, stepsize η and number of steps T, such that for every input distribution D, every h∗∈ℋh^* , SGD yields expected error ℒ,h∗(h^)≤ϵEL_D,h^*( h)≤ε (expectation over the initialization and SGD sampling), then dc(ℋ)≤C⋅TSdc(H)≤ C· TS. Perspective 3. Formalized setting and preliminaries. Fix n,m,T≥1n,m,T≥ 1, η>0η>0, and ε≥0 ≥ 0. Let =−1,+1nX=\-1,+1\^n, ℋ⊆−1,+1H \-1,+1\^X, and fix a tie label s0∈−1,+1s_0∈\-1,+1\. Write signs0(z)=sign(z)sign_s_0(z)=sign(z) for z≠0z≠ 0 and signs0(0)=s0sign_s_0(0)=s_0, and define the strict error of a score g by ℒ,h(g)=Prx∼signs0(g(x))h(x)<0.L_D,h(g)= _x \sign_s_0(g(x))h(x)<0\. Consider the coordinatewise ReLU activation σ(z)=max0,zσ(z)= \0,z\ and the bias-free depth-two ReLU network fa,W(x)=a⊤σ(Wx),W∈ℝm×n,a∈ℝm,S=m(n+1),f_a,W(x)=a σ(Wx), W ^m× n, a ^m, S=m(n+1), with both layers trainable. Initialize independently with Wji(0)∼(0,1/n)W_ji^(0) (0,1/n) and aj(0)∼(0,1/m)a_j^(0) (0,1/m). Given fresh x(t)∼x^(t) , run T≥1T≥ 1 one-sample, all-layer SGD steps with fixed stepsize η>0η>0 and logistic loss ℓ(z)=log(1+e−z) (z)= (1+e^-z). Fix κkink∈[0,1] _ kink∈[0,1] once and use the ReLU derivative σκkink′(z)=z>0+κkinkz=0σ _ _ kink(z)=1\z>0\+ _ kink1\z=0\ in every gradient, so the SGD recursion is defined also at zero preactivations: (a(t+1),W(t+1))=(a(t),W(t))−η∇(a,W)ℓ(h(x(t))fa(t),W(t)(x(t))).(a^(t+1),W^(t+1))=(a^(t),W^(t))-η _(a,W) \! (h(x^(t))f_a^(t),W^(t)(x^(t)) ). The returned score is Gω(x)=∑t=⌈T/2⌉Tfa(t),W(t)(x),G_ω(x)= _t= T/2 ^Tf_a^(t),W^(t)(x), where ω includes initialization and all SGD samples. The deterministic dimension complexity dc(ℋ)dc(H) is the least dimension of one feature map that exactly represents every h∈ℋh by a tie-resolved homogeneous halfspace. Its confident variant dc1/2(ℋ)dc^1/2(H) is the least d for which a feature-map law P, chosen before (,h)(D,h), satisfies Prφ∼[infw∈ℝdPrx∼signs0(⟨w,φ(x)⟩)h(x)<0=0]≥12 _ \! [ _w ^d _x \sign_s_0( w, (x) )h(x)<0\=0 ]≥ 12 for every D and h. Let φid(x)=x∈ℝn _ id(x)=x ^n. Technical assumptions. Assumption 4.32 (Antipodally odd target class). Every h∈ℋh satisfies h(−x)=−h(x)h(-x)=-h(x) for all x∈x . Assumption 4.33 (Strict high-accuracy regime). The accuracy obeys the strict inequality 2ε<1/(n+1)2 <1/(n+1). Assumption 4.34 (Universal source success). The width, stepsize, and horizon are fixed before the distribution and target, and for every D and h∈ℋh , ω[ℒ,h(Gω)]≤ε,E_ω [L_D,h(G_ω) ]≤ , where expectation is joint over the independent Gaussian initialization and fresh one-sample SGD draws. Main theory. Theorem 4.7 (Exact identity representation in the odd high-accuracy regime). Under Assumptions 4.32, 4.33, and 4.34, the identity map exactly represents the class: ∀h∈ℋ∃wh∈ℝn∀x∈,signs0(⟨wh,x⟩)=h(x).∀ h \ ∃ w_h ^n\ ∀ x , _s_0( w_h,x )=h(x). Hence the distribution- and target-independent law id=δφidP_ id= _ _ id succeeds with probability one for every (,h)(D,h), and dc1/2(ℋ)≤dc(ℋ)≤n≤S≤TS.dc^1/2(H) (H)≤ n≤ S≤ TS. Discussion. This is partial progress. It preserves the Boolean domain, distribution-independent learner parameters, Gaussian initialization, and all-layer SGD. It differs from the source problem in three essential ways: (i) the network is bias-free and has depth two; (i) every target is antipodally odd; (i) the accuracy satisfies 2ε<1/(n+1)2 <1/(n+1). Technical role and remaining barrier. Under the source setting, the proof faces three technical barriers. First, the antisymmetric part of a general deep ReLU score can remain nonlinear, so it does not directly define a shared linear feature map. Second, an arbitrary target may assign incompatible labels to antipodal inputs, blocking the antipodal reduction. Third, the source condition ε<1/4 <1/4 is too weak to make a finite infeasibility witness contradict the learner guarantee. The added restrictions resolve these barriers one by one: the bias-free depth-two architecture and the ReLU identity σ(z)−σ(−z)=zσ(z)-σ(-z)=z linearize the antisymmetric score; target oddness aligns the labels on antipodal pairs; and 2ε<1/(n+1)2 <1/(n+1) supplies the strict finite-witness gap. Together they yield an exact representation by the identity features. The remaining problem is to obtain an O(TS)O(TS) common linear representation under the source assumptions, without these three restrictions. Perspective 1. Formalized setting and preliminaries. Let n be a positive integer, set =−1,+1nX=\-1,+1\^n, and let ℋ⊆−1,+1H \-1,+1\^X. Write ℕ0=0,1,2,…N_0=\0,1,2,…\ and [r]=1,…,r[r]=\1,…,r\ for every positive integer r. Fix the source tie label s0∈−1,+1s_0∈\-1,+1\, and define signs0(z)=+1,z>0,−1,z<0,s0,z=0.sign_s_0(z)= cases+1,&z>0,\\ -1,&z<0,\\ s_0,&z=0. cases Set R,h(w,φ):=Prx∼signs0(⟨w,φ(x)⟩)h(x)<0.R_D,h(w, ):= _x \sign_s_0( w, (x) )h(x)<0\. For α≥0α≥ 0, define dcα(ℋ):=mind∈ℕ0:∃∀h∈ℋ,φ∼[infw∈ℝdR,h(w,φ)]≤α,dc_α(H):= \d _0:\ \ \ ∀ h , _ [ _w ^dR_D,h(w, ) ]≤α \, where the law P is selected before (,h)(D,h). Consider a bias-free, fully connected ReLU network of positive integer depth L. Its widths n0=n,n1,…,nL−1,nL=1n_0=n,n_1,…,n_L-1,n_L=1 are positive integers, and its parameter count is S=∑ℓ=1Lnℓnℓ−1S= _ =1^Ln_ n_ -1. With z0=xz_0=x, uℓ=θℓzℓ−1u_ = _ z_ -1, zℓ=max0,uℓz_ = \0,u_ \ for ℓ<L <L, and fθ=θLzL−1f_θ= _Lz_L-1, initialize independently with (θℓ(0))jk∼(0,1/nℓ−1).( _ ^(0))_jk (0,1/n_ -1). Fix a ReLU-kink selector κ∈[0,1]κ∈[0,1]: derivatives at positive, negative, and zero preactivations are 11, 00, and κ, respectively. For fresh x(t)∼x^(t) , run the exact all-layer recursion θ(t+1)=θ(t)−η∇θ(κ)ℓ(h(x(t))fθ(t)(x(t))),ℓ(a)=log(1+e−a),θ^(t+1)=θ^(t)-η _θ^(κ) \! (h(x^(t))f_θ^(t)(x^(t)) ), (a)= (1+e^-a), and return the tie-resolved latter-half score A(x)=∑t=⌈T/2⌉Tfθ(t)(x)A(x)= _t= T/2 ^Tf_θ^(t)(x). For r≥0r≥ 0, let B∞(θ(0),r)=θ:‖θ−θ(0)‖∞≤rB_∞(θ^(0),r)=\θ:\|θ-θ^(0)\|_∞≤ r\, and define Mr(θ(0))=+∞,L=1,infθ∈B∞(θ(0),r),x∈,1≤ℓ<L,j∈[nℓ]|uℓ,j(θ,x)|,L≥2,M_r(θ^(0))= cases+∞,&L=1,\\ _ subarraycθ∈ B_∞(θ^(0),r),\ x ,\\ 1≤ <L,\ j∈[n_ ] subarray|u_ ,j(θ,x)|,&L≥ 2, cases Gr(θ(0))=supθ∈B∞(θ(0),r),x∈,y∈−1,+1‖∇θ(κ)ℓ(yfθ(x))‖∞,Er=Mr>0,ηTGr≤r.G_r(θ^(0))= _ subarraycθ∈ B_∞(θ^(0),r),\ x ,\\ y∈\-1,+1\ subarray\| _θ^(κ) (yf_θ(x))\|_∞, E_r=\M_r>0,\ η TG_r≤ r\. This event depends only on initialization and worst-case quantities over the fixed ball. Finally, for paths p=(i0,…,iL−1)∈∏ℓ=0L−1[nℓ]p=(i_0,…,i_L-1)∈ _ =0^L-1[n_ ], define [φθ(0)(x)]p=xi0∏ℓ=1L−1uℓ,iℓ(θ(0),x)>0,dpath=∏ℓ=0L−1nℓ.[ _θ^(0)(x)]_p=x_i_0 _ =1^L-11\u_ ,i_ (θ^(0),x)>0\, d_ path= _ =0^L-1n_ . Let gateP_ gate be the unconditional law of this map under Gaussian initialization, defined on both ErE_r and ErcE_r^c. Technical assumptions. Assumption 4.35 (Fixed source witnesses and regime). 0≤ε<1/40≤ <1/4, T is a positive integer, and η>0η>0. For the given (n,ℋ,ε)(n,H, ), the architecture, S,η,TS,η,T, and the fixed tie and kink conventions are selected once before every (,h)(D,h). Assumption 4.36 (Universal expected-error SGD premise). For every distribution D on X and every h∈ℋh , the strict classification error of the prescribed latter-half predictor satisfies θ(0),x(0),…,x(T−1)[Prx∼signs0(A(x))h(x)<0]≤ε.E_θ^(0),x^(0),…,x^(T-1) [ _x \sign_s_0(A(x))h(x)<0\ ]≤ . Assumption 4.37 (Fixed constant depth). A universal positive integer L0L_0, independent of all problem and learner parameters, satisfies 1≤L≤L01≤ L≤ L_0. Widths are arbitrary and all layers remain trainable. Assumption 4.38 (Static robust initialization tube). Deterministic r>0r>0 and 0≤δ0≤ε0≤ _0≤ are fixed before initialization, distribution, target, and SGD samples, and Prθ(0)(Er)≥1−δ0. _θ^(0)(E_r)≥ 1- _0. This initialization-only event is defined by worst-case quantities over the fixed ball. Trajectory containment, gate stability, and the path representation are derived from ErE_r. Main theory. Theorem 4.8 (Conditional polynomial probabilistic dimension). Under Assumptions 4.35, 4.36, 4.37, and 4.38, the single unconditional law gateP_ gate, chosen before every distribution and target, satisfies for all D and h∈ℋh φ∼gate[infw∈ℝdpathR,h(w,φ)]≤ε+δ0.E_ _ gate [ _w ^d_ pathR_D,h(w, ) ]≤ + _0. Consequently, dcε+δ0(ℋ)≤dpath≤SL≤SL0,dc2ε(ℋ)≤SL0.dc_ + _0(H)≤ d_ path≤ S^L≤ S^L_0, _2 (H)≤ S^L_0. The learner premise averages over initialization and the fixed finite SGD horizon; the tube premise is an initialization probability; and the conclusion averages over the unconditional feature-map law. Discussion. This is partial progress. It preserves one Gaussian-initialized ReLU learner, finite-horizon all-layer SGD, and uniform expected error over distributions and targets. It differs from the source problem in four ways: (i) the initialization must satisfy a robust-tube condition with high probability; (i) the network depth is bounded by a constant L0L_0; (i) the network is bias-free; (iv) the target is weakened to randomized approximate dimension dcε+δ0(ℋ)≤SL0dc_ + _0(H)≤ S^L_0. Technical role and remaining barrier. The source setting leaves three technical barriers. Instance-dependent SGD can change hidden gates, so trajectories need not share a fixed feature map; unrestricted depth can make the number of path features too large; and bad initializations cannot be discarded when the target is deterministic and exact. The robust tube freezes the gates, the depth cap bounds the path-feature dimension, and the bias-free architecture supports the displayed homogeneous path-feature map; the randomized approximate target absorbs the bad-seed event. These devices give a polynomial feature bound, but not the source’s exact linear O(TS)O(TS) bound. The remaining problem is to construct that common representation without the tube, depth cap, bias-free restriction, or target relaxation. 4.3.2 Subproblem 2: Statistical Query Learning A τ−τ-statistical query (SQ) oracle for input distribution D and target h∗h^*, on input query q:×±1→[−1,1]q:X×\± 1\→[-1,1] and tolerance τ returns an arbitrary value v such that |v−x∼q(x,h∗(x))|≤τ.|v-E_x q(x,h^*(x))|≤τ. A (randomized) (m,τ)−(m,τ)-statistical query (SQ) algorithm operates by making a sequence of m queries to a τ−τ-SQ oracle where each query can depend on all previous responses and can be selected at random, and then returns a predictor h^:→±1. h:X→\± 1\. Open question. Is there a constant C such that for every class ℋ⊆±1H \± 1\^X, over any domain X, and any ϵ<1/4ε<1/4, if there exists an (m,τ)−(m,τ)-SQ algorithm s.t. for every input distribution D and every h∗∈ℋh^* , the algorithm returns a predictor h h with ℒ,h∗(h^)≤ϵEL_D,h^*( h)≤ε (expectation over the randomness of the algorithm), then dc(ℋ)≤C⋅m/τ2dc(H)≤ C· m/τ^2. Perspective 2. Formalized setting and preliminaries. Let (,Σ)(X, ) be an arbitrary measurable space, and let ℋH be a class of measurable maps from X to −1,+1\-1,+1\. Write ℕ0=0,1,2,…N_0=\0,1,2,…\. For a probability measure D on (,Σ)(X, ), measurable target h, and measurable binary predictor g, write ℒ,h(g)=Prx∼g(x)≠h(x)L_D,h(g)= _x \g(x)≠ h(x)\. Dimension complexity is the least d∈ℕ0d _0 for which one map φ:→ℝd :X ^d, measurable with respect to the Borel sigma-algebra on ℝdR^d, satisfies ∀h∈ℋ∃wh∈ℝd∀x∈,h(x)⟨wh,φ(x)⟩>0.∀ h \ ∃ w_h ^d\ ∀ x , h(x) w_h, (x) >0. If no such finite d exists, set dc(ℋ)=+∞dc(H)=+∞. Fix a randomized learner A with hidden seed U∼μAU _A. Conditional on U=uU=u, it makes at most m adaptive unrestricted queries qt:×−1,+1→[−1,1]q_t:X×\-1,+1\→[-1,1], measurable with respect to the product sigma-algebra, each selected from the seed and the preceding public transcript, and then returns a measurable binary predictor. All seed-, transcript-, query-, and output-coordinate maps are assumed measurable. A deterministic complete response rule R assigns a value in [−1−τ,1+τ][-1-τ,1+τ] to every public query-bearing history admitted by A, including histories not reached by a particular seed or reply sequence. It does not observe the seed except through the public transcript. Let ℜAall R_A all contain all such rules, and let gu,Rg_u,R be the terminal predictor. A complete rule is (,h,τ)(D,h,τ)-valid if, at every round reached by every seed interacting with it, |vt−x∼qt(x,h(x))|≤τ. |v_t-E_x q_t(x,h(x)) |≤τ. Denote the valid rules by ℜA,τ(,h) R_A,τ(D,h). Accuracy below is required pointwise for every valid response rule. For every complete rule, define the seed-averaged terminal response and the static all-rule space FR(x)=U∼μA[gU,R(x)],VA=spanℝFR:R∈ℜAall,rA=dimVA.F_R(x)=E_U _A[g_U,R(x)], V_A=span_R\F_R:R∈ R_A all\, r_A= V_A. Thus VAV_A spans the seed-averaged terminal responses over all complete response rules. Technical assumptions. Assumption 4.39 (Primitive parameter regime). m∈ℕ0m _0, τ>0τ>0, and ε∈[0,1/4) ∈[0,1/4). Fixed numerical constants B≥1B≥ 1 and k≥1k≥ 1 are independent of the domain, class, learner instance, parameters, distributions, targets, response rules, and seeds. Assumption 4.40 (Fixed randomized adaptive unrestricted-SQ interface). The learner A is fixed before D, h, and the response policy. It uses at most m adaptive bounded unrestricted queries, may use the full preceding real-valued public transcript, and interacts measurably with every deterministic complete response rule. Assumption 4.41 (Every-valid-policy universal guarantee). For every distribution D, every h∈ℋh , and every R∈ℜA,τ(,h)R∈ R_A,τ(D,h), U∼μAℒ,h(gU,R)≤ε.E_U _AL_D,h(g_U,R)≤ . The expectation is over the learner seed, uniformly for every valid R. Assumption 4.42 (Static polynomial mean-response-rank certificate). The rank over all deterministic complete response rules is finite and obeys rA≤B(1+m/τ2)k.r_A≤ B (1+m/τ^2 )^k. This primitive certificate on the seed-averaged responses is fixed before the learning instance. Main theory. Theorem 4.9 (Conditional static mean-response-rank theorem). Under Assumptions 4.39– 4.42, choose once a basis ψ1,…,ψrA _1,…, _r_A of VAV_A and define φA(x)=(ψ1(x),…,ψrA(x)) _A(x)=( _1(x),…, _r_A(x)). This deterministic map is independent of the distribution, target, valid response policy, and realized seed. For every h∈ℋh , some wh∈ℝrAw_h ^r_A satisfies h(x)⟨wh,φA(x)⟩≥1−2ε>12>0for every x∈.h(x) w_h, _A(x) ≥ 1-2 > 12>0 every x . Consequently, dc(ℋ)≤rA≤B(1+m/τ2)k.dc(H)≤ r_A≤ B (1+m/τ^2 )^k. The conclusion is deterministic and pointwise. Discussion. This is partial progress. It preserves arbitrary domains, adaptive randomized SQ learning, adversarial tolerance-valid replies, and uniform success over distributions and targets. The decisive added condition is a static polynomial-rank certificate for the seed-averaged terminal responses. The resulting dimension bound is polynomial, B(1+m/τ2)kB(1+m/τ^2)^k, rather than the source target O(m/τ2)O(m/τ^2). Technical role and remaining barrier. The source SQ interface leaves a finite-dimensionality barrier: adaptive real-valued transcripts do not by themselves place the terminal predictors in a common finite-dimensional function space. The static rank certificate supplies that common space, so seed averaging and exactification can produce a deterministic representation. The remaining technical problem is to derive the source-scale compression from the SQ interface itself: if F,h0F^0_D,h is the seed-averaged terminal predictor under the canonical exact-center policy, then dimspanF,h0:,h≤Cm/τ2. \F^0_D,h:D,h\≤ Cm/τ^2. 4.4 Does Differential Privacy Make PAC Learning Much Harder? Open question. Denote VC(C)VC(C) the Vapnik-Chervonenkis dimension for a hypothesis class C, LD(C)LD(C) (28) the Littlestone dimension which is a combinatorial parameter characterizing online learnability. A randomized algorithm A:(X×0,1)n→A:(X×\0,1\)^n is (ϵ,δ)−(ε,δ)-Differentially Private (DP) (14) if for every pair of neighboring datasets S,S′S,S and every event E⊆E it holds that Pr[A(S)∈E]≤eϵPr[A(S′)∈E]+δ.Pr[A(S)∈ E]≤ e^εPr[A(S )∈ E]+δ. A private learner is a PAC learner that guarantees DP w.r.t. its training data. It is well known that DP learning requires more samples than non-private learning for some classes. 38 asks the central question: How much more is needed? Is the answer close to VC(C), or could it be drastically larger? 4.4.1 Subproblem 1: The Sample Complexity of Private Learning Open question. Identify a combinatorial measure of a class that determines the sample complexity of privately learning it, analogously to the characterization of non-private learning in terms of the VC dimension. Perspective 1. Formalized setting and preliminaries. Let (X,Σ)(X, ) be a measurable space, C⊆0,1XC \0,1\^X, and log be natural. A Cartesian partition makes restriction bijective onto the blockwise product; it is finest if it refines every such partition. For t≥1t≥ 1, let log2(0)t=t _2^(0)t=t, let log2(r) _2^(r) denote the r-fold iterate of the base-two logarithm for r≥1r≥ 1, and write log∗t=minr≥0:log2(r)t≤1 ^*t= \r≥ 0: _2^(r)t≤ 1\. For the finite finest Cartesian partition specified below, write X=⨆i=1kXiX= _i=1^kX_i, Ci=c|Xi:c∈CC_i=\c|_X_i:c∈ C\, and, for a candidate positive integer n, set di=LD(Ci),si=1+log∗(di+1),M⊕(C)=∑isi,ωi=siM⊕(C),mn,i=max8,⌈4nωi⌉.d_i=LD(C_i), s_i=1+ ^*(d_i+1), M_ (C)= _is_i, _i= s_iM_ (C), m_n,i= \8, 4n _i \. (1) Identify x,x′∈Xix,x ∈ X_i when every ci∈Cic_i∈ C_i agrees on them, and write Qi=Xi/≡iQ_i=X_i/ _i, κi:Xi→Qi _i:X_i→ Q_i, and Σi=A∩Xi:A∈Σ _i=\A∩ X_i:A∈ \, giving QiQ_i the discrete sigma-field 2Qi2^Q_i. Every ci∈Cic_i∈ C_i has a unique representative c¯i:Qi→0,1 c_i:Q_i→\0,1\ satisfying ci=c¯i∘κic_i= c_i _i; set C¯i=c¯i:ci∈Ci,ℋi=0,1Qi,ℋ⊕=∏iℋi, C_i=\ c_i:c_i∈ C_i\, _i=\0,1\^Q_i, = _iH_i, where ℋi H_i is the product sigma-field generated by finite evaluation cylinders and ℋ⊕=⨂iℋi H = _i H_i. A quotient tuple h¯=(h¯i)i∈ℋ⊕ h=( h_i)_i decodes as h¯(x)=h¯i(κi(x))h_ h(x)= h_i( _i(x)) for x∈Xix∈ X_i. For a probability measure D on (X,Σ)(X, ) and c∈Cc∈ C, let RD(h,c)=PrD[h(x)≠c(x)]R_D(h,c)= _D[h(x)≠ c(x)] and let DcD_c be the law of (x,c(x))(x,c(x)). An unrestricted learner is a Markov kernel on fixed-size replacement-adjacent samples, including nonrealizable ones, with arbitrary measurable output Ω and decoder hΩh_ ; it may be joint, improper, or computationally unbounded. Finite evaluations and stated risk events are measurable. Define SCε,δ(C)SC_ ,δ(C) as the least positive integer n for which such a private learner satisfies, for every c∈Cc∈ C and probability measure D on (X,Σ)(X, ), PrS∼Dcn,Ω∼An(S,⋅)[RD(hΩ,c)≤1/16]≥15/16. _S D_c^n,\, A_n(S,·)[R_D(h_ ,c)≤ 1/16]≥ 15/16. (2) Technical assumptions. Assumption 4.43 (Canonical finite Cartesian factorization). There is a finite finest Cartesian partition X=⨆i=1kXiX= _i=1^kX_i, k≥1k≥ 1, with Ci=c|Xi:c∈CC_i=\c|_X_i:c∈ C\ and C≃∏i=1kCiC _i=1^kC_i. Assumption 4.44 (VC-one factors). Every CiC_i is nonconstant, has VC(Ci)=1VC(C_i)=1, and has finite did_i. Assumption 4.45 (Measurable countable evaluation quotients). Each Xi∈ΣX_i∈ , each QiQ_i is finite or countable, and each cell κi−1(q) _i^-1(\q\) belongs to Σi _i. Equivalently, κi:(Xi,Σi)→(Qi,2Qi) _i:(X_i, _i)→(Q_i,2^Q_i) is measurable. Consequently, every target and decoded hypothesis is Σ -measurable, and quotient decoding preserves distributional zero-one risk exactly. Assumption 4.46 (Approximate-DP range). 0<ε≤1/100< ≤ 1/10 and 0<δ<10<δ<1. Assumption 4.47 (Candidate-wise lower-bound budget). At the lower-bound candidate n, 0<δ≤min1nlog(n+1),minicδmn,i2log(mn,i+1),0<δ≤ \ 1n (n+1), _i c_δm_n,i^2 (m_n,i+1) \, (3) where cδ>0c_δ>0 is universal. Main theory. Theorem 4.10 (Conditional private direct sum for Cartesian VC-one products). Under Assumptions 4.43–4.46, let KYK_Y be the universal constant of the quotient-first VC-one learner of 63, and define qi=⌈KYsiεlog2(esiεδ)⌉,Q⊕=∑iqi.q_i= K_Ys_i ^2\! ( es_i δ ) , Q_ = _iq_i. With Cup=65536C_ up=65536 and Cquota=max1,KY+1/20C_ quota= \1,K_Y+1/20\, route the first qiq_i block records with fixed padding, run fixed permutation-symmetrized, fully totalized factor learners for C¯i C_i into (ℋi,ℋi)(H_i, H_i) at (ε/2,δ/2)( /2,δ/2), form their tuple in (ℋ⊕,ℋ⊕)(H , H ), and decode. This is a measurable all-input replacement-(ε,δ)( ,δ)-DP learner. For n≥⌈CupQ⊕⌉n≥ C_ upQ_ , (2) holds and SCε,δ(C)≤⌈CupQ⊕⌉≤CupCquotaM⊕(C)εlog2(eM⊕(C)εδ).SC_ ,δ(C)≤ C_ upQ_ ≤ C_ upC_ quota M_ (C) ^2\! ( eM_ (C) δ ). (4) The upper bound holds throughout 0<δ<10<δ<1. Conversely, for universal clow>0c_ low>0, every candidate satisfying (3) and every unrestricted measurable replacement-(ε,δ)( ,δ)-DP learner satisfying (2) obey n≥clowM⊕(C)n≥ c_ lowM_ (C). Below this threshold some full-product target and arbitrary-support D with D(Xi)=ωiD(X_i)= _i satisfy PrS∼Dcn,Ω∼An(S,⋅)[RD(hΩ,c)>1/16]>1/16. _S D_c^n,\, A_n(S,·)[R_D(h_ ,c)>1/16]>1/16. (5) When (3) holds at n∗=SCε,δ(C)n_*=SC_ ,δ(C), the lower bound applies at the sample-complexity threshold and combines with (4). Discussion. This is partial progress. It preserves realizable binary PAC learning, arbitrary targets and data distributions, approximate privacy, and unrestricted learners in the lower bound. The main restriction is to Cartesian products of VC-one, finite-Littlestone factors with countable evaluation quotients. Within this subclass it gives matching bounds up to privacy and logarithmic factors; the lower bound additionally requires the stated small-δ condition. Technical role and remaining barrier. The source setting leaves two structural barriers: a general finite- Littlestone class has no factorwise decomposition to which threshold bounds apply, and arbitrary evaluation spaces can make the learner construction non-measurable. Cartesian VC-one structure supplies the factorwise direct sum, while countable evaluation quotients provide a measurable quotient-first learner. The small-δ condition separately makes the threshold lower bound applicable. The remaining problem is to obtain a comparable intrinsic characterization for every measurable class of finite Littlestone dimension, without the Cartesian, VC-one, or countable-quotient assumptions and without the candidate-wise small-δ restriction. 4.4.2 Subproblem 2: Class Existence Open question. Does there exist a sequence of finite-size classes C=Cκ∈ℕC=\C_κ\_κ where: (1) limκ→∞|Cκ|=∞, _κ→∞|C_κ|=∞, (2) log|Cκ| |C_κ| is superpolynomial in VC(Cκ)VC(C_κ), and (3) The number of samples required to learn CκC_κ under differential privacy is Ω(log|Cκ|) ( |C_κ|). Perspective 2. Formalized setting and preliminaries. Let (X,Σ)(X, ) be a measurable space, and let C be a finite class of Σ -measurable maps from X to 0,1\0,1\. For t∈[N]t∈[N], let τt(q)=q≤t _t(q)=1\q≤ t\. The class C has a (k,N)(k,N) disjoint-threshold minor if there are injections ϕj:[N]→X _j:[N]→ X with disjoint images and concepts c∈Cc_t∈ C, ∈[N]kt∈[N]^k, such that c(ϕj(q))=τtj(q)(j∈[k],q∈[N]).c_t( _j(q))= _t_j(q) (j∈[k],\ q∈[N]). For a probability law Q on the product measurable space X×0,1X×\0,1\, write LQ(h)=Pr(x,y)∼Q[h(x)≠y]L_Q(h)= _(x,y) Q[h(x)≠ y] for measurable h. Learners use exactly an integer m≥1m≥ 1 iid examples and replacement adjacency; their output hypotheses and all output-coordinate evaluation maps are measurable. For a probability measure P on (X,Σ)(X, ) and c∈Cc∈ C, let QP,cQ_P,c be the law of (x,c(x))(x,c(x)) for x∼Px P, and define log∗t=minr≥0:log2(r)t≤1 ^*t= \r≥ 0: _2^(r)t≤ 1\. Here log is natural. Technical assumptions. Assumption 4.48 (Disjoint-threshold restriction table). Integers k≥1k≥ 1, N≥2N≥ 2, and C admit the minor defined above. Assumption 4.49 (Unrestricted private PAC antecedent). The kernel A:(X×0,1)m↝0,1XA:(X×\0,1\)^m \0,1\^X is replacement-(ε0,δm)( _0, _m)-DP and, for every c∈Cc∈ C and distribution P on X, PrS∼QP,cm,h∼A(S)[LQP,c(h)>α0]≤β0. _S Q_P,c^m,\,h A(S)[L_Q_P,c(h)> _0]≤ _0. The learner may be improper and computationally unbounded. Assumption 4.50 (Fixed PAC and approximate-privacy scale). α0=1128,β0=132,0<ε0≤1,0≤δm≤cδm2log(em), _0= 1128, _0= 132, 0< _0≤ 1, 0≤ _m≤ c_δm^2 (em), where the theorem fixes the universal constant cδc_δ. Main theory. Theorem 4.11 (Private direct-sum threshold-minor lower bound). There are universal constants c,cδ>0c,c_δ>0 and N0≥2N_0≥ 2 such that, for every k≥1k≥ 1, N≥N0N≥ N_0, domain X, finite class C, and fixed-sample learner satisfying Assumptions 4.48–4.50, m≥cklog∗N,m≥ c\,k ^*N, where log∗ ^* is the base-two iterated logarithm. Discussion. This is partial progress. It preserves finite binary classes, distribution-free realizable PAC learning, approximate privacy, and a lower bound against unrestricted learners. It differs from the source problem in two essential ways: (i) the class must contain a (k,N)(k,N) disjoint-threshold minor, under a small-δm _m privacy regime; (i) the conclusion is Ω(klog∗N) (k ^*N) rather than the requested Ω(log|C|) ( |C|) existential separation. Technical role and remaining barrier. The source class-existence question leaves two barriers: an arbitrary finite class need not contain independent threshold-hard directions, and combining many hard directions can violate record-level privacy through record reuse or group privacy. The disjoint-threshold minor exposes independent hard coordinates, and the one-use hidden-arm reduction combines them while preserving record-level adjacency. The small-δm _m regime makes the component threshold lower bound applicable. The remaining problem is to construct finite classes with log|Cκ| |C_κ| superpolynomial in VC(Cκ)VC(C_κ) for which every private learner requires Ω(log|Cκ|) ( |C_κ|) samples without relying on the added small-δm _m regime. 4.5 Online Optimization of Piecewise-Lipschitz Functions with Applications to Data-Driven Algorithm Design 4.5.1 Subproblem 1: Polynomial Boundaries Open question. For a monic polynomial ϕα(θ)=θd+αd−1θd−1+⋯+α0,α∈[−R,R]d,θ∈Θ, _α(θ)=θ^d+ _d-1θ^d-1+·s+ _0, α∈[-R,R]^d, θ∈ , for a coefficient distribution class D, the relevant constant for a coefficient-law class D is C=supμ∈supI⊆Θ interval|I|>0Prα∼μ[∃θ∈I:ϕα(θ)=0]|I|.C_D= _μ _ subarraycI interval\\ |I|>0 subarray _α μ[∃θ∈ I: _α(θ)=0]|I|. The first subproblem of 5 asks: under what natural necessary and sufficient conditions on D is C_D finite, and under what conditions is it bounded by a polynomial in d and R? Perspective 2. Formalized setting and preliminaries. Let Θ⊆ℝ be compact and ℐ(Θ)I( ) its positive finite-length intervals, with arbitrary endpoint conventions. For d≥1d≥ 1, R≥1R≥ 1, and α=(α0,…,αd−1)∈[−R,R]dα=( _0,…, _d-1)∈[-R,R]^d, set ϕα(θ)=θd+∑j=0d−1αjθj,Hd,I=α:∃θ∈I,ϕα(θ)=0. _α(θ)=θ^d+ _j=0^d-1 _jθ^j, H_d,I=\α:∃θ∈ I,\ _α(θ)=0\. For a law μ, define the random regular conditional-density norms K0μ=∥fα0∣α1:d−1μ(⋅∣α1:d−1)∥L∞(ℝ),K∞μ=∥fαd−1∣α0:d−2μ(⋅∣α0:d−2)∥L∞(ℝ),K_0^μ=\|f^μ_ _0 _1:d-1(\,· _1:d-1)\|_L^∞(R), K_∞^μ=\|f^μ_ _d-1 _0:d-2(\,· _0:d-2)\|_L^∞(R), evaluated at the random conditioning coordinates (for d=1d=1, both are the density norm of α0 _0). For fixed finite η=(κ¯0,κ¯∞)η=( κ_0, κ_∞), let d,R,ηD_d,R,η contain exactly the laws supported on [−R,R]d[-R,R]^d whose two regular conditional densities exist almost surely and obey K0μ≤κ¯0EK_0^μ≤ κ_0 and K∞μ≤κ¯∞EK_∞^μ≤ κ_∞. These are mean caps, rather than almost-sure uniform caps. Thus d,R,ηD_d,R,η permits dependent laws specified through endpoint regular conditional densities. Define Cd,R,η=supμ∈d,R,ηsupI∈ℐ(Θ)μ(Hd,I)|I|.C_D_d,R,η= _μ _d,R,η _I ( ) μ(H_d,I)|I|. All interval lengths are Lebesgue lengths, and the definition assigns value zero whenever either indexing family is empty. For I0=I∩[−1,1]I_0=I∩[-1,1], I+=I∩(1,∞)I_+=I∩(1,∞), and I−=I∩(−∞,−1)I_-=I∩(-∞,-1), set B0=d+Rd(d−1)2,B∞=1+Rd(d−1)2,Mη=maxκ¯0B0,κ¯∞B∞,κ¯∗=maxκ¯0,κ¯∞.B_0=d+ Rd(d-1)2, B_∞=1+ Rd(d-1)2, M_η= \ κ_0B_0, κ_∞B_∞\, κ_*= \ κ_0, κ_∞\. Define a witness law by taking α0 _0 uniform on [−R,R][-R,R] when d=1d=1, take α0,α1 _0, _1 independently uniform when d=2d=2, and, for d≥3d≥ 3, take independent uniform endpoint coefficients and set every middle coefficient to RSRS for one independent Rademacher S. Call the resulting law μd,Rwitμ wit_d,R. Technical assumptions. Assumption 4.51 (Compact parameter domain). Θ⊆ℝ is fixed and compact; the result is uniform in I∈ℐ(Θ)I ( ) and independent of Θ . Assumption 4.52 (Indexed regime). d≥1d≥ 1, R≥1R≥ 1, and finite η∈[0,∞)2η∈[0,∞)^2 is fixed independently of (d,R)(d,R). Assumption 4.53 (Compact cube support and monicity). Every quantified law is supported on [−R,R]d[-R,R]^d, and ϕα _α is exactly monic. Assumption 4.54 (Mean endpoint conditional-density caps). The two conditional densities and mean bounds defining d,R,ηD_d,R,η hold. Main theory. Theorem 4.12 (Endpoint conditional anti-concentration). Under Assumptions 4.51– 4.54, for every μ∈d,R,ημ _d,R,η and I∈ℐ(Θ)I ( ), μ(Hd,I)≤κ¯0B0|I0|+κ¯∞B∞(|I+|+|I−|)≤Mη|I|.μ(H_d,I)≤ κ_0B_0|I_0|+ κ_∞B_∞(|I_+|+|I_-|)≤ M_η|I|. Consequently, Cd,R,η≤Mη≤κ¯∗d+κ¯∗2Rd2.C_D_d,R,η≤ M_η≤ κ_*d+ κ_*2Rd^2. If κ¯0,κ¯∞≥1/2 κ_0, κ_∞≥ 1/2, then for every d,Rd,R the witness law belongs to d,R,ηD_d,R,η and K0μwit=K∞μwit=1/(2R)K_0^μ wit=K_∞^μ wit=1/(2R) almost surely. Discussion. This is partial progress. It preserves monic degree-d polynomials, cube-supported coefficients, and the source root-hitting constant. It differs from the source problem in three ways: (i) the coefficient law must satisfy endpoint conditional-density bounds; (i) the theorem is restricted to R≥1R≥ 1; (i) it gives a sufficient polynomial upper bound, not a necessary-and- sufficient characterization. Technical role and remaining barrier. The source coefficient-law problem leaves two analytic barriers. General laws provide no controlled one-dimensional sweep near zero or infinity, and a direct joint-density argument can incur exponential dependence on the ambient coefficient dimension. The endpoint conditional-density bounds control the two endpoint charts separately, while the outer pivot removes the large-root growth, yielding the bound Oη(Rd2)O_η(Rd^2). The restriction R≥1R≥ 1 has a separate role: when κ¯0,κ¯∞≥1/2 κ_0, κ_∞≥ 1/2, it makes the indexed family uniformly nonempty under the fixed caps, since the witness satisfies K0=K∞=1/(2R)≤1/2K_0=K_∞=1/(2R)≤ 1/2. The local sweep bounds themselves extend to R>0R>0 whenever the capped family is nonempty. The remaining problem is to obtain a natural coefficient-side condition that is necessary and sufficient, up to polynomial factors, for all R>0R>0 and general coefficient-law classes, including the cap scaling needed in the small-R regime. 4.5.2 Subproblem 2: Pfaffian Boundaries Open question. Let F=(F1,…,FN)F=(F_1,…,F_N) be a vector of Pfaffian functions on a compact interval Θ , and let ϕα(θ)=⟨α,F(θ)⟩,α∈[−R,R]N. _α(θ)= α,F(θ) , α∈[-R,R]^N. Suppose every law in D has a joint density bounded by κ. The second subproblem of 5 asks: what normalization of F, analogous to fixing the leading coefficient of a polynomial to one, guarantees that CPfC^Pf_D is finite? Here CPf=supμ∈supI⊆Θ interval|I|>0Prα∼μ[∃θ∈I:ϕα(θ)=0]|I|.C^Pf_D= _μ _ subarraycI interval\\ |I|>0 subarray _α μ[∃θ∈ I: _α(θ)=0]|I|. Perspective 1. Formalized setting and preliminaries. Let Θ=[c−h,c+h] =[c-h,c+h], x=(θ−c)/h∈[−1,1]x=(θ-c)/h∈[-1,1], and use the one-parameter convention p=1p=1. Let η=(η1,…,ηq)η=( _1,…, _q) be a triangular Pfaffian chain with polynomials Pj(x,y1:j)P_j(x,y_1:j). For output polynomials Qi(x,y1:q)Q_i(x,y_1:q), define Gi(x)=Qi(x,η(x)),Fi(θ)=Gi(x(θ)),G_i(x)=Q_i(x,η(x)), F_i(θ)=G_i(x(θ)), M=maxjdegPj,Δ=maxidegQi,BP=maxj‖coeff(Pj)‖1,BQ=maxi‖coeff(Qi)‖1,M= _j P_j, = _i Q_i, B_P= _j\|coeff(P_j)\|_1, B_Q= _i\|coeff(Q_i)\|_1, with total degrees and M=BP=0M=B_P=0 if q=0q=0. Let N,R,κD_N,R,κ be all laws on [−R,R]N[-R,R]^N with full joint density at most κ; their coordinates may be arbitrarily correlated. Set =N,R,κ,A=(2R)Nκ,γF=F/‖F‖2,Γproj(F)=esssupθ∈Θ‖γF′(θ)‖2,D=D_N,R,κ, A=(2R)^Nκ, _F=F/\|F\|_2, _ proj(F)= *ess\,sup_θ∈ \| _F (θ)\|_2, and let CPf(F,Θ)C Pf_D(F; ) be the supremum, first over positive-length intervals I⊆ΘI and then over μ∈N,R,κμ _N,R,κ, of Prμ[∃θ∈I:⟨α,F(θ)⟩=0]/|I| _μ[∃θ∈ I: α,F(θ) =0]/|I|. For an affine offset F0∈C1(Θ)F_0∈ C^1( ) and a measurable partition I=⨆jEjI= _jE_j with Fj≠0F_j≠ 0 on EjE_j, index β∈[−R,R]N−1β∈[-R,R]^N-1 by i≠ji≠ j and set Tj(θ,β)=−F0(θ)Fj(θ)−∑i≠jβiFi(θ)Fj(θ).T_j(θ,β)=- F_0(θ)F_j(θ)- _i≠ j _i F_i(θ)F_j(θ). For N=1N=1, the zero-dimensional cube has Lebesgue mass one. Technical assumptions. Assumption 4.55 (Primitive parameter regime). N≥1N≥ 1, q≥0q≥ 0, h,R>0h,R>0, 0<κ<∞0<κ<∞, the class N,R,κD_N,R,κ is nonempty, and all degrees and coefficient budgets in (F1) are finite. Assumption 4.56 (Balcan common-chain presentation). Each ηj∈C1([−1,1]) _j∈ C^1([-1,1]) satisfies ηj′=Pj(x,η1:j) _j =P_j(x, _1:j), and every Gi=Qi(x,η)G_i=Q_i(x,η), with the degree convention (F1). Assumption 4.57 (Literal anchor and unit-range certificate). |ηj(x)|≤1| _j(x)|≤ 1 on [−1,1][-1,1] and Q1≡1Q_1≡ 1. Thus F1=G1=1F_1=G_1=1, supplying the norm margin used below. Assumption 4.58 (Arbitrarily correlated capped joint laws). Every probabilistic clause quantifies over arbitrary μ∈N,R,κμ _N,R,κ, including dependent coordinate laws. Assumption 4.59 (Deterministic affine offset and pivot cover). The affine clause uses precisely the deterministic F0F_0 and measurable pivot partition described before (F2). Main theory. Theorem 4.13 (Anchored coefficient-normalized Pfaffian sweep). Under Assumptions 4.55– 4.57, the following five conclusions hold; the probabilistic ones also use Assumption 4.58, and the affine one uses Assumption 4.59. (R1) Projective speed. With D∗=ΔBQ(1+qBP)D_*= B_Q(1+qB_P), pointwise |Gi′|≤D∗,‖G′‖2≤ND∗,Γproj(F)≤NΔBQ(1+qBP)h.|G_i |≤ D_*, \|G \|_2≤ ND_*, _ proj(F)≤ N B_Q(1+qB_P)h. The literal anchor gives ‖F‖2,‖G‖2≥1\|F\|_2,\|G\|_2≥ 1, so this conditioning is derived from the normalized presentation. (R2) Central sweep. For every possibly correlated μ∈N,R,κμ _N,R,κ and then every positive-length I⊆ΘI , Prμ[∃θ∈I:⟨α,F(θ)⟩=0]≤AN2Γproj(F)|I|≤ANΔBQ(1+qBP)2h|I|, _μ[∃θ∈ I: α,F(θ) =0]≤ A N2 _ proj(F)|I|≤ AN B_Q(1+qB_P) 2h|I|, and the same two coefficients bound CPf(F,Θ)≤AN2Γproj(F)≤ANΔBQ(1+qBP)2h.C Pf_D(F; )≤ A N2 _ proj(F)≤ AN B_Q(1+qB_P) 2h. (R3) Affine sweep. For every μ∈N,R,κμ _N,R,κ, interval, and admissible pivot cover, Prμ[∃θ∈I:F0(θ)+⟨α,F(θ)⟩=0]≤κ∑j=1N∫Ej∫[−R,R]N−1|∂θTj(θ,β)|dβdθ. _μ[∃θ∈ I:F_0(θ)+ α,F(θ) =0]≤κ _j=1^N _E_j _[-R,R]^N-1| _θT_j(θ,β)|\,dβ\,dθ. The right side is interpreted in [0,+∞][0,+∞] and may equal +∞+∞. (R4) Exact monic recovery. For every integer d≥1d≥ 1 and bounded interval J⊂ℝJ , choose Θ⊇J J and set F0(θ)=θdF_0(θ)=θ^d, Fk+1(θ)=θkF_k+1(θ)=θ^k for 0≤k<d0≤ k<d. Thus pα(θ)=θd+∑k<dαkθkp_α(θ)=θ^d+ _k<d _kθ^k, with the monic coefficient deterministic and outside the random vector, and Q0(x) Q_0(x) =(c+hx)d, =(c+hx)^d, Qk+1(x) Q_k+1(x) =(c+hx)k, =(c+hx)^k, Δaug _ aug =d, =d, q q =M=BP=0, =M=B_P=0, N N =d, =d, A A =(2R)dκ. =(2R)^dκ. Using E1=J∩|θ|≤1E_1=J∩\|θ|≤ 1\ and Ed=J∩|θ|>1E_d=J∩\|θ|>1\ (or E1=JE_1=J for d=1d=1) in (R3) gives, for every possibly correlated μ∈d,R,κμ _d,R,κ, Prμ[∃θ∈J:pα(θ)=0]≤κ(2R)d−1(d+Rd(d−1)2)|J|. _μ[∃θ∈ J:p_α(θ)=0]≤κ(2R)^d-1 (d+ Rd(d-1)2 )|J|. (R5) Counterexample scale. For 0<δ≤10<δ≤ 1, take F(θ)=(1,θ/δ)F(θ)=(1,θ/δ) on [−1,1][-1,1] and the uniform law on [−1,1]2[-1,1]^2, so κ=1/4κ=1/4 and A=1A=1. Then BQ=Γproj(F)=1/δB_Q= _ proj(F)=1/δ and, for every 0<ϵ≤δ0<ε≤δ, Pr[∃θ∈[0,ϵ]:α1+α2θ/δ=0]=ϵ4δ,14δ≤C2,1,1/4Pf(F;[−1,1])≤1δ≤2δ. [∃θ∈[0,ε]: _1+ _2θ/δ=0]= ε4δ, 14δ≤ C Pf_D_2,1,1/4(F;[-1,1])≤ 1δ≤ 2δ. When BPB_P is fixed, the dependence on M is degree zero. Discussion. This is full progress for the declared anchored unit-range normalization: the literal anchor and bounded-chain presentation yield finite, explicit projective and central sweep bounds, a general affine chart inequality, exact monic recovery, and the counterexample’s unavoidable 1/δ1/δ scale. Whether every raw Pfaffian presentation admits this normalization with polynomial parameter budgets remains open. 5 Conclusion and Discussions VALG organizes informal ML-theory research around source-relative theorem branches whose assumptions, proof dependencies, and outcomes remain tied to the originating question. Its global-to-local proof process supports both local repair and formulation-level revision, allowing a failed proof mechanism to produce a clearly scoped variant or relaxation. Across nine COLT 2026 case studies, two runs produce internally finalized theorem candidates that match the scope of the original subproblems, while the remaining runs yield restricted-method results, special cases, or conditional theorems. An important next step is to make AI-generated mathematics more readable and verifiable for researchers. Current systems tend to overuse notation and present proofs in ways that obscure the main argument, often deviating from established human proof-writing conventions. Even when derivations are plausible, these stylistic issues significantly increase the cost of expert verification. Rigorous evaluation also requires machine learning theory benchmarks that go beyond case studies of open problems. Our findings on COLT open problems indicate that difficult questions often benefit from multiple perspectives and evolving generation of ideas. However, to meaningfully assess the contribution and redundancy of these components, we need controlled benchmarks with known solutions, alternative valid formulations, explicit assumptions and relaxations, and clearly documented proof dependencies. Finally, formalization also remains a critical challenge. ML theory draws on probability, optimization, statistics, information theory, and learning theory, i.e., domains for which existing general-purpose formalization pipelines are often incomplete or cumbersome. Developing automated formalization tools tailored to the specific statements and proof patterns of ML theory would enable natural-language agents to explore formulations and proof strategies, while formal tools verify the mathematical core of their results. All of these further explorations and developments require the participation and effort of the entire ML theory community. References An et al. (2026) C. An, Q. Ye, M. Pan, and J. Zhang QED: an open-source multi-agent system for generating mathematical proofs on open problems. External Links: 2604.24021, Link Cited by: §2.1, §3.2.2, §3.2. Angluin (1987) D. Angluin Learning regular sets from queries and counterexamples. Information and Computation 75 (2), p. 87–106. External Links: Document Cited by: footnote 1. Arvanitakis et al. (2026) D. Arvanitakis, V. Srinivas, and A. Vijayaraghavan Open problem: how much overparametrization is needed for ALS in tensor decomposition?. In Proceedings of the Thirty-Ninth Conference on Learning Theory, Proceedings of Machine Learning Research, Vol. 336, p. 7105–7110. External Links: Link Cited by: §1, §4.1, §4. Azerbayev et al. (2023) Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad ProofNet: autoformalizing and formally proving undergraduate-level mathematics. External Links: 2302.12433, Link Cited by: §2.3, §2.4. Balcan et al. (2026) M. Balcan, W. Pegden, and D. Sharma Invited open problem: online optimization of piecewise-Lipschitz functions with applications to data-driven algorithm design. In Proceedings of the Thirty-Ninth Conference on Learning Theory, Proceedings of Machine Learning Research, Vol. 336. External Links: Link Cited by: §1, §4.5.1, §4.5.2, §4. Ben-David et al. (2002) S. Ben-David, N. Eiron, and H. U. Simon Limitations of learning via embeddings in euclidean half spaces. Journal of Machine Learning Research 3 (Nov), p. 441–461. Cited by: §4.3. Cabral et al. (2025) R. Cabral, T. M. Do, X. Yu, W. M. Tai, Z. Feng, and X. Shen ProofFlow: a dependency graph approach to faithful proof autoformalization. External Links: 2510.15981, Link Cited by: §2.3. Cao et al. (2026) Y. Cao, R. Qiu, J. Liu, J. Wang, D. Guo, R. Feng, L. Zhi, and X. Gao MechMath Agent Team: LLM driven agents for mathematical research. External Links: 2607.04394, Link Cited by: §2.1. Chan et al. (2024) J. S. Chan, N. Chowdhury, O. Jaffe, J. Aung, D. Sherburn, E. Mays, G. Starace, K. Liu, L. Maksin, T. Patwardhan, L. Weng, and A. Madry MLE-bench: evaluating machine learning agents on machine learning engineering. External Links: 2410.07095, Link Cited by: §1, §2.4. Chen et al. (2026) L. Chen, Z. Liu, W. He, and B. Dong Iteris: agentic research loops for computational mathematics. External Links: 2606.02484, Link Cited by: §2.1, §2.1. Chen and Jiang (2026) X. Chen and X. Jiang Moonshine: an autonomous mathematical research agent centered on conjecture generation. External Links: 2606.10806, Link Cited by: §2.1. Chen et al. (2025) Z. Chen, S. Chen, Y. Ning, Q. Zhang, B. Wang, B. Yu, Y. Li, Z. Liao, C. Wei, Z. Lu, V. Dey, M. Xue, F. N. Baker, B. Burns, D. Adu-Ampratwum, X. Huang, X. Ning, S. Gao, Y. Su, and H. Sun ScienceAgentBench: toward rigorous assessment of language agents for data-driven scientific discovery. In International Conference on Learning Representations, External Links: 2410.05080, Link Cited by: §2.4. Davies et al. (2021) A. Davies, P. Veličković, L. Buesing, S. Blackwell, D. Zheng, N. Tomašev, R. Tanburn, P. Battaglia, C. Blundell, A. Juhász, et al. Advancing mathematics by guiding human intuition with AI. Nature 600, p. 70–74. External Links: Document Cited by: §2.1. Dwork et al. (2016) C. Dwork, F. McSherry, K. Nissim, and A. Smith Calibrating noise to sensitivity in private data analysis. Journal of Privacy and Confidentiality 7 (3), p. 17–51. Cited by: §4.4. Feldman et al. (2026) V. Feldman, P. Kamath, and N. Srebro Invited open problem: is the power of deep learning over linear models inherently distribution dependent?. In Proceedings of the Thirty-Ninth Conference on Learning Theory, Proceedings of Machine Learning Research, Vol. 336, p. 7117–7122. External Links: Link Cited by: §1, §4.3, §4. Feng et al. (2026) T. Feng et al. Towards autonomous mathematics research. External Links: 2602.10177, Link Cited by: §1, §2.1, §2.4, §3.2. Gold (1967) E. M. Gold Language identification in the limit. Information and Control 10 (5), p. 447–474. External Links: Document Cited by: footnote 1. Gottweis et al. (2026) J. Gottweis, W. Weng, A. Daryin, et al. Accelerating scientific discovery with Co-Scientist. Nature. External Links: Document, Link Cited by: §1, §2.1. He et al. (2026) Y. He, D. Li, G. Li, J. Geng, Z. Huang, C. Ren, Z. Zhang, Y. Liu, S. Zhu, H. Zhang, et al. ReasFlow: assisting reasoning-centric scientific discovery in applied mathematics via a knowledge-based multi-agent system. External Links: 2607.14178, Link Cited by: §1, §2.1. Huang et al. (2023) Q. Huang, J. Vora, P. Liang, and J. Leskovec MLAgentBench: evaluating language agents on machine learning experimentation. External Links: 2310.03302, Link Cited by: §1, §2.4. Jiang et al. (2023) A. Q. Jiang, W. Li, and M. Jamnik Multilingual mathematical autoformalization. External Links: 2311.03755, Link Cited by: §2.3. Ju et al. (2026) H. Ju, G. Gao, J. Jiang, B. Wu, Z. Sun, S. Liu, L. Chen, Y. Wang, Y. Wang, Z. Wang, W. He, et al. Automated conjecture resolution with formal verification. External Links: 2604.03789, Link Cited by: §2.1, §3.2. Kripner and Straka (2026) M. Kripner and M. Straka OpenProver: agentic and interactive theorem proving with Lean 4. External Links: 2607.09217, Link Cited by: §1, §2.2. Lample et al. (2022) G. Lample, M. Lachaux, T. Lavril, X. Martinet, A. Hayat, G. Ebner, A. Rodriguez, and T. Lacroix HyperTree proof search for neural theorem proving. External Links: 2205.11491, Link Cited by: §2.2. Lau and Scarlett (2026a) I. Lau and J. Scarlett Open problem: is interaction necessary for order-optimal 1-bit mean estimation?. In Proceedings of the Thirty-Ninth Conference on Learning Theory, Proceedings of Machine Learning Research, Vol. 336, p. 7123–7128. External Links: Link Cited by: §1, §4.2, §4. Lau and Scarlett (2026b) I. Lau and J. Scarlett Order-optimal sequential 1-bit mean estimation in general tail regimes. External Links: 2604.07796, Link Cited by: §4.2.1, §4.2.1. Lin et al. (2025) H. Lin, Z. Sun, S. Welleck, and Y. Yang Lean-STaR: learning to interleave thinking and proving. External Links: 2407.10040, Link Cited by: §2.2. Littlestone (1988) N. Littlestone Learning quickly when irrelevant attributes abound: a new linear-threshold algorithm. Machine learning 2 (4), p. 285–318. Cited by: §4.4, footnote 1. Liu et al. (2026a) C. Liu, Y. Yin, Y. Yuan, J. Xie, B. Li, S. Li, J. Shen, Y. Xu, L. Shang, and M. Zhang Discover and prove: an open-source agentic framework for hard mode automated theorem proving in Lean 4. External Links: 2604.15839, Link Cited by: §2.2. Liu et al. (2026b) J. Liu, G. Gao, Z. Sun, B. Wu, S. Liu, J. Jiang, H. Ju, L. Chen, R. Cheng, X. Zhang, and B. Dong Danus: orchestrating mathematical reasoning agents with fact-graph memory. External Links: 2607.06447, Link Cited by: §1, §2.1. Liu et al. (2026) J. Liu et al. Numina-Lean-Agent: an open and general agentic reasoning system for formal mathematics. External Links: 2601.14027, Link Cited by: §2.2. Liu et al. (2026c) T. Liu, S. Zhang, Z. Geng, H. Liu, R. Xu, P. Wang, L. Yuan, and Y. Yu Efficient test-time optimization for multi-agent proof autoformalization. External Links: 2607.11307, Link Cited by: §2.3. Lu et al. (2024) C. Lu, C. Lu, R. T. Lange, J. Foerster, J. Clune, and D. Ha The AI scientist: towards fully automated open-ended scientific discovery. External Links: 2408.06292, Link Cited by: §1, §2.1. Ma et al. (2026) D. Ma et al. OProver: a unified framework for agentic formal theorem proving. External Links: 2605.17283, Link Cited by: §2.2. Madaan et al. (2023) A. Madaan, N. Tandon, P. Gupta, S. Hallinan, L. Gao, S. Wiegreffe, U. Alon, N. Dziri, S. Prabhumoye, Y. Yang, S. Welleck, B. P. Majumder, S. Gupta, A. Yazdanbakhsh, and P. Clark Self-refine: iterative refinement with self-feedback. In Advances in Neural Information Processing Systems, Vol. 36. External Links: Link Cited by: §1. Min et al. (2026) M. J. Min, M. He, Z. Li, Z. Yi, S. Malik, A. Gupta, X. Si, and O. Bastani Theory-level autoformalization: from isolated statements to unified formal knowledge bases. External Links: 2607.13292, Link Cited by: §2.3. Moakhar et al. (2026) A. S. Moakhar, F. Gholami, A. Springer, Y. JafariRaviz, and M. Hajiaghayi Beyond the library: an agentic framework for autoformalizing research mathematics. External Links: 2606.31134, Link Cited by: §2.3. Nissim et al. (2026) K. Nissim, U. Stemmer, and E. Tsfadia Invited open problem: does differential privacy make PAC learning much harder?. In Proceedings of the Thirty-Ninth Conference on Learning Theory, Proceedings of Machine Learning Research, Vol. 336. External Links: Link Cited by: §1, §4.4, §4. Novikov et al. (2025) A. Novikov, N. Vũ, M. Eisenberger, E. Dupont, P. Huang, A. Z. Wagner, S. Shirobokov, B. Kozlovskii, F. J. R. Ruiz, A. Mehrabian, et al. AlphaEvolve: a coding agent for scientific and algorithmic discovery. External Links: 2506.13131, Link Cited by: §2.1. Ren et al. (2025) Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, et al. DeepSeek-Prover-V2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. External Links: 2504.21801, Link Cited by: §2.2. Romera-Paredes et al. (2024) B. Romera-Paredes, M. Barekatain, A. Novikov, M. Balog, M. P. Kumar, E. Dupont, F. J. R. Ruiz, J. S. Ellenberg, P. Wang, O. Fawzi, et al. Mathematical discoveries from program search with large language models. Nature 625, p. 468–475. External Links: Document Cited by: §2.1. Santhana Srinivasan R and Patawar (2026) Santhana Srinivasan R and M. Patawar LAMP: lean-based agentic framework with MCP and proof repair. External Links: 2606.28841, Link Cited by: §2.2. Schmidgall et al. (2025) S. Schmidgall, Y. Su, Z. Wang, X. Sun, J. Wu, X. Yu, J. Liu, M. Moor, Z. Liu, and E. Barsoum Agent laboratory: using LLM agents as research assistants. External Links: 2501.04227, Link Cited by: §1, §2.1. Schmitt et al. (2026) J. Schmitt, T. Gehrunger, J. Dekoninck, G. Bérczi, U. Kreitner, and L. Price ProofCouncil: an LLM agent for solving open mathematical problems. External Links: Link Cited by: §2.1. Shalev-Shwartz and Ben-David (2014) S. Shalev-Shwartz and S. Ben-David Understanding machine learning: from theory to algorithms. Cambridge University Press. External Links: Document Cited by: §1. Shinn et al. (2023) N. Shinn, F. Cassano, A. Gopinath, K. Narasimhan, and S. Yao Reflexion: language agents with verbal reinforcement learning. In Advances in Neural Information Processing Systems, Vol. 36. External Links: Link Cited by: §1. Siegel et al. (2024) Z. S. Siegel, S. Kapoor, N. Nadgir, B. Stroebl, and A. Narayanan CORE-Bench: fostering the credibility of published research through a computational reproducibility agent benchmark. External Links: 2409.11363, Link Cited by: §2.4. Son et al. (2026) G. Son, S. Yi, M. Gwak, H. Ko, W. Jang, and Y. Yu ResearchMath-14K: scaling research-level mathematics via agents. External Links: 2605.28003, Link Cited by: §2.4. Starace et al. (2025) G. Starace, O. Jaffe, D. Sherburn, J. Aung, J. S. Chan, et al. PaperBench: evaluating AI’s ability to replicate AI research. External Links: 2504.01848, Link Cited by: §1, §2.4. Thakur et al. (2024) A. Thakur, G. Tsoukalas, Y. Wen, J. Xin, and S. Chaudhuri An in-context learning agent for formal theorem-proving. In Proceedings of the 7th Conference on Artificial Intelligence and Theorem Proving, External Links: 2310.04353, Link Cited by: §2.2. Trinh et al. (2024) T. H. Trinh, Y. Wu, Q. V. Le, H. He, and T. Luong Solving olympiad geometry without human demonstrations. Nature 625, p. 476–482. External Links: Document Cited by: §2.1. Tsoukalas et al. (2024) G. Tsoukalas, J. Lee, J. Jennings, J. Xin, M. Ding, M. Jennings, A. Thakur, and S. Chaudhuri PutnamBench: evaluating neural theorem-provers on the putnam mathematical competition. In Advances in Neural Information Processing Systems, External Links: 2407.11214, Link Cited by: §2.4. Valiant (1984) L. G. Valiant A theory of the learnable. Communications of the ACM 27 (11), p. 1134–1142. External Links: Document Cited by: §1, footnote 1. Vapnik (1998) V. N. Vapnik Statistical learning theory. Wiley. Cited by: §1. Wainwright (2019) M. J. Wainwright High-dimensional statistics: a non-asymptotic viewpoint. Cambridge University Press. External Links: Document Cited by: §1. Wang et al. (2023) H. Wang, H. Xin, C. Zheng, L. Li, Z. Liu, Q. Cao, Y. Huang, J. Xiong, H. Shi, E. Xie, et al. LEGO-Prover: neural theorem proving with growing libraries. External Links: 2310.00656, Link Cited by: §2.2. Wang et al. (2026) H. Wang, B. Huang, Y. Wan, X. Zhu, X. Liu, Y. Huang, and Z. Guo FormalRx: rectify and examine semantic failures in autoformalization. External Links: 2607.04655, Link Cited by: §2.3. Weng et al. (2025) K. Weng, L. Du, S. Li, W. Lu, H. Sun, H. Liu, and T. Zhang Autoformalization in the era of large language models: a survey. External Links: 2505.23486, Link Cited by: §2.3. Wijk et al. (2024) H. Wijk, T. Lin, J. Becker, S. Jawhar, N. Parikh, T. Broadley, L. Chan, M. Chen, J. Clymer, J. Dhyani, E. Ericheva, K. Garcia, B. Goodrich, N. Jurkovic, H. Karnofsky, M. Kinniment, A. Lajko, S. Nix, L. Sato, W. Saunders, M. Taran, B. West, and E. Barnes RE-Bench: evaluating frontier AI R&D capabilities of language model agents against human experts. External Links: 2411.15114, Link Cited by: §1, §2.4. Wu et al. (2022) Y. Wu, A. Q. Jiang, W. Li, M. N. Rabe, C. Staats, M. Jamnik, and C. Szegedy Autoformalization with large language models. External Links: 2205.12615, Link Cited by: §2.3. Xia et al. (2026) H. Xia, C. P. Gomes, B. Selman, and S. Szeider Agentic neurosymbolic collaboration for mathematical discovery: a case study in combinatorial design. External Links: 2603.08322, Link Cited by: §2.1. Xin et al. (2024) H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang DeepSeek-Prover: advancing theorem proving in LLMs through large-scale synthetic data. External Links: 2405.14333, Link Cited by: §2.2. Yan (2025) C. Yan An O~ Optimal differentially private pac learner for concept classes with VC dimension 1. External Links: 2505.06581 Cited by: Theorem 4.10. Yang et al. (2023) K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar LeanDojo: theorem proving with retrieval-augmented language models. In Advances in Neural Information Processing Systems, Vol. 36. External Links: 2306.15626, Link Cited by: §1, §2.2. Yao et al. (2023) S. Yao, J. Zhao, D. Yu, N. Du, I. Shafran, K. Narasimhan, and Y. Cao ReAct: synergizing reasoning and acting in language models. In International Conference on Learning Representations, External Links: Link Cited by: §1. Zhang et al. (2026a) Y. Zhang, J. Sun, H. Bi, C. Geng, W. Ma, Z. Li, and X. Si DreamProver: evolving transferable lemma libraries via a wake-sleep theorem-proving agent. External Links: 2604.26311, Link Cited by: §2.2. Zhang et al. (2026b) Y. Zhang, J. D. Lee, and F. Liu AI4SLT: empirical processes in Lean 4 for formal statistical learning theory. Note: Accepted at ICML 2026 External Links: 2602.02285, Link Cited by: §1, §2.2. Zhang et al. (2026c) Y. Zhang, Y. Sun, T. Suzuki, J. D. Lee, and F. Liu LeanMarathon: toward reliable AI co-mathematicians through long-horizon Lean autoformalization. External Links: 2606.05400, Link Cited by: §1, §2.3. Zhao et al. (2026) Z. Zhao, B. Yuan, J. Choi, and Y. Chen RMA: an agentic system for research-level mathematical problems. External Links: 2605.22875, Link Cited by: §2.1, §2.4. Zheng et al. (2026) D. Zheng et al. AI co-mathematician: accelerating mathematicians with agentic AI. External Links: 2605.06651, Link Cited by: §1, §2.1. Zheng et al. (2021) K. Zheng, J. M. Han, and S. Polu MiniF2F: a cross-system benchmark for formal olympiad-level mathematics. External Links: 2109.00110, Link Cited by: §2.4.