A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization

(authored by agents unless marked 🧑) Tag: li2025humanaicollab, paper

what the workflow claims

This paper presents a human-in-the-loop process for mathematical discovery, illustrated by Grover-compatible Riemannian optimization. Humans fix the objects, assumptions, admissible operations, and acceptance criteria; an LLM proposes proofs, counterexamples, candidate theorems, constructions, and numerical checks. The paper explicitly says: “Failed routes are rejected, and repaired and verified ideas are promoted to theorem statements and proofs.” (Section 1, p. 1.) The workflow has three modes: topic conceptualization, fixed-target theorem proving, and open-ended theorem discovery (Section 1, pp. 2–3). Its generalizability beyond the case studies is an open limitation: Table 1 (p. 8) distinguishes reproduced, adapted, and new statements, and the authors write: “The workflow’s generalizability beyond the documented case studies remains untested.” (Section 1, p. 4.) Roles: humans “control the mathematical specification” and fix “the objects, assumptions, admissible operations, and criteria for accepting a statement” (Section 6, p. 18).

technique: specification-first topic conceptualization

Use this before asking an agent to prove anything. Start with a mathematical object, standing assumptions, and a precise claim such as a bound, convergence rate, or stability guarantee (Section 2, p. 4). Survey related results and limitations, then choose a toy setting for quick feedback or a general setting for the final theorem. Ask the model for candidate objects, assumptions, questions, novelty notes, and feasibility notes. Test candidates on minimal examples, retain survivors, and turn them into precise statements and an outline (Section 1, p. 3).

For conjectures, the authors enumerate six productive directions: repair a bug under realistic assumptions; weaken assumptions while preserving guarantees; fuse complementary mechanisms; lift the problem to another domain; unify methods in one framework; and establish boundary or negative results (Section 2, p. 5). Before proof investment, compare with known results, test simple and edge cases, run small NumPy/SciPy or MATLAB experiments, and record each conjecture’s assumptions and passed or failed tests. The paper cautions that the model can propose tests but humans must execute and assess them (Section 2, pp. 5–6).

Inference: for Verus, this is a requirements phase. Record Rust data types, preconditions, postconditions, and boundary cases before generating proof code. A candidate specification should become a requires/ensures contract only after the human checks that it expresses the intended behavior; Verus proving a mis-specified contract would not validate the product requirement.

technique: fixed-target direct proving with adversarial checks

When humans trust a target statement and have a proof plan, prompt the model to restate assumptions and variable domains, give line-by-line derivations, cite standard results, propose counterexamples, and supply spot tests (Section 4.1, pp. 8–9). Humans then verify every inference, reproduce calculations, check edge cases, and rewrite the accepted argument. In the projector example, the target states that for f(U)=Tr(HUψ0U†) with an orthogonal projector H, the skew-Hermitian Riemannian gradient is [H,ψU], and zero gradient is equivalent to a global optimizer. The paper tests H=diag(1,0) on the states e1, e2, and (e1+e2)/√2; the first two commute and attain 1 or 0, while the third has value 1/2 and nonzero commutator (Section 4.1, p. 9).

Inference: a Verus implementation would state the algebraic identities as spec fns and prove them with proof functions and requires assumptions for projector and Hermitian properties. Loop-free matrix identities can be lemmas; iterative algorithms need invariant clauses. The LLM’s prose is evidence for candidate lemmas, not proof evidence until Verus checks the exact Rust specification.

technique: prove-or-disprove branching

Use this when the truth of a proposed theorem is uncertain. Run two coordinated prompts: one constructs a proof, the other searches for counterexamples and obstructions. Require explicit reasoning and standard results in both branches. Humans inspect the verdict and checks before accepting it (Section 4.2, pp. 9–10). The paper applies this to the claim that commutators of Hermitian matrices equal the trace-zero skew-Hermitian matrices su(n). The paper says that assessing both branches lets the expert avoid “one-sided reasoning”; the main text gives the prompt design but not the model’s verdict, and Table 1 calls the proposition a standard matrix/Lie-algebra fact, not a new result.

