Banger paper from Google Research on multi-agent proof discovery.

(bookmark it)

It’s really interesting to see this emerging multi-agent pattern: not enforcing too much execution structure and pairing it with dedicated agents for advising and verification.

I think it is generally applicable as well. Great read.

Here is how it works:

Cogentic runs on Gemini and works on open problems in theoretical computer science, starting from the problem statement with no expert hints.

The system works in rounds, and the orchestrator decides how many provers to run in each round. Every prover gets one direction to work on, such as a specific bound or a counterexample search, plus a short briefing that a summarizer agent writes from earlier attempts and verifier feedback. Each summarizer writes its briefing independently, so provers in the same round read different summaries of the same history.

Each draft goes through two adversarial verifiers. One checks the draft on its own, and the other reads all of the round’s drafts side by side to catch shared mistakes. A draft is accepted only if both pass it.

The agents share state through two disk documents. A record logs every attempt with the objection it failed on, and a ledger stores verified lemmas and ruled-out directions. An auditor extracts correct lemmas from rejected proofs, verifies them again independently, and adds them to the ledger.

A separate process advisor reads the verification logs across rounds and updates the instructions given to provers and verifiers. The orchestrator and the advisor can’t give mathematical opinions, so the provers provide all the math.

It produced new results on five open problems in online learning, auction theory, and mechanism design, each checked by domain experts. Most problems took around 100 Gemini calls, and the hardest took around 1,000.

Paper: https://arxiv.org/abs/2609.40324

Chat with Paper: https://academy.dair.ai/papers/cogentic-multi-agent-orchestration-for-automated-proof-discovery-2609.40324…

Cogentic: Multi-Agent Orchestration for Automated Proof Discovery

Source: https://arxiv.org/html/2609.40324 \uselogo

Vineet GuptaAffiliation:Google ResearchYanchen JiangAffiliation:Google ResearchChristopher LiawAffiliation:Google ResearchAranyak MehtaAffiliation:Google ResearchGrigoris VelegkasAffiliation:Google ResearchDi WangAffiliation:Google Research

Abstract

We present Cogentic, a multi-agent harness for automated proof discovery on open research problems. While frontier language models can generate strong mathematical ideas in a single shot, single-shot generation is often insufficient for open problems that require exploring multiple competing conjectures, overcoming subtle technical obstructions, and retaining intermediate progress over a long horizon. Cogentic addresses these challenges through an iterative prove–verify loop in which an orchestrator allocates a population of independent provers across distinct proof directions, subjects their output to adversarial verification by several specialized components, and promotes confirmed intermediate results into a persistent verified ledger that later rounds build on. The harness is designed to be able to solve research-level math and theoretical computer science problems. Using Gemini as the base model, Cogentic produced novel results on five open problems across online learning, auction theory, and mechanism design. Each result was independently verified by domain experts and is developed in full in companion papers. We list these results, and new ones as they are verified, athttps://sites.google.com/view/cogentic.

keywords

multi-agent orchestration, automated proof discovery, LLM reasoning, adversarial verification, inference efficiency

††footnotetext:The following authors have additional affiliations beyond Google Research: Yang Cai (Yale University) and Vineet Gupta (Google DeepMind).## 1Introduction

We introduce Cogentic, a multi-agent harness for proof discovery on open research problems. Inspired by our own experience conducting research in theoretical computer science and mathematics, the harness divides the work like a research group would: an orchestrator decides what gets worked on, provers draft proofs in parallel, and verifiers read those drafts looking for potential issues. We found that our system is quite efficient: The results reported here were based on Cogentic runs which usedO⁡(100)O(100)calls to Gemini for most problems, andO⁡(1000)O(1000)for the hardest. The system has headroom for further optimization of the number of calls but also allows for naturally scaling up to solve harder problems. A key feature of the system is that it only needs a problem statement, without any expert hints, and can work autonomously until it produces a result in the form of a paper. To evaluate the harness, we focus on problem domains within our own areas of expertise, targeting natural-language, human-readable proofs where we can directly verify the mathematical reasoning and provide exposition surrounding the background of the paper and the novel techniques that the system generates.

Interactive theorem provers — Lean(Moura and Ullrich, 2021), Isabelle/HOL(Nipkow et al., 2002), Coq(Castéran and Bertot, 2004)— provide machine-checked guarantees, and a substantial line of work uses language models to lower the cost of obtaining them: retrieving premises and generating tactics(Yang et al., 2023), drafting an informal proof and compiling it into a formal sketch(Jiang et al., 2022), and training for olympiad-level formal reasoning with reinforcement learning(Hubert et al., 2026). More recently the same machinery has been used on open research problems(Tsoukalas et al., 2026). In contrast, Cogentic operates in natural language, producing mathematical prose that domain experts can verify.

A distinct and highly successful line of work uses language models to search for mathematical objects rather than for arguments. Program search has discovered new constructions in extremal combinatorics(Romera-Paredes et al., 2024), evolutionary coding agents have improved algorithms and bounds(Novikov et al., 2025), and related systems perform test-time learning on open problems(Wang et al., 2025;Yuksekgonul et al., 2026)or explore many problems at once(Georgiev et al., 2025). Neuro-symbolic search attains medal-level performance in olympiad geometry by pairing a learned proposer with a symbolic engine(Trinh et al., 2024). The same recipe extends beyond mathematics to writing expert-level empirical research software under a quality metric(Aygün et al., 2026). What each of these approaches requires is a cheap, faithful, and machine-computable score. Sometimes theorems can be proven by reducing the question to finding mathematical structures with certain properties: e.g.,Nagda et al. (2026)found proofs of inapproximability for combinatorial problems by finding extremal structures, and(Cai et al., 2026f)found bounds on gain from bilateral trade by finding extremal probability distributions, both using AlphaEvolve(Novikov et al., 2025)with such oracles. However, not every problem is amenable to such an approach.

A second line of work is based on scaling the LLM inference budget, perhaps through multiple model calls, to solve more complex tasks. The base case is simply to sample more — chain-of-thought prompting(Wei et al., 2022), self-consistency across sampled solutions(Wang et al., 2022), and repeated sampling with a selector over the candidates(Brown et al., 2024;Snell et al., 2024). Another approach is to scale the inference via multi-agent interaction. Debate between instances has been reported to improve factuality and reasoning(Du et al., 2024;Liang et al., 2024), and models have been used to evaluate the work of other models(Zhuge et al., 2024). Our framework builds on an iterative interaction between provers and verifiers. The verifiers are adversarial and begin with the assumption that the proofs are incorrect or incomplete. We explain our framework in more detail in Section2.

There are several recent works that apply agentic harnesses to research-level mathematics and theoretical computer science. We do not attempt to give a comprehensive survey or compare these efforts, but they include(Feng et al., 2026;Lin et al., 2026;Schmitt et al., 2026;Zheng et al., 2026;Gottweis et al., 2026).

