VALG Tracks Theorem Rewrites With Typed Proof Graphs; Only 2 of 9 COLT Open Subproblems Retain Their Original Scope

[VALG](https://arxiv.org/abs/2608.13060) attempts to address a step that formal-proof agents typically avoid: when a research problem has not yet been fully formalized, how can an agent modify assumptions and theorem targets without quietly replacing the original problem along the way? The system first retrieves relevant literature, creates branches from different research perspectives, and then fixes each viable idea into a “theorem contract” containing a data model, learner, oracle, loss, quantified conditions, and a single target.

Once the proof stage begins, VALG represents the argument as a typed directed acyclic graph: source nodes are the original assumptions, intermediate nodes are lemmas, and the sole sink is the target theorem. A global checker first verifies that node interfaces, probability and convergence modes, parameter dependencies, and proof closure are compatible. Local agents then complete derivations in dependency order, after which independent reviewers assess structure, rigor, citations, and edge cases and combine their judgments. If a failure is confined to one derivation, only that section is redone; if the proof architecture is invalid, the graph is rebuilt; and only when the theorem itself is blocked does the system create a restricted or relaxed version explicitly linked to the original problem.

The authors evaluated VALG on nine subproblems drawn from five COLT 2026 open-problem papers, covering tensor decomposition, 1-bit mean estimation, deep and linear models, differentially private learning, and online optimization. Across nine runs, the system retained 22 internally finalized theorem candidates. Only two runs produced candidates within the scope of the original research brief; the rest were special cases, restricted methods, or conditional theorems. That proportion is itself an important signal: an agent’s ability to maintain an auditable research trail does not mean it can generally solve open problems.

The [open-source implementation](https://github.com/DechenZhang/VALG-ML-Theory-Agent) is built from Codex skills, sub-agents, and file-based intermediate artifacts, and supports both human-approval and autopilot modes. Engineering and research teams should next examine whether the candidates withstand independent expert review or formalization in proof assistants such as Lean. For now, “internally finalized” still refers only to the system’s own review outcome and should not be treated as a new theorem validated by the academic community.