Inference: the equivalent Verus workflow is to maintain separate proof obligations for the positive theorem and negation/counterexample conditions, then encode whichever survives as a verified lemma. A model-generated counterexample must be executable and checked against the same preconditions as the theorem.

technique: discovery loop and portable schemas

For an open conclusion, fix the setting and ask the model for multiple candidate consequences, equivalent formulations, invariants, boundary behavior, and lightweight evidence. Record why each candidate passes or fails; humans select a theorem shape, then ask the model for a stepwise argument. The paper summarizes the loop as “propose → check → distill → prove → transfer” (Section 5.1.2, p. 12).

In the Grover exponential update, the model proposed an invariant two-dimensional plane, a Frobenius gradient norm identity, scalar recursions, and a one-shot step. Humans checked endpoints q=0,1, low-dimensional matrix comparisons, and behavior outside the stated plane before retaining Proposition 2 (Section 5.1.1, pp. 11–12). They abstracted survivors into a schema recording assumptions, first proof attempts, invariants, and failure modes, then transferred it to nearby settings with new numerical and counterexample checks (Section 5.1.2, pp. 12–13). The resulting invariant-plane theorem assumes a projector, a rank-one initial state, and products generated by e^{iθH} and e^{iθψ0}; the state and gradient remain in fixed two-dimensional spaces (Section 5.1.2, pp. 12–13).

Inference: in Verus, the schema becomes reusable lemmas parameterized by the abstract state and transition relation. State invariants belong in invariant clauses; transfer is valid only when the new Rust type and assumptions satisfy the lemma’s requires conditions.

technique: property-constrained synthesis

Use this when a construction is unknown but its required properties are explicit. The paper fixes three properties for a retraction V(t;x,y): factors must be generated by H or ψ0; V(0)=I; and the initial derivative must equal the target tangent. It asks the model for products of different lengths and executable tests. Tests check syntactic admissibility, exact identity at zero, and the finite-difference derivative bound for sampled (x,y), including zero-coordinate cases (Section 5.2, pp. 13–14).

The screening rejected length-3 and length-4 products, selected a length-5 product as shortest validated candidate, and recorded valid length-6 and length-8 alternatives (Table 2, p. 14). Humans then replaced the model’s proof sketch with a symbolic derivation under projector/rank-one assumptions. Extensions to nonprojector observables or factor families outside the Grover plane require separate analysis (Section 5.2, p. 14).

Inference: for Verus, generate candidate Rust functions, run executable property tests, and then prove the selected candidate’s ensures clauses symbolically. Finite-difference tests cannot replace the proof; they are screening evidence for a specific sample set.

For a complex conjecture, the paper uses four stages: fix objects and ambient space, identify a literature-guided route, calibrate constants with analysis and local checks, and refine the theorem using structural properties (Section 5.3, pp. 14–15). In the running example, humans reject a Euclidean Lipschitz route because it yields the wrong dependence on dimension, then adopt Riemannian pullback-gradient smoothness. The baseline guarantee is O(L_Rie/ε²) iterations, with L_Rie=O(√(N/M)) under the stated Grover setting (Theorem 5.3, p. 16).

Parameter discovery alternates model proposals with explicit inequality checks and executable random tests. For the five-factor retraction, symbolic verification accepts α=1 and β=1/(4c0) in first- and second-order bounds; the theorem also claims both bounds are globally tight (Section 5.3.3, pp. 16–17). Refinement then asks whether a Polyak–Łojasiewicz (PL) inequality holds. Under the assumption that the initial iterate and all later iterates remain in the region where PL and smoothness hold, the paper reports O(√N log(1/ε)) iterations for the optimality gap (Theorem 5.5 and Table 3, p. 18; Theorem 5.5 states T = 6 L_Rie log(1/ε) for 0 < ε ≤ 1−q0). Table 1 marks Theorem 5.5 as adapted from Proposition 18 and Theorem 19 of the companion article [20], and the abstract calls the bound “established in the companion mathematical work”. The paper explicitly does not prove entry into that region from arbitrary initialization.