Finally, we place our contributions against recent milestones obtained with large agentic systems, including the resolution of a Millennium Prize problem(OpenAI, 2026b)and other long-standing mathematical conjectures(OpenAI, 2026a;Anthropic, 2026). We focus on problems in our areas of expertise, at the hardness level of open questions in flagship theoretical computer science conferences like STOC and FOCS, using a relatively low inference budget,O⁡(100)O(100)toO⁡(1000)O(1000)Gemini calls per problem.

2The Harness

Cogentic consists of a group of agents working on a single problem. They share a workspace on disk and are coordinated by an orchestrator that decides which of them runs, when, and on what.

Components.

We outline the main components of our system below.

• •Theorchestratorserves as the central controller: it tracks global state, partitions prover slots across research directions, spawns summarizers to condense history into targeted briefings for individual provers, evaluates verifier consensus, and manages ledgers that store important findings obtained so far and records that track prior proof attempts and their verdicts. The orchestrator does not perform mathematical derivations itself.
• •Literature reviewerssearch for related work and retrieve information such as definitions and theorems that a prover is likely to need. They can also be sent out again mid-run to do a more targeted search and find results that can help overcome ongoing technical barriers.
• •Proversgenerate candidate proofs independently and in parallel based on assigned briefings that selectively summarize findings obtained so far.
• •Verifierscritique candidate solutions from complementary angles and scopes.
• •Therecordkeeps track of prover attempts and their corresponding critiques from verifiers, and theledgerkeeps track of verified intermediate lemmas that came out of proof attempts. These are the central ways that our agents communicate and document progress, as explained in more detail below.
• •Anadvisorreads outputs across rounds to help the orchestrator decide how to control and allocate prover attempts and what to adjust the instructions given to each individual prover for the next round.
• •Finally, aconsolidation stageformats and audits the final manuscript.

Workflow.

The work proceeds in rounds (Figure1). A round produces a batch of candidate proofs, puts them through verification, and writes into the record and the verified ledger that the next round starts from. Rounds continue until a draft clears verification or until the budget runs out.

Figure 1:One round of Cogentic. The orchestrator decides how many provers to run and which direction each attends to, an advisor writes each prover an individual briefing, the provers draft candidate proofs in parallel, and every draft is verified both on its own and alongside the others from the round. What a round establishes is written down for subsequent rounds: the attempts and why they failed, the verified ledger of intermediate results, and the standing instructions maintained by the process advisor. Literature reviewers supply background at the start and can be dispatched again mid-run when attempts stall at the same step. Rounds continue until a draft clears verification after which the accepted proof is consolidated, expanded into a formal manuscript, and audited.

2.1Directions and Assignments

A round opens with the orchestrator planning the work: how many provers to run, and what direction each should attend to. A direction here is a specific claim (e.g., a bound, a constant, a construction), finding counterexamples, or as the run goes on, repairing and finalizing promising proofs. A prover is assigned to a direction to work on, but not how to work on it. It reads what has been attempted previously for that direction, what the verifiers said about those attempts, as well as common information like the literature survey and the verified ledger, and chooses its own next step.

As the run goes on, the material relevant to a prover grows in volume. Rather than passing all of it as input, each prover sees only a briefing, written for it by a summarizer, which is spawned by the orchestrator. The summarizer reads all prior attempts and their verdicts, selects the most informative ones as context, and gives suggestions for possible next steps, based on what has worked and what has not. Each summarizer produces its briefing independently, so provers in the same round receive different readings of the same history. Longer documents are given as paths rather than quoted in full, so a prover (which itself is an agent, such as an Antigravity agent(The Antigravity Team, 2025)) can open what it wants to read selectively.

2.2Verification

After each prover completes a proof, it is read by a verifier whose task is to check the correctness of the proof. A separate verifier reads all of the round’s drafts side by side, which allows it to spot shared blind spots and compare the strengths of individual proofs. A draft is accepted only when it passes both verifiers. Both are adversarial: they start from the assumption that every step is wrong until justified, and that every citation is incorrect until checked.

2.3Cross-Round Communication

Each round leaves two artifacts: a record of what was tried, and a ledger of results that have been verified. Therecordpools attempts by what they were trying to establish, storing with each one the method used and the objection it failed on. The orchestrator and advisor read the record and decide what the next round should do.

Theledgeraccumulates confirmed fragments, such as intermediate lemmas, across rounds. Verifiers often confirm individual lemmas inside proofs they otherwise reject. At the end of a round, an auditor extracts those fragments, rewrites each as a self-contained lemma, and sends it to be verified again in isolation. What survives becomes available to every later prover as something that may be reused without being proved again. The ledger also records dead ends, for example, a bound excluded by a verified counterexample is written down as excluded, so that later rounds do not revisit them.

2.4Process Level Adaptation

At the end of each round, a process advisor reviews verification logs, not only from the current round but from the run as a whole, to adjust how subsequent rounds are conducted. It surfaces patterns that become visible over time: repeated mistakes, common gaps in arguments, recurring verification blind spots where one verifier missed but was caught by some other verifier, etc. Based on these observations, it recommends adjustments to the instructions given to provers and verifiers — for example, a warning about a mistake several provers keep making, or a stricter justification standard for the kind of step where earlier drafts cut corners. It also advises the orchestrator on how to allocate prover attempts and how to adjust the instructions given to each prover and verifier for the next round. This is a separate agent because the orchestrator, which must juggle concurrent duties across many agents, rarely has the context window to review and synthesize log trends itself. Note that, neither the advisor nor the orchestrator is permitted a mathematical opinion: they cannot speculate on what the answer is likely to be, recommend a technique, or declare a direction promising or dead.

2.5Termination and Output

When a candidate clears all verification, the orchestrator may continue to explore some remaining promising that may yield a better result, terminating once those avenues are exhausted. Upon termination, a comparator selects the strongest verified proof, a formal writer expands it into a complete manuscript, and a final verification audit checks the compiled document against the accepted proof to ensure no errors were introduced during exposition. The output is a self-contained document that states the theorems and the proofs, with the lemmas it depends on, notation, and background of the problem written out in full, so that it can be read and checked by domain experts who knows nothing about the run that produced it.

3Results

We applied Cogentic using Gemini to open research problems across online learning, auction theory, and mechanism design. The problems are in the areas of the research expertise of the authors. Each run operated from the problem statement without human mathematical intervention; domain experts subsequently verified every proof. Table1summarizes the five results, which are developed in full in companion papers. We maintain an up-to-date list of results obtained with Cogentic, with links to their companion papers, athttps://sites.google.com/view/cogentic.

Table 1:Open problems resolved or improved by Cogentic. Each result is developed in full in a companion paper; seehttps://sites.google.com/view/cogenticfor updates.### 3.1Efficient Online Inverse Linear Optimization

