Cogentic: Multi-Agent Orchestration for Automated Proof Discovery

• Cogentic requires only a problem statement, runs autonomously, and targets natural-language proofs that experts can verify directly.The authors focus on problem domains within their own expertise.Source: §1 · p. 1
• Unlike approaches that search for mathematical objects using cheap, faithful, machine-computable scores, Cogentic produces natural-language mathematical prose for expert verification.The paper notes that not every problem is amenable to object-search approaches.Source: §1 · p. 2
• Cogentic frames proof discovery as iterative interaction between provers and adversarial verifiers that initially treat proof steps and citations as unverified.The paper situates this approach among inference-budget scaling and multi-agent interaction methods.Source: §1 · p. 2
• The authors target open questions at the hardness level of flagship theoretical computer science conferences, using O(100) to O(1000) Gemini calls per problem.Most problems used O(100) calls and the hardest used O(1000).Source: §1 · pp. 1–2

2. The Harness

• The harness coordinates literature reviewers, an orchestrator, parallel provers, verifiers, an advisor, and a consolidation stage around a shared workspace.The orchestrator allocates prover slots and tracks global state but does not perform mathematical derivations.Source: §2 · pp. 2–3, Figure 1 · p. 3

2.1. Directions and Assignments

• The orchestrator assigns each prover a research direction, while independent briefings summarize prior attempts and suggest next steps from what has and has not worked.A direction is a specific claim, a search for counterexamples, or later repair and finalization of a promising proof.Source: §2.1 · p. 4

2.2. Verification

• A proof is accepted only after both an individual verifier and a separate verifier comparing all drafts from that round approve it.Both verifiers begin by treating steps and citations as incorrect until justified or checked.Source: §2.2 · p. 4

2.3. Cross-Round Communication

• Each round records attempted methods and objections, while the verified ledger preserves confirmed lemmas and dead ends for later rounds.Lemmas extracted from otherwise rejected proofs are verified again in isolation before entering the ledger.Source: §2.3 · p. 4

2.4. Process Level Adaptation

• A process advisor reviews verification logs across rounds and recommends changes to instructions and prover allocation, without offering a mathematical opinion.It surfaces recurring mistakes, argument gaps, and verification blind spots.Source: §2.4 · pp. 4–5

2.5. Termination and Output

• After verification clears, the system may explore remaining promising directions; it then selects the strongest verified proof, expands it into a manuscript, and audits it against the accepted proof.The output is a self-contained document intended for domain experts unfamiliar with the run.Source: §2.5 · p. 5

3.1. Efficient Online Inverse Linear Optimization

• O(d) cumulative shortfall is achievable uniformly over the horizon by a deterministic, proper, anytime algorithm using O(d^2) arithmetic and one linear optimization per round.The paper describes this as the first efficient bound of this order and the first proper one.Source: §3.1 · p. 6

3.2. Competition Complexity for Two-Sided Markets

• Two added sellers on the smaller side suffice for Seller Trade Reduction to match the original market’s first-best gains from trade; one seller is insufficient even when m=n=1.This reduces the earlier requirement of at least 20,000 additional agents per side to two on one side.Source: §3.2 · p. 7

3.3. Anytime Regret with 𝑛Experts

• As n→∞, anytime regret’s leading constant matches fixed-time regret’s; a horizon-free algorithm achieves the bound for every loss-vector sequence, and the leading constant is optimal.The optimality claim follows because an anytime algorithm is also a fixed-horizon algorithm at every T.Source: §3.3 · p. 8

3.4. Simple versus Optimal Revenue for an Additive Buyer

• 3.52: OPT is at most 3.52 · max(SRev, BRev) for a single additive buyer with independent item values.Source: §3.4 · p. 8

3.5. Price of Anarchy for Autobidding Auctions

• 1.5: pFPA1 has tight PoA 1.5 for two bidders; for n≥2, pFPA2n achieves PoA at most 2−Ω(1/n), matching the lower bound up to constants.The two-bidder tightness is stated for anonymous mechanisms with mild assumptions.Source: §3.5 · p. 9

4. Discussion

• The problems came from the authors’ areas of expertise, and some companion-paper coauthors had already been working on them.Domain experts verified the natural-language proofs.Source: §4 · p. 10
• The authors checked arguments, wrote the exposition, and sometimes developed results further than the harness had.Source: §4 · p. 10
• The initial papers were coherent and readable, but the authors added literature placement, framing, and explanation of the techniques.Source: §4 · p. 10
• Candidate results can be generated faster than they can be read, and that gap widens as the compute budget grows.Formalizing proofs could settle correctness mechanically, but human understanding might still lag; balancing throughput and understanding remains an open question.Source: §4 · p. 10

A.1. Efficient Online Inverse Linear Optimization

• A.1 asks for a cutting-plane algorithm with regret polynomial in d and independent of horizon T.Source: §A.1 · p. 15

A.2. Recruiting Two Traders Suffices for Two-Sided Markets

• A.2 asks whether adding two sellers lets Seller Trade Reduction match the original market’s first-best GFT, assuming buyer values first-order stochastically dominate seller costs.The prompt specifies m ≥ n ≥ 1.Source: §A.2 · p. 15

A.3. Anytime Algorithm for Prediction with Expert Advice

• A.3 asks how anytime regret scales with n experts and whether the price of anytime tends to 1 as n tends to infinity.Source: §A.3 · p. 15

A.4. Selling Separately vs. Bundling

• A.4 poses proving that the better of separate item sales and grand bundling earns at least one-third of optimal revenue for an additive buyer with independent item values.Source: §A.4 · p. 16

A.5. Autobidding

• The prompt introduces a two-bidder mechanism in which bidder i wins with probability b_i/(b_1+b_2), and asks whether its price of anarchy (PoA) is 1.5.Source: §A.5 · pp. 16–17
• A.5 notes that the setting beyond two bidders remains open and asks reviewers to understand the PoA lower bound as a function of n.Source: §A.5 · p. 17
• A.5 asks for an n-bidder mechanism whose PoA approaches the lower bound, allowing dependence on n but not on values or costs beyond bids.The prompt gives 2 − O(1/n) as an example target when the lower bound is 2 − Ω(1/n).Source: §A.5 · p. 17