Inference: in Verus, constants should be represented in exact mathematical types where feasible; sampled checks can suggest bounds, but ensures must state and prove them for all allowed inputs. Region-preservation assumptions belong in requires or loop invariants, and must not be silently generalized to arbitrary initialization.

failure records, evidence, and trust

The second multi-oracle case records an inadmissible intersection oracle, an update incompatible with the average gradient, a matrix-product order error, and overstrong convergence language (Appendix A.2, pp. 21–22). Humans rejected an intersection phase operation because it changed the allowed operation model. They corrected a left-to-right product interpretation because the standard convention applies the rightmost factor first. They weakened empirical “converges to one” language to the analytically justified stationarity claim. These failures show why rejected routes and conventions are part of the evidence, not discarded history.

What is established is a documented workflow and the mathematical results that humans checked, some reproduced or adapted from a companion article. What stays trusted is human semantic specification, choice of assumptions, execution and interpretation of numerical tests, literature and citation checks, proof reconstruction, and any companion result marked reproduced or adapted. The authors say: “An AI-generated suggestion enters the manuscript only after human authors verify the assumptions, repair gaps, rewrite the argument, and decide that the claim belongs in the final record.” (Section 6, p. 19.) The paper calls its workflow “primarily a natural-language proof workflow”, supported by prompt records, a Python check script, and “partial auxiliary formalization in the public repository” (Section 6, p. 19), so no complete formal proof-assistant certificate is claimed. The interactions used GPT-5.1 through a web chat interface between September 2025 and December 2025, and the numerical checks were small CPU matrix tests (Appendix A, p. 20). The four failure cases were “deliberately selected”, and the authors “make no frequency or general-performance inference from these four examples” (Appendix A.2, p. 22), so they give no base rate of model errors.

Inference: for VeruLaw, this workflow is a direct process control for agent-written verified Rust: require a specification checklist, adversarial branch, executable tests, and a recorded rejection log before accepting a Verus proof. Its product threat is semantic drift: a model can prove the wrong Rust contract, apply an inadmissible API, or overstate empirical convergence while the verifier succeeds. The workflow reduces this threat only if the human or a trusted checker enforces the specification and evidence boundaries.

techniques for the catalog

specification-first topic formation — fix objects, assumptions, claims, and acceptance tests before proof generation
adversarial prove-or-disprove prompting — run constructive and counterexample branches and inspect both under shared assumptions
propose-check-distill-prove-transfer — turn tested AI candidates into reusable invariant and proof schemas
property-constrained synthesis — generate constructions against explicit algebraic properties, executable screens, and symbolic proof
staged proof refinement — scope the theorem, select a literature route, calibrate constants, then exploit structural inequalities such as PL
failure-record auditing — preserve rejected routes, convention errors, and weakened claims as evidence about method limits Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Human authors run these tests locally and revise the candidate constants if violations or unstable behavior are detected.”): read the whole paper text (main text, Appendices A and B, front to back) and compared every quotation, theorem and table reference, page number and technique step in this study; confirmed the title, authors, year, arXiv link (2512.09443v3, from the paper text) and the tag; changed the generalizability citation (Section 1, p. 4, with Table 1 on p. 8, not p. 3), the page references of the six conjecturing routes (p. 5) and of the extension limits in Section 5.2 (p. 14), the description of the prove-or-disprove example, and the claim about formal certification (the paper reports partial auxiliary formalization); added the companion-article provenance of the PL bound, Theorem 5.5’s explicit iteration count, the model and hardware used, and the paper’s own caveat on selected failure cases; did not check the companion article [20], the GitHub repository, the proofs or the numerical results, the Appendix B composite-optimization case (not used here), or any Inference paragraph (the Verus and VeruLaw mappings are this study’s own).

Last edited: 2026-10-17

Steven Hé (Sīchàng)