In online inverse linear optimization, a learner watches an expert make choices and tries to make the same ones without ever being told what the expert is optimizing. A vectorw∗w^{*}in the unit ball𝔹⊆ℝd\mathbb{B}\subseteq\mathbb{R}^{d}is fixed and hidden. At each round an adversary reveals a compact action setXt⊆𝔹X_{t}\subseteq\mathbb{B}, the learner recommends somex^t∈Xt\hat{x}_{t}\in X_{t}, and then observes the expert’s choicext∈arg⁡maxx∈Xt​⟨w∗,x⟩x_{t}\in\arg\max_{x\in X_{t}}\langle w^{*},x\rangle. It does not seew∗w^{*}or the value of any action. The learner is charged the cumulative shortfallRT=∑t≤T⟨w∗,xt−x^t⟩R_{T}=\sum_{t\leq T}\langle w^{*},x_{t}-\hat{x}_{t}\rangle, a sum of non-negative terms, and the question is whether that sum can be bounded by a function ofddalone, uniformly inTT.

A bound uniform inTTis stronger thanO⁡(T)O(\sqrt{T})orO⁡(d​ln⁡T)O(d\ln T), both of which let the total grow without bound. And a learner isproperif it commits to a nonzero estimatew^t\hat{w}_{t}of the objective before seeing the menu and then recommends a maximizer of⟨w^t,⋅⟩\langle\hat{w}_{t},\cdot\rangle; a proper learner answers not only what to do but what it takes the expert to be optimizing, and its recommendation costs one linear optimization overXtX_{t}. The problem reduces to a cutting-plane game with a strong separation oracle, in which the learner queriespt∈ℝdp_{t}\in\mathbb{R}^{d}and an adversary who has seenptp_{t}returns a unit vectorvtv_{t}with⟨w∗−pt,vt⟩≥0\langle w^{*}-p_{t},v_{t}\rangle\geq 0; bounding the regret of that game suffices to boundsRTR_{T}.

Prior work left a gap between the two desiderata. For arbitrary action sets the best efficient bounds wereO⁡(d​ln⁡T)O(d\ln T), polynomial but growing with the horizon:Gollapudi et al. (2021)obtained this from a regularized center of gravity, andSakaue et al. (2025b)obtained it efficiently from an online Newton step, atO⁡(d2)O(d^{2})per round afterSakaue (2026a)removed the Mahalanobis projection. Bounds uniform inTTwere either exponential indd— the John ellipsoid rule ofGollapudi et al. (2021), atexp⁡(O⁡(d​log⁡d))\exp(O(d\log d))— or required extra structure on the action sets(Sakaue et al., 2025a;Oki and Sakaue, 2026). Whether a finitepoly⁡(d)\operatorname{poly}(d)bound was achievable at all was answered affirmatively byDewasurendra (2026), but by a rule that is neither proper nor efficient: it pools covers of the optimality-gap class across dyadic scales into a weighted vote whose finite implementation can involveTΘ⁡(d)T^{\Theta(d)}tests and requires nonconvex optimization over the action set, without committing to a linear objective before seeing the menu.

Theorem 1(Cai et al., 2026a).

There is a deterministic, proper, anytime algorithm for online inverse linear optimization with cumulative shortfallRT=O⁡(d)R_{T}=O(d), uniform in the horizonTT, usingO⁡(d2)O(d^{2})arithmetic and one linear optimization per round.

This is the first bound of that order that is efficient, and the first that is proper. It is within a factor ofO⁡(d)O(\sqrt{d})of the optimal bound: every algorithm suffersΩ⁡(d)\Omega(\sqrt{d})(Sakaue et al., 2025b).

The proof builds on the variable-metric framework ofSakaue et al. (2025b), in which the learner runs online gradient descent under a metricHtH_{t}that stretches along directions already queried. Two changes remove the logarithm. First, withgt=−vtg_{t}=-v_{t}, the rank-one metric updategt​gt⊤g_{t}g_{t}^{\top}isself-normalized, divided by the dual-metric lengthst=‖gt‖Ht−1s_{t}=\|g_{t}\|_{H_{t}^{-1}}of the observed direction. Second, thelogdetHt\log\det H_{t}potential — which bounds the total squared step length∑tst2\sum_{t}s_{t}^{2}but grows liked​log⁡Td\log T, and is the source of theln⁡T\ln Tin every earlier volumetric analysis — is replaced by the trace powertr(Ht−1/2)\operatorname{tr}(H_{t}^{-1/2}). That potential starts atdd, stays non-negative, and falls by at leastτ4​st2\tfrac{\tau}{4}s_{t}^{2}each round, whereτ=Θ⁡(1/d)\tau=\Theta(1/d)controls the metric update, so∑tst2≤4​d/τ=O⁡(d2)\sum_{t}s_{t}^{2}\leq 4d/\tau=O(d^{2}), independently of the horizon. With the iterate step sizeα=Θ⁡(1/d)\alpha=\Theta(1/d), the distance-contraction argument and the reduction then giveRT=O⁡(1/α+α​∑tst2)=O⁡(d)R_{T}=O(1/\alpha+\alpha\sum_{t}s_{t}^{2})=O(d).

The argument uses the expert’s optimality only to make each round legal, so the same bound holds when the expert merely does at least as well as the learner by its own criterion; this is the firstO⁡(d)O(d)bound competing against an expert that does not optimize. The companion paper also gives corruption-robust and rank-adaptive variants, and an application to convex minimization: anLL-Lipschitz convex function with a minimizer within distanceRRof the initial point can be minimized from subgradient directions alone with total suboptimalityO⁡(d​L​R)O(dLR)over an infinite run.

Subsequent to the companion paper,Sakaue (2026b)obtained a tightO⁡(d)O(\sqrt{d})bound. However, this algorithm is inefficient and it remains an open question to obtain an efficient algorith withO⁡(d)O(\sqrt{d})regret.

3.2Competition Complexity for Two-Sided Markets

The Bulow–Klemperer theorem(Bulow and Klemperer, 1994)establishes that in one-sided auctions, adding a single bidder to a simple mechanism yields at least the revenue of the optimal mechanism for the original market. A natural question is whether a Bulow–Klemperer-type result also holds for two-sided markets. This line of work was initiated byBabaioff et al. (2020a), who show that, when the buyers’ valuations first-order stochastically dominate the sellers’ costs, adding roughlyn⁡(m+4​m)n(m+4\sqrt{m})buyers suffices for a prior-independent mechanism to have gains from trade (GFT) at least that of the first-best GFT, wheremmis the number of buyers,nnthe number of sellers, andm≥nm\geq n. Following up on this,Cai et al. (2024)showed that if one augmentsbothsides of the market thenO⁡(1)O(1)agents suffice. Their analysis, however, requires a large constant, namely at least20,00020{,}000per side. At least two questions remained open, including (i) whether the constant can be improved and (ii) whether it is sufficient to recruit from only one side of the market.

Using Cogentic we proved the following theorem, which answers both questions simultaneously.

Theorem 2(Cai et al., 2026e).

For anym≥n≥1m\geq n\geq 1, if the buyer distributionFBF_{B}first-order stochastically dominates the seller distributionFSF_{S}, then adding exactly two sellers — the smaller side of the market — suffices for Seller Trade Reduction to achieve expected gains from trade at least the first-best gains from trade of the original market:

STR⁡(m,n+2)≥OPT⁡(m,n).\operatorname{STR}(m,n+2)\;\geq\;\operatorname{OPT}(m,n).Moreover this is tight: even form=n=1m=n=1, recruiting one additional seller does not suffice for any prior-independent mechanism.

The constant drops from at least20,00020{,}000per side to22on one side, and the recruitment is one-sided, so the mechanism designer need only find two more participants of the type already in shorter supply.

3.3Anytime Regret withnnExperts

In prediction with expert advice, a learner plays a distribution overnnexperts, an adversary reveals a loss vector in[0,1]n[0,1]^{n}, and the learner is charged its expected loss relative to the best single expert in hindsight. When the horizonTTis known, multiplicative weights tuned toTTguarantees regretT​ln⁡n/2\sqrt{T\ln n/2}, and the leading constant1/21/\sqrt{2}cannot be improved for largenn(Cesa-Bianchi et al., 1997). Ananytimealgorithm is given no horizon and must satisfy its bound at everyttsimultaneously. The best known anytime guarantee for many experts wast​ln⁡n\sqrt{t\ln n}, a factor2\sqrt{2}worse, and whether that factor was necessary had remained open. Forn=2n=2,Luo and Schapire (2014)proved that the anytime regret is strictly larger than the fixed-time regret obtained byCover (1966). Later,Harvey et al. (2023)gave the optimal anytime algorithm forn=2n=2but also conjectured that asn→∞n\to\infty, the leading constant of the anytime regret and fixed-time regret would coincide. Some evidence towards this conjecture was given byHarvey et al. (2024), who proved that in continuous time, the anytime and fixed-time constants agree asn→∞n\to\inftywhen the experts follow independent Brownian motions.

With the Cogentic framework, we prove that the leading constant of the fixed-time regret and anytime regret coincide asn→∞n\to\infty.

Theorem 3(Cai et al., 2026b).

There is an algorithm for prediction with expert advice which uses no knowledge of the horizon and whose regret overnnexperts satisfies

Rt≤(1+O⁡(ln⁡ln⁡nln⁡n))​t​ln⁡n2simultaneously for all​t≥1R_{t}\;\leq\;\left(1+O\!\left(\sqrt{\frac{\ln\ln n}{\ln n}}\right)\right)\sqrt{\frac{t\ln n}{2}}\qquad\text{simultaneously for all }t\geq 1for every sequence of loss vectors in[0,1]n[0,1]^{n}.

The leading constant is optimal, since an anytime algorithm is in particular a fixed-horizon algorithm at everyTT.

The proof Cogentic found is elementary. Run one multiplicative-weights instance for each horizon on a geometric gridHm=(1+ε)mH^{m}=(1+\varepsilon)^{m}and aggregate them with a master multiplicative-weights algorithm. At any timettsome instance is tuned to a horizon in[t,(1+ε)​t][t,(1+\varepsilon)t]and so has regret1+ε​t​ln⁡n/2\sqrt{1+\varepsilon}\sqrt{t\ln n/2}; it would suffice for the master to track that instance cheaply. The obstruction is that the pool grows withttwhile the master’s regret grows with the number of instances it tracks, which would leave a time-dependent overhead in the leading constant. The construction keeps the pool bounded by waking instancemmonly at round⌊δ​Hm⌋\lfloor\delta H^{m}\rfloorand retiring it after round⌊Hm⌋\lfloor H^{m}\rfloor. ThenO⁡(ε−1​log⁡δ−1)O(\varepsilon^{-1}\log\delta^{-1})instances are awake at once, independent oftt, and at most that many are born during any one instance’s lifetime. This second count matters because when new instances arrive, we must allocate some of the existing probability mass to new instances. Retirement leaves the prefix before⌊δ​Hm⌋\lfloor\delta H^{m}\rflooruncovered, and recursing on it contributes a geometric series1+δ+δ+⋯1+\sqrt{\delta}+\delta+\cdots. Takingε=ln⁡ln⁡n/ln⁡n\varepsilon=\sqrt{\ln\ln n/\ln n}andδ=ε3\delta=\varepsilon^{3}makes the grid coarseness, the aggregation overhead, and the recursion together cost a factor1+O⁡(ε)1+O(\varepsilon).

3.4Simple versus Optimal Revenue for an Additive Buyer

Consider a single buyer with additive valuations overnnitems whose values are drawn independently. LetSRev\operatorname{SRev}be the revenue from selling each item separately at a fixed price, andBRev\operatorname{BRev}the revenue from selling the grand bundle at a single price. LetOPT\operatorname{OPT}be the revenue of the optimal mechanism, which may be randomized and arbitrarily complex.Babaioff et al. (2020b)showed that the better of these two simple mechanisms is within a constant factor of optimal:OPT≤6⋅max⁡(SRev,BRev)\operatorname{OPT}\leq 6\cdot\max(\operatorname{SRev},\operatorname{BRev}). The duality framework ofCai et al. (2016)later extended this result to a more general setting. For the original single-additive-buyer setting,Ma and Simchi-Levi (2021)improved the factor to5.25.2. The optimal constant is still unknown, and the best lower bound on the approximation ratio is22(Rubinstein, 2016).

Theorem 4(Cai et al., 2026d).

For a single additive buyer whose values fornnitems are independent,

3.52⋅max⁡(SRev,BRev)≥OPT.3.52\cdot\max(\operatorname{SRev},\operatorname{BRev})\;\geq\;\operatorname{OPT}.

The proof builds on the duality framework ofCai et al. (2016). Letvjv_{j}be the buyer’s value for itemjj, and letV=∑jvjV=\sum_{j}v_{j},Mmax=maxj⁡vjM_{\max}=\max_{j}v_{j}, andM=max⁡{SRev,BRev}M=\max\{\operatorname{SRev},\operatorname{BRev}\}. The framework gives

OPT≤SRev+𝔼⁡[V−Mmax],\operatorname{OPT}\leq\operatorname{SRev}+\mathbb{E}[V-M_{\max}],so it remains to bound the expectednon-favorite welfare𝔼⁡[V−Mmax]\mathbb{E}[V-M_{\max}], i.e., the total value of all items except the buyer’s favorite.

Prior analyses truncate item values atSRev\operatorname{SRev}and split𝔼⁡[V−Mmax]\mathbb{E}[V-M_{\max}]into aCore\operatorname{Core}and aTail\operatorname{Tail}, each bounded separately(Cai et al., 2016). We instead truncate at the joint scaleMM, which also accounts forBRev\operatorname{BRev}, and show directly that

𝔼⁡[V−Mmax]≤𝔼⁡[VM],VM=∑j=1nmin⁡{vj,M}.\mathbb{E}[V-M_{\max}]\leq\mathbb{E}[V_{M}],\qquad V_{M}=\sum_{j=1}^{n}\min\{v_{j},M\}.This removes theTail\operatorname{Tail}analysis entirely and leaves a singleCore\operatorname{Core}-like quantity. We then derive extremal distributions that maximize and minimize the second-order moment bound𝔼⁡[VM2]\mathbb{E}[V_{M}^{2}], while keeping𝔼⁡[VM]\mathbb{E}[V_{M}]fixed. The upper and lower bounds then suggest a relationship between𝔼⁡[VM]\mathbb{E}[V_{M}]andMMthat allows us to bound𝔼⁡[VM]\mathbb{E}[V_{M}]by a constant multiple ofMM.

3.5Price of Anarchy for Autobidding Auctions

Automated bidding (autobidding) is now a widely adopted interface for advertisers to bid into high frequency ad auctions. In this interface, advertisers specify high level constraints, such as return-on-spend and budget constraints. To measure efficiency, the literature uses a standard metric known as the price of anarchy (PoA) which is the ratio of the welfare in the optimal allocation and the worst-case equilibrium welfare.Aggarwal et al. (2019)initiated this line of work, showing that the second-price auction (SPA) achieves a tight PoA of22. Subsequent work byLiaw et al. (2023)proved that no deterministic mechanism—including the first-price auction (FPA)—can beat the PoA barrier of22in the prior-free setting, even for two bidders. When randomization is combined with non-truthful payments, however, the barrier of22can be broken for two bidders:Mehta (2022)achieved a two-bidder PoA of approximately1.891.89via a randomized truthful auction, andLiaw et al. (2023)improved the two-bidder upper bound to1.81.8using a randomized first-price auction, while proving annn-bidderlower bound(for evennn) showing that every anonymous mechanism hasPoA≥2​n+4n+4=2−4n+4\mathrm{PoA}\geq\frac{2n+4}{n+4}=2-\frac{4}{n+4}. At least two questions remain open: (i) what is the exact minimax optimal PoA forn=2n=2bidders, and (ii) for generaln≥3n\geq 3bidders, whether any mechanism can break the deterministic PoA barrier of22and match the2−Θ⁡(1/n)2-\Theta(1/n)lower bound.

Using Cogentic we proved the following theorem, which answers both questions simultaneously using the family ofrr-Proportional First-Price Auctions (𝗉𝖥𝖯𝖠r\mathsf{pFPA}_{r}), in which each bidderi∈[n]i\in[n]wins a query with probabilityxi,j=bi,jr/∑k=1nbk,jrx_{i,j}=b_{i,j}^{r}/\sum_{k=1}^{n}b_{k,j}^{r}and pays their bidbi,jb_{i,j}upon winning (a bidder facing no competing bid wins for free).

Theorem 5(Cai et al., 2026c).

In prior-free autobidding markets with return-on-spend constraints:

1. 1.Forn=2n=2bidders, the standard Proportional First-Price Auction (𝗉𝖥𝖯𝖠1\mathsf{pFPA}_{1}, withr=1r=1) achieves a Price of Anarchy of at most1.51.5. Moreover, this is tight: any anonymous two-bidder mechanism (with mild assumptions) hasPoA≥1.5\mathrm{PoA}\geq 1.5.
2. 2.For generaln≥2n\geq 2bidders, the2​n2n-Proportional First-Price Auction (𝗉𝖥𝖯𝖠2​n\mathsf{pFPA}_{2n}, withr=2​nr=2n) achieves a Price of Anarchy of at most PoA⁡(𝗉𝖥𝖯𝖠2​n)≤2−14​n+1=2−Ω⁡(1/n).\mathrm{PoA}(\mathsf{pFPA}_{2n})\leq 2-\frac{1}{4n+1}=2-\Omega(1/n).This matches the2−4n+42-\frac{4}{n+4}lower bound up to constant factors in the1/n1/nterm.

In the second part of the theorem, the upper bound holds only assuming that bids are undominated (i.e. no bidder can raise their bid on any query to win more while satisfying their RoS constraint).

For the first part of this theorem, the authors had already suspected that the proportional first-price auction would have an improved Price of Anarchy over rFPA, and their conjecture was that the bound is1.51.5, but did not have a proof. Cogentic was able to prove both the upper bound and the lower bound for any mechanism. The authors had not previously studied the second part of the theorem and did not provide any hints to the system. It independently came up with the mechanism and analysis.

4Discussion

As noted, Cogentic produces natural language proofs which are verified by experts. That was possible because of how the problems were chosen: they come from areas the authors work in. Some companion papers include coauthors who had already been working on the corresponding problems. We checked the argument, wrote the exposition around it, and in some cases carried it further than the harness had. We note that the initial papers were coherent and nicely readable on their own, but we added further exposition such as better placement in the literature, the framing, and distilling and explaining the techniques.

A system like this can produce candidate results faster than they can be read, and the gap widens as the compute budget grows. One possibility is to formalize in a proof assistant such as Lean(Moura and Ullrich, 2021), so that correctness is settled mechanically. However, human understanding of the solution might lag behind. In the past, understanding the solution of a problem has also led to new directions and problems being explored. Balancing out the throughput of this generation and human understanding remains an important question.

References

• Aggarwal et al. (2019)Gagan Aggarwal, Ashwinkumar Badanidiyuru, and Aranyak Mehta.Autobidding with constraints.InInternational Conference on Web and Internet Economics, pages 17–30. Springer, 2019.
• Anthropic (2026)Anthropic.Learning more about claude’s mathematical capabilities.https://www.anthropic.com/research/riemann-zeta, August 2026.
• Aygün et al. (2026)Eser Aygün, Anastasiya Belyaeva, Gheorghe Comanici, Marc Coram, Hao Cui, Jake Garrison, Renee Johnston, Anton Kast, Cory Y McLean, Peter Norgaard, et al.An ai system to help scientists write expert-level empirical software.Nature, pages 1–3, 2026.
• Babaioff et al. (2020a)Moshe Babaioff, Kira Goldner, and Yannai A. Gonczarowski.Bulow-klemperer-style results for welfare maximization in two-sided markets.In Shuchi Chawla, editor,Proceedings of the 2020 ACM-SIAM Symposium on Discrete Algorithms, SODA 2020, Salt Lake City, UT, USA, January 5-8, 2020, pages 2452–2471. SIAM, 2020a.10.1137/1.9781611975994.150.URLhttps://doi.org/10.1137/1.9781611975994.150.
• Babaioff et al. (2020b)Moshe Babaioff, Nicole Immorlica, Brendan Lucier, and S Matthew Weinberg.A simple and approximately optimal mechanism for an additive buyer.Journal of the ACM (JACM), 67(4):1–40, 2020b.
• Brown et al. (2024)Bradley Brown, Jordan Juravsky, Ryan Ehrlich, Ronald Clark, Quoc V Le, Christopher Ré, and Azalia Mirhoseini.Large language monkeys: Scaling inference compute with repeated sampling.arXiv preprint arXiv:2407.21787, 2024.
• Bulow and Klemperer (1994)Jeremy I Bulow and Paul D Klemperer.Auctions vs. negotiations, 1994.
• Cai et al. (2016)Yang Cai, Nikhil R Devanur, and S Matthew Weinberg.A duality based unified approach to bayesian mechanism design.InProceedings of the forty-eighth annual ACM symposium on Theory of Computing, pages 926–939, 2016.
• Cai et al. (2024)Yang Cai, Christopher Liaw, Aranyak Mehta, and Mingfei Zhao.The power of two-sided recruitment in two-sided markets.InProceedings of the 56th Annual ACM Symposium on Theory of Computing, pages 201–212, 2024.
• Cai et al. (2026a)Yang Cai, Anupam Gupta, Vineet Gupta, Guru Guruganesh, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Renato Paes Leme, Grigoris Velegkas, and Di Wang.Efficient online inverse optimization withO⁡(d)O(d)regret.arXiv preprint arXiv:2609.13440, 2026a.
• Cai et al. (2026b)Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, and Di Wang.Prediction with expert advice: Anytime regret with many experts matches the fixed-time constant, 2026b.URLhttps://arxiv.org/abs/2609.27206.
• Cai et al. (2026c)Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, and Di Wang.Efficiency of generalized proportional first-price auctions under auto-bidding, 2026c.Forthcoming.
• Cai et al. (2026d)Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, and Di Wang.Improved revenue guarantees for selling separately and bundling, 2026d.URLhttps://arxiv.org/abs/2609.28873.
• Cai et al. (2026e)Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, Di Wang, and Mingfei Zhao.The power of recruiting the smaller side: Two additional traders suffice in two-sided markets.arXiv preprint arXiv:2609.27304, 2026e.
• Cai et al. (2026f)Yang Cai, Vineet Gupta, Zun Li, and Aranyak Mehta.A new lower bound for the random offerer mechanism in bilateral trade using ai-guided evolutionary search.arXiv preprint arXiv:2603.08679, 2026f.
• Castéran and Bertot (2004)Pierre Castéran and Yves Bertot.Interactive theorem proving and program development. coq’art: The calculus of inductive constructions., 2004.
• Cesa-Bianchi et al. (1997)Nicolò Cesa-Bianchi, Yoav Freund, David Haussler, David P Helmbold, Robert E Schapire, and Manfred K Warmuth.How to use expert advice.Journal of the ACM (JACM), 44(3):427–485, 1997.
• Cover (1966)Thomas M Cover.Behavior of sequential predictors of binary sequences.Number 7002. Stanford University, Stanford Electronics Laboratories, Systems Theory, 1966.
• Dewasurendra (2026)Pahan Dewasurendra.Multiscale reward hedging from correct demonstrations.arXiv preprint arXiv:2608.06825, 2026.
• Du et al. (2024)Yilun Du, Shuang Li, Antonio Torralba, Joshua B Tenenbaum, and Igor Mordatch.Improving factuality and reasoning in language models through multiagent debate.InInternational Conference on Machine Learning (ICML), 2024.
• Feng et al. (2026)Tony Feng, Trieu H Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung, Joonkyung Lee, Carlo Pagano, Sang-hyun Kim, Federico Pasqualotto, et al.Towards autonomous mathematics research.arXiv preprint arXiv:2602.10177, 2026.
• Georgiev et al. (2025)Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, and Adam Zsolt Wagner.Mathematical exploration and discovery at scale.arXiv preprint arXiv:2511.02864, 2025.
• Gollapudi et al. (2021)Sreenivas Gollapudi, Guru Guruganesh, Kostas Kollias, Pasin Manurangsi, Renato Paes Leme, and Jon Schneider.Contextual recommendations and low-regret cutting-plane algorithms.Advances in Neural Information Processing Systems, 34:22498–22508, 2021.
• Gottweis et al. (2026)Juraj Gottweis, Wei-Hung Weng, Alexander Daryin, Tao Tu, Petar Sirkovic, Artiom Myaskovsky, Grzegorz Glowaty, Felix Weissenberger, Alessio Orlandi, Dan Popovici, Anil Palepu, Keran Rong, Ryutaro Tanno, Khaled Saab, Fan Zhang, Jacob Blum, Andrew Carroll, Kavita Kulkarni, Nenad Tomašev, Dina Zverinski, Ivor Rendulic, Elahe Vedadi, Florian Hasler, Luka Rimanic, Marina Boia, Ivan Budiselic, Ben Feinstein, Mathias Bellaiche, Tom Sheffer, Jan Freyberg, Jeremy Ratcliff, Ottavia Bertolli, Katherine Chou, Avinatan Hassidim, Burak Gokturk, Amin Vahdat, Yuan Guan, Vikram Dhillon, Eeshit Dhaval Vaishnav, Byron Lee, Tiago R. D. Costa, José R. Penadés, Gary Peltz, Yossi Matias, James Manyika, Demis Hassabis, Yunhan Xu, Pushmeet Kohli, Annalisa Pawlosky, Alan Karthikesalingam, and Vivek Natarajan.Accelerating scientific discovery with co-scientist.Nature, 655(8122):487–496, May 2026.ISSN 1476-4687.10.1038/s41586-026-10644-y.URLhttp://dx.doi.org/10.1038/s41586-026-10644-y.
• Harvey et al. (2023)Nicholas J. A. Harvey, Christopher Liaw, Edwin Perkins, and Sikander Randhawa.Optimal anytime regret with two experts.Mathematical Statistics and Learning, 6(1):87–142, 2023.
• Harvey et al. (2024)Nicholas J. A. Harvey, Christopher Liaw, and Victor S Portella.Continuous prediction with experts’ advice.Journal of Machine Learning Research, 25(228):1–32, 2024.
• Hubert et al. (2026)Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, et al.Olympiad-level formal mathematical reasoning with reinforcement learning.Nature, 651(8106):607–613, 2026.
• Jiang et al. (2022)Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample.Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.arXiv preprint arXiv:2210.12283, 2022.
• Liang et al. (2024)Tian Liang, Zhiwei He, Wenxiang Jiao, Xing Wang, Yan Wang, Rui Wang, Yujiu Yang, Shuming Shi, and Zhaopeng Tu.Encouraging divergent thinking in large language models through multi-agent debate.InProceedings of the 2024 conference on empirical methods in natural language processing, pages 17889–17904, 2024.
• Liaw et al. (2023)Christopher Liaw, Aranyak Mehta, and Andres Perlroth.Efficiency of non-truthful auctions in auto-bidding: The power of randomization.InProceedings of the ACM Web Conference 2023, pages 3561–3571, 2023.
• Lin et al. (2026)Honghao Lin, David P Woodruff, Yuan Deng, Jieming Mao, Song Zuo, and Vahab Mirrokni.Stellar colosseum: A many-agent harness for long-horizon research in mathematics and theoretical computer science.arXiv preprint arXiv:2609.15983, 2026.
• Luo and Schapire (2014)Haipeng Luo and Robert Schapire.Towards minimax online learning with unknown time horizon.InInternational Conference on Machine Learning, pages 226–234. PMLR, 2014.
• Ma and Simchi-Levi (2021)Will Ma and David Simchi-Levi.Reaping the benefits of bundling under high production costs.InInternational Conference on Artificial Intelligence and Statistics, pages 1342–1350. PMLR, 2021.
• Mehta (2022)Aranyak Mehta.Auction design in an auto-bidding setting: Randomization improves efficiency beyond vcg.InProceedings of the ACM Web Conference 2022, WWW ’22, page 173–181, New York, NY, USA, 2022. Association for Computing Machinery.ISBN 9781450390965.10.1145/3485447.3512062.URLhttps://doi.org/10.1145/3485447.3512062.
• Moura and Ullrich (2021)Leonardo de Moura and Sebastian Ullrich.The lean 4 theorem prover and programming language.InInternational Conference on Automated Deduction, pages 625–635. Springer, 2021.
• Nagda et al. (2026)Ansh Nagda, Prabhakar Raghavan, and Abhradeep Thakurta.Reinforced generation of combinatorial structures: Hardness of approximation, 2026.URLhttps://arxiv.org/abs/2509.18057.
• Nipkow et al. (2002)Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson.Isabelle/HOL: a proof assistant for higher-order logic.Springer, 2002.
• Novikov et al. (2025)Alexander Novikov, Ngân Vũ, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco JR Ruiz, Abbas Mehrabian, et al.Alphaevolve: A coding agent for scientific and algorithmic discovery.arXiv preprint arXiv:2506.13131, 2025.
• Oki and Sakaue (2026)Taihei Oki and Shinsaku Sakaue.Finite and corruption-robust regret bounds in online inverse linear optimization under m-convex action sets.arXiv preprint arXiv:2602.01682, 2026.
• OpenAI (2026a)OpenAI.An OpenAI model has disproved a central conjecture in discrete geometry.https://openai.com/index/model-disproves-discrete-geometry-conjecture/, May 2026a.
• OpenAI (2026b)OpenAI.On the Navier–Stokes Millennium Prize problem.https://openai.com/index/navier-stokes-solution/, September 2026b.
• Romera-Paredes et al. (2024)Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M Pawan Kumar, Emilien Dupont, Francisco JR Ruiz, Jordan S Ellenberg, Pengming Wang, Omar Fawzi, et al.Mathematical discoveries from program search with large language models.Nature, 625(7995):468–475, 2024.
• Rubinstein (2016)Aviad Rubinstein.On the computational complexity of optimal simple mechanisms.InProceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science (ITCS), pages 21–28, 2016.
• Sakaue (2026a)Shinsaku Sakaue.Simple projection-free algorithm for contextual recommendation with logarithmic regret and robustness.arXiv preprint arXiv:2603.20826, 2026a.
• Sakaue (2026b)Shinsaku Sakaue.Tight regret bound for online inverse linear optimization via multiscale matrix weights.arXiv preprint arXiv:2609.26978, 2026b.
• Sakaue et al. (2025a)Shinsaku Sakaue, Han Bao, and Taira Tsuchiya.Revisiting online learning approach to inverse linear optimization: A Fenchel-Young loss perspective and gap-dependent regret analysis.arXiv preprint arXiv:2501.13648, 2025a.
• Sakaue et al. (2025b)Shinsaku Sakaue, Taira Tsuchiya, Han Bao, and Taihei Oki.Online inverse linear optimization: Efficient logarithmic-regret algorithm, robustness to suboptimality, and lower bound.Advances in Neural Information Processing Systems, 38:85189–85217, 2025b.
• Schmitt et al. (2026)Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck, Gergely Bérczi, Uri Kreitner, Liam Price, and David Holmes.Proofcouncil: An llm agent for solving open mathematical problems, 2026.URLhttps://arxiv.org/abs/2607.09474.
• Snell et al. (2024)Charlie Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar.Scaling llm test-time compute optimally can be more effective than scaling model parameters.arXiv preprint arXiv:2408.03314, 2024.
• The Antigravity Team (2025)The Antigravity Team.Introducing Google Antigravity, a new era in AI-assisted software development.https://antigravity.google/blog/introducing-google-antigravity, November 2025.Google Antigravity Blog.
• Trinh et al. (2024)Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong.Solving olympiad geometry without human demonstrations.Nature, 625(7995):476–482, 2024.
• Tsoukalas et al. (2026)George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferraiuolo, Henryk Michalewski, Edward Lockhart, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, and Swarat Chaudhuri.Advancing mathematics research with ai-driven formal proof search, 2026.URLhttps://arxiv.org/abs/2605.22763.
• Wang et al. (2022)Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou.Self-consistency improves chain of thought reasoning in language models.arXiv preprint arXiv:2203.11171, 2022.
• Wang et al. (2025)Yiping Wang, Shao-Rong Su, Zhiyuan Zeng, Eva Xu, Liliang Ren, Xinyu Yang, Zeyi Huang, Xuehai He, Luyao Ma, Baolin Peng, et al.Thetaevolve: Test-time learning on open problems.arXiv preprint arXiv:2511.23473, 2025.
• Wei et al. (2022)Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed Chi, Quoc V Le, and Denny Zhou.Chain-of-thought prompting elicits reasoning in large language models.Advances in neural information processing systems, 35:24824–24837, 2022.
• Yang et al. (2023)Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar.Leandojo: Theorem proving with retrieval-augmented language models.Advances in Neural Information Processing Systems, 36:21573–21612, 2023.
• Yuksekgonul et al. (2026)Mert Yuksekgonul, Daniel Koceja, Xinhao Li, Federico Bianchi, Jed McCaleb, Xiaolong Wang, Jan Kautz, Yejin Choi, James Zou, Carlos Guestrin, et al.Learning to discover at test time.arXiv preprint arXiv:2601.16175, 2026.
• Zheng et al. (2026)Daniel Zheng, Ingrid von Glehn, Yori Zwols, Iuliya Beloshapka, Lars Buesing, Daniel M. Roy, Martin Wattenberg, Bogdan Georgiev, Tatiana Schmidt, Andrew Cowie, Fernanda Viegas, Dimitri Kanevsky, Vineet Kahlon, Hartmut Maennel, Sophia Alj, George Holland, Alex Davies, and Pushmeet Kohli.Ai co-mathematician: Accelerating mathematicians with agentic ai, 2026.URLhttps://arxiv.org/abs/2605.06651.
• Zhuge et al. (2024)Mingchen Zhuge, Changsheng Zhao, Dylan Ashley, Wenyi Wang, Dmitrii Khizbullin, Yunyang Xiong, Zechun Liu, Ernie Chang, Raghuraman Krishnamoorthi, Yuandong Tian, et al.Agent-as-a-judge: Evaluate agents with agents.arXiv preprint arXiv:2410.10934, 2024.

Appendix APrompts Used for the Problems

A.1Efficient Online Inverse Linear Optimization

Traditionally,cutting-planealgorithmshavebeendevelopedtominimizethenumberofcallstotheseparationoracleuntiltheoraclereturnsahyperplanethatpasseswithinsomedistance\\deltaofw^\*.

Inoursetting,insteadoftryingtominimizethenumberofseparationoraclequeriesbeforefindinga“close“hyperplane,wewouldliketominimizethetotal(overallTrounds)distancebetweenthereturnedhyperplanesandthehiddenpointw^\*.Thatis,wewouldliketominimizetheexpression:Reg’=\\sum\_\{t=1\}^T\(\\langlew^\*,v\_t\\rangle\-\\langlep\_t,v\_t\\rangle\)=\\sum\_\{t=1\}^T\\langlew^\*\-p\_t,v\_t\\rangle.

Canwedesignacuttingplanealgorithmwhoseregretispolynomialind,andindependentofT?

NotethatthisproblemisfromthepaperNeurIPS2021paper“ContextualRecommendationsandLow-RegretCutting-Plane“.

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

Supposetherearembuyersandnsellersandm\\geqn.

WeassumethatthebuyerdistributionF\_Bfirst-orderstochasticallydominatesthesellerdistributionF\_S.

LetSTR(m,n)betheexpectedGFTofSellerTradeReductionasdiscussedinthepaper.

LetOPT(m,n)betheexpectedfirst-bestGFT.

Showthatadding2additionalsellersissufficienttoguaranteethatSellerTradeReductionachievesatleastthefirst-bestGFToftheoriginalmarket.Thatis,showthatSTR(m,n+2)>=OPT(m,n)forallm,n>=1.

A.3Anytime Algorithm for Prediction with Expert Advice

Inthatpaper,theyestablishtheoptimalanytimeregretfortwoexperts.

Iwanttounderstandwhatistheanytimeregretfornexpertsasn\\to\\infty.Canweshowthatthepriceofanytimegoesto1asn\\to\\infty?Pleasetakealookattheconjecturedescribedinhttps://arxiv.org/pdf/2002.08994.

Pleasealsohavethelitreviewersdoadeepsearchsoyouunderstandthelandscape.Feelfreetolaunchasmanylitreviewersasyoufeelyouneed.

A.4Selling Separately vs. Bundling

**ProblemStatement:**

Provethatforasingleadditivebuyerwithmultipleitems,therevenuefromthebetterofsellingtheitemsseparatelyorsellingthemasagrandbundleisafactor-3approximationtotheoptimalexpectedrevenue.Theitemshaveindependentvaluesdrawnfromknowndistributions.

Formally,showthat:\\text\{OPT\}\\le3\\max\\\{\\text\{SREV\},\\text\{BREV\}\\\}

**Definitions:**

-\\text\{OPT\}:Theexpectedrevenueoftheoptimal(fullygeneral,randomized)BayesianIncentiveCompatiblemechanism.

-\\text\{SREV\}:Themaximumexpectedrevenueachievablebysellingeachitemseparatelyatitem-specificprices.

-\\text\{BREV\}:Themaximumexpectedrevenueachievablebysellingallitemstogetherasasinglegrandbundle.

-AdditiveBuyer:Thebuyer’svalueforasetofitemsisthesumoftheirvaluesfortheindividualitems.

**ReferenceMaterial:**

Thefollowingtwopapersareusefulreferences:

1.*ADualityBasedUnifiedApproachtoBayesianMechanismDesign*(Cai,Devanur,Weinberg):https://www.cs.yale.edu/homes/cai/publication/duality-journal/duality-journal.pdf

2.*ASimpleandApproximatelyOptimalMechanismforanAdditiveBuyer*(Babaioff,Immorlica,Lucier,Weinberg):https://arxiv.org/pdf/1405.6146

**ProofOutlineandInstructions:**

Pleasethinkstep-by-stepandstructureyourproofcarefullyusingLaTeXforallmathematics.Ifyoucannotprovethefactor3approximation,youshouldfirsttrytoprovethatthisisafactor4approximation,thentrytostrengthenit.

A.5Autobidding

We provided two prompts to the system corresponding to then=2n=2case and then≥2n\geq 2case. Note that the prompts asked the system to make some mild assumption. We removed the assumption by asking Gemini to look at the output proof and modify it accordingly.

Iwanttoconsiderthefollowingmechanism.Fortwobidders,iftheirbidsareb\_1andb\_2,

thenbidderiwinswithprobabilityb\_i/\(b\_1\+b\_2\)and,conditionalonwinning,paysb\_i.

ProveordisprovethatthismechanismhasaPoAof1.5.

Youcanandshouldassumethatallbiddershavestrictlypositivevalueonallqueries.

Thatpapergivesamechanismthatworkswellfortwobidders.However,thesettingformorethantwobiddersremainsopen.

Yourgoalistofirstunderstandthelowerboundinhttps://arxiv.org/abs/2207.03630.WhatkindofPoAlowerbounddoesitgiveasafunctionofnwherenisthenumberofbidders.

Onceyouunderstandthat,let’strytofindanupperbound.Ineitherwords,comeupwithamechanismthat,foralln,givesaPoAasclosetothelowerboundasyoucan.

Forexample,ifthelowerboundPoAisoftheform2\-\\Omega\(1/n\)thenanideaupperboundshouldbeoftheform2\-O\(1/n\).

Notethatyourmechanismisallowedtodependonnbutshouldnotdependonvalues,costs,etc.otherthanthebids.

Youcanandshouldassumethatallbiddershavestrictlypositivevalueonallqueries.

Youcanandshoulddosomeliteraturereviewonwhatisknownaboutthisproblem.