Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Finding a nonzero nonnegative point in a linear subspace is the feasibility core of linear optimization. For a subspace with orthogonal complement , the pair of problems
subsumes every polyhedral feasibility problem and every linear program through standard homogenization. A maximum support solution of the pair, a point of each cone with as many positive coordinates as possible, always exists, and identifies which coordinates can be positive at all. Rescaling algorithms solve such problems with elementary steps (a simple "basic procedure" interleaved with a reconditioning step) and with running-time bounds in terms of a condition measure of the input.
Timeline of the results this mission builds on, as described in the source (arXiv:2003.08911v3, pp. 1–3):
Let be a linear subspace and its orthogonal complement. The support of is . The maximum support index set is
and a maximum support point is an whose support is . For each coordinate , , and the condition measure is , with when .
For let be the vectors vanishing off , , and, for a positive diagonal matrix , the orthogonal projection onto .
Algorithm 1 (partial support) takes with a guess of . It starts from , and repeatedly calls a basic procedure, which returns either with , in which case the algorithm halts with and ; or with , in which case it doubles for a maximizer of (a rescaling step), drops from if , and halts with , if becomes empty. Its output is written .
Algorithm 2 (maximum support) starts with and in each main iteration computes and ; it halts if and otherwise replaces by .
With and , for every , every subspace and every admissible behaviour of the basic procedure: Algorithm 2 never gets stuck, has no infinite execution, never starts main iteration , performs at most
rescaling steps, and upon termination returns , and points , with , .
The result. Theorem 1 gives an algorithm for the maximum support problem whose cost depends only on , without knowing either quantity: guessing rounds and rescaling steps, each of which is a call of the basic procedure on a projected problem. Because the pair of problems subsumes polyhedral feasibility and linear programming, a maximum support solution is a certificate of which inequalities of a homogenized system can hold strictly. The duality behind the stopping test, that and partition the coordinates, is a theorem of the alternative for subspaces of the Goldman–Tucker type.
Formalizing it. The result is proved in the source; nothing here is open. No part of it is machine-checked: there is no formal development of projection-and-rescaling algorithms, of condition measures for subspaces, or of the subspace form of the strict-complementarity partition. Checking the source against the formal statements already found that the printed bounds (5), (6) and (7) are false for some subspaces (counterexamples are recorded in the corresponding items); the targets above carry the minimal corrections, so a complete proof certifies the corrected bounds.
The correctness part reduces to the partition claim and to Corollary 1. The partition requires a theorem of the alternative for the pair and the nonnegative orthant, which is not literally the LP form of Farkas' lemma available in libraries.
The counting part is where the printed argument breaks. The proof of Proposition 1 asserts "throughout the algorithm", by applying Lemma 1 to each rescaling step. But the basic procedure certifies only the subspace , not . As long as the two cones and coincide and the identity holds. Once an index of has been trimmed, which can happen when , it does not. The count of rescalings must also use doublings per trimmed index rather than , which matters precisely because Algorithm 2 uses guesses for which is a power of . The obvious induction on steps therefore has to carry the invariant and works only under . For larger guesses, which Algorithm 2 makes in its early iterations, only the coarse count is available.
is EuclideanSpace ℝ (Fin n) and a Submodule; is Mathlib's orthogonal complement. The Euclidean norm is never used for the paper's norms: and are written coordinatewise, and maximizes over the unit box, not the Euclidean ball. Index sets are Finset (Fin n). is stored as its diagonal. is the orthogonal projection of onto , which agrees with the paper's map on . when , as in the source. Proposition 1 and Theorem 1 assume , since Algorithm 1 cannot run on .
Both algorithms are transition relations whose states carry the rescaling and iteration counters, and the basic procedure is nondeterministic: every admissible answer and every maximizer is a possible step, and both branches may be available at once. Every statement quantifies over all executions. Progress (no reachable non-halted state is stuck) and the absence of infinite executions are stated explicitly. This rules out the trivializing formalizations: a relation with no transitions (which would make "upon termination" vacuous), a fixed deterministic basic procedure, over the Euclidean ball, bounds for a single execution, and termination as "some execution halts". A sorry-free check exhibits, for and , a reachable halted state of Algorithm 2 after two rescaling steps, which also witnesses that the printed (7) fails.
A complete development needs the theorem of the alternative for subspaces, orthogonal projections onto intersections of subspaces, a variant/measure argument for termination of nondeterministic relations, and logarithm and floor arithmetic for the schedule . The partition claim and the condition-measure lemmas are reusable for other rescaling and condition-number analyses. Proofs of the milestones, alternative arguments for the partition, and the sharper count of Proposition 1 are all welcome.
The stability number of a graph, the largest number of pairwise non-adjacent vertices, is one of the basic parameters of combinatorial optimization: computing it is NP-hard, and random graphs are the standard test bed for what typical instances look like. For the Erdős–Rényi–Gilbert graph , in which every edge is present independently, the behaviour of is known to first order in the dense regime (Grimmett–McDiarmid 1975) and in the sparse regime (Frieze 1990). Independence of the edges is what all these arguments use, and it is also the feature that real networks most obviously lack.
A. Gupte and Y. Zhu (arXiv:2207.04514, Mathematics of Operations Research, 2025) introduce a random graph in which the edges at a vertex are dependent through a Markov chain, and ask which classical properties survive. Their first main result is a lower bound on of order that holds with high probability. This mission formalizes that result, read in the arXiv version v4 (24 May 2024).
Fix an initial probability and a decay parameter , and write . The recursive Markov random graph (Definition 1 of the paper) has vertices and is generated vertex by vertex. When arrives, its edges to the earlier vertices form a row of Bernoulli variables , with when the edge is present. Rows of different vertices are independent. Within a row:
So each row is a non-homogeneous Markov chain whose transition matrix (display (2) of the paper) depends on the marginal of the previous edge. The marginals then obey the recursion with , and a present edge lowers the chance of the next one by the factor . At the model is ; the paper assumes throughout.
The average degree is . A property holds with high probability (w.h.p.) if its probability tends to as , and concentrates to if for every . The logarithm is natural.
For every , and ,
The constant is the paper's, and the statement is required for every and every admissible , .
In attack order:
The theorem shows that the dependence between consecutive edges does not destroy the scale of the stability number. Combined with the paper's upper bound (Theorem 2.4) and its analysis of the greedy algorithm (Proposition 2.3), it places between the dense and the sparse regimes of . Theorem 2.2, a milestone here, is of independent interest: the graph has average degree , and Corollaries 2.5–2.7 of the paper derive from it bounds on the minimum degree and the chromatic number and the existence of large clique minors.
The formalization adds a checked account of a proof whose printed version has gaps. Several printed lemmas are false as stated: Lemmas 4.2 and 4.3 lose a scaling factor, Lemma 6.2 has a wrong upper bound, Lemmas 10.1 and 10.4 are stated in a setting where they fail and Lemma 10.1 has a wrong constant, Theorem 4.4 is false without a Markov hypothesis, and the stochastic-dominance step (5) in the printed proof of Theorem 2.2 is false. Each affected milestone is stated in a minimally corrected form. Theorem 2.1 and Theorem 2.2 themselves are true. None of these results has a machine-checked proof.
A first idea is to transfer arguments directly. For with the bound comes from Turán's theorem plus concentration of the edge count, and the edge count is a sum of independent indicators. In the edges at a vertex are strongly dependent: the edge count of a row is the partial sum of a non-homogeneous Markov chain whose marginals decay like , so its mean grows only like . Standard laws of large numbers do not apply, and concentration of a row sum around needs a second-moment bound that uses the Markov structure; the marginal recursion alone does not suffice (a comonotone coupling with the same marginals has row sums that stay bounded). The heart of the mission is therefore Corollary 4.6, a law of large numbers for this chain, built from the recursion estimates of Lemmas 4.2–4.3 and the second-moment bound of Lemma 10.1, and its transfer to the average degree through the independence of the rows.
The vertex set is Fin n, the paper's being k − 1, and the edge is G.Adj (j−1) (i−1). The law of is an explicit finite weight rmrgWeight n p r G on SimpleGraph (Fin n). It is a product over rows, each row's weight being the Markov chain above with the transition out of edge using the -th iterate of from . Probabilities are rmrgProb n p r E, the sum of the weights of the graphs in . Definition 1's phrase "independent of all other edges" cannot hold for the next edge of the same row; it is read through the paper's generation process (rows independent, each row a Markov chain with transition matrix (2)). Lemma 3.1 is the milestone certifying that the marginals of this weight obey the recursion. A sanity file checks that the weights sum to for and that the first two edge marginals are and .
The decay chain is IsDecayChain P Y β on a probability space: -valued measurable variables, the Markov property, and the two transition rules, with conditional probabilities written multiplicatively. Expectations are Bochner integrals, and "w.h.p." and concentration are limits of probabilities of the events , as defined on p. 4 of the paper. Variances in Lemma 10.2 come with square integrability for all large , so the hypothesis is not met by the junk value .
A trivializing formalization is ruled out: the weight is exactly the law of Definition 1, not one favouring sparse graphs, and no hypothesis of the goal pins the graph or the probability.
The corrections, each with a counterexample satisfying the paper's hypotheses, are declared on the items:
Theorem 4.4 is false as stated and is not an item; Corollary 4.6, which the proof of Theorem 2.2 cites, replaces it. Displays (5)–(10), Proposition 2.3, Theorem 2.4 and Corollaries 2.5–2.7, 4.5, 4.7 and 5.2 are out of scope.
A complete development needs:
rmrgProb: marginals, independence of rows, the row-to-chain identification;SimpleGraph.indepNum, which Mathlib does not yet have.The last two are reusable beyond this mission. Contributions to any milestone are welcome, as are alternative proofs of Theorem 2.2 that avoid the printed stochastic-dominance step.
Centralized platforms that assign work to independent service providers, such as ride-hailing and freelance marketplaces, sales organisations distributing leads, and firms sourcing from several suppliers, are often asked to give their providers guarantees: a minimum income, a max-min fair share of the work, or another fairness criterion. A guarantee shrinks the set of allocations the system may use, so it can lower the total value the system generates. The question is how much value can be lost.
Many settings of this kind have no bound at all on the price of fairness or the price of anarchy (Bertsimas, Farias and Trichakis 2011; Koutsoupias and Papadimitriou 2009). Gur, Iancu and Warnes (SSRN 3351509, published in Management Science in 2020) identify a broad class of job-allocation systems and guarantees for which the relative loss is bounded by a quantity that depends only on the number of providers and on how different they are. This mission formalizes that bound, Theorem 1 of the paper, and the steps of its proof.
A job in a finite set has an intrinsic value . Values may be negative. A set of jobs has value . There are providers . An allocation is a tuple of subsets of , where is the set of jobs given to provider . Provider turns its jobs into value . The heterogeneity profile lies in with , and the degree of heterogeneity is
The feasible allocations form a set that satisfies Assumption 1:
The allocations with guarantees form a non-empty subset that satisfies Assumption 2 (Pareto efficiency): if , and for every , then . Income guarantees under monotone payments, max-min fairness and α-fairness are of this kind (§2.3 of the paper). The value loss under provider guarantees is
For every and all , satisfying Assumptions 1 and 2,
The statement fixes nothing beyond the paper's model: every finite job set, every real-valued , every number of providers and every profile in the box.
These are the steps of the proof in Appendix A, in attack order:
The result. With homogeneous providers () any Pareto-efficient guarantee costs less than half of the optimal value, since . For every fixed the loss stays below . A system designer may therefore choose among income guarantees, max-min fairness and similar rules knowing that none of them can destroy more than a fixed fraction of value. Theorem 2 of the paper shows that the bound is tight. Theorem 1 is the paper's main result.
Formalizing it. The result is proved in the paper; nothing in this mission is open mathematically. The work is the formal proof. On the way it produces reusable pieces:
Two printed gaps get settled:
The obvious attempt is to compare an optimal unrestricted allocation with an optimal guaranteed one job by job. This gives no bound, because and are arbitrary sets subject only to the axioms: there is no explicit allocation rule to compare against. The paper's route has several steps that each need care.
Everything lives in the namespace ProviderGuarantee.Bound. The definitions are in the single file ProviderGuarantee.Bound.Model:
Fintype, and carries no sign condition. An allocation is a function Fin n → Finset D, so provider of the paper is the index .fun i => A (σ i)), and monotonicity and provider independence use Function.update. Assumption 2 includes .sSup. Every set of allocations is finite, so this is a true maximum on non-empty sets, and is a hypothesis of the goal.sSup and the dual value is a real sInf over (15). (15) is (16) with explicit. The milestones state feasibility, boundedness and attainment, so neither value is a default.The goal is about the value loss of the allocation model over all admissible , and . A formalization stating Theorem 1 about the LP value, at a single vertex, at , with , or with a weakened Assumption 1 or 2 would prove a different and easier statement, and is ruled out.
A complete development needs:
Finset.biUnion);LinearOptimization.lp_strong_duality) is a possible tool;Contributions are welcome for any milestone, and for the invariance of (14) under permutation and positive scaling of , which the goal's proof needs and the paper uses tacitly.
Training and back-testing a reinforcement-learning policy for a supply chain requires policy simulation: given an initial state, a horizon and a sequence of exogenous events, compute the actions the policy takes when the system evolves under its own decisions. In large online retail networks the horizon is the number of customer orders, in the millions, and each step needs one evaluation of a neural-network policy. Sequential simulation therefore costs policy evaluations in series, and this dominates the cost of training and evaluating such policies (Farias et al., 2025).
Parallel discrete-event simulation methods such as Time Warp (Jefferson, 1985) parallelise a single trajectory by optimistic execution and rollback, but they rely on local causality that fulfillment problems lack: every order can interact with every other through shared node capacities. Farias, Gijsbrechts, Khojandi, Peng and Zheng propose the Picard iteration: split the time steps among many processes, let each process evaluate the policy only on its own steps while replaying cached actions elsewhere, and iterate until the cache stops changing. For the fulfillment optimization (FO) problem, the central example of the paper and a standard model of online order fulfillment (Acimovic & Farias, 2019), the paper proves that the number of iterations is bounded independently of . This mission formalizes that bound.
A controlled dynamical system has states , actions , disturbances , a set of feasible actions at each state, an always-feasible action , and a transition map . A policy is a map . Given and disturbances , the sequential run is , .
In the FO problem there are products and nodes. A state records inventories and remaining capacities . Each disturbance is an order for a product . An action is a node , feasible when and , or the action (do not fulfil). Fulfilling from node removes one unit of capacity at and one unit of the ordered product's inventory at ; action changes nothing.
The Picard iteration (Algorithm 1 of the paper) assigns each time step to a process. In the FO problem the assignment is by products: each product is owned by one process, and every order of that product is handled by its owner. The cache starts as . In iteration every process re-simulates from . On its own orders it evaluates the policy. On every other order it replays the cached action if that action is feasible in its own state, and takes otherwise. The new cache takes each order's action from the process that owns it. The algorithm stops when .
The theorem assumes three properties of the policy:
Bid-price policies (Talluri & van Ryzin, 1998) satisfy all three. Write for the set of nodes with positive initial capacity whose capacity is no longer positive at some time in the sequential run.
For every feasible policy satisfying Assumptions 1–3, every real initial state, every order sequence, every horizon and every product-to-process assignment,
and whenever the stopping test succeeds at an iteration , the returned cache is on . Since , this gives the paper's informal Theorem 3.1 (at most iterations).
The bound makes the parallel speed-up concrete. One iteration costs about sequential policy evaluations with processes, so convergence in iterations gives an effective speed-up of order . This is independent of and depends on the instance only through the number of nodes that run out of capacity. When supply exceeds demand this number can be much smaller than , which the paper uses to explain the speed-ups of several hundred times it measures on a GPU.
Formalizing the result adds three things. First, it fixes the statement. As printed, with defined as the first time , the theorem is false for the real capacities the paper allows: a capacity of goes to and then to without ever being . Two steps of the appendix also fail as printed: eq. (3) at , and the equality in the skip step, which ignores the feasibility fallback of Algorithm 1. The mission states the corrected forms, each checked by randomized brute-force search on small instances. Second, it produces a checked version of an argument that the paper presents compactly, with a mixed indexing of states. Third, the definitions give a reusable model of the Picard iteration for general dynamical systems. As far as is known, no part of this result has been machine-checked.
A wrong cached action from another process changes a process's state, and through it all of the process's later decisions. In the special case treated in §3.1, a greedy policy with unlimited inventory, every wrong action goes to a node that runs out in the sequential run (Lemma 3.2). Each iteration then fixes the cache up to the next exhaustion time. That invariant does not hold for policies that depend on inventory: a wrong action can go to a node that never runs out, and the paper notes that Lemma 3.2 "no longer holds". The general argument has to control inventories, not actions, across all processes and iterations at once. It must also cope with the fallback to when a replayed action is infeasible, which makes non-owner processes lag behind the owner's run rather than copy it.
Over real data, Assumption 3 gives invariance only under whole-unit increments of capacity. The policy need not depend on capacities only through their signs.
The Lean development uses the following conventions.
Fin I and nodes Fin J; inventories are Fin I → Fin J → ℝ and capacities Fin J → ℝ, of any sign. Actions are Option (Fin J), with none the paper's action .ω : ℕ → Ω with product map prod : Ω → Fin I. Processes form an arbitrary type with an ownership map own : Fin I → ι. Orders are 0-based: Lean order t is the paper's order , and seqState … t is the state before it.Ruled-out formalizations. The theorem would become trivial if processes evaluated the policy on every order (that is sequential simulation), and it would describe a different algorithm if the infeasibility fallback were dropped or the cache were taken from a fixed process; replacing by would give the weaker Theorem 3.1. The definitions follow Algorithm 1 line by line.
Definitions. There are two definition files: a general Picard iteration for any controlled dynamical system and assignment of time steps to processes (reusable beyond this mission), and the FO instance with Assumptions 1–3 and . A local check confirms that the hypotheses are satisfiable by a policy that actually fulfils orders.
Contributions welcome. Proofs of the milestones in the order listed, and alternative proofs of the goal.
The secretary problem asks how to hire the best of candidates who are interviewed one at a time in random order, when every hiring decision must be made irrevocably at the interview. It is the standard model of online selection under uncertainty, and its answer, Dynkin's rule, hires the maximum with probability (Dynkin 1963; see the survey of Ferguson 1989). No algorithm does better without further information.
In many applications that further information exists: a recommender system, a past auction, or a résumé screen gives a prediction of every candidate's value before the interviews start. The learning-augmented (algorithms-with-predictions) framework asks for algorithms that exploit predictions when they are accurate (consistency) while keeping a worst-case guarantee when they are not (robustness) (Lykouris and Vassilvitskii 2021; Mitzenmacher and Vassilvitskii 2022). Fujii and Yoshida (arXiv:2306.08340, Mathematics of Operations Research 2024) give such an algorithm for the secretary problem with a guarantee that degrades smoothly with the prediction error. This mission formalizes their main result for the classical (single-choice) problem.
There are candidates. Candidate has a value , revealed at its interview, and a prediction , known in advance. In the continuous-time model each candidate independently receives an arrival time uniform on , and candidates are interviewed in increasing order of .
For a threshold , candidate deviates if its multiplicative error exceeds :
The deviating candidates form the set , and . The prediction error is , so that for all .
Algorithm 1 (learned Dynkin) takes a time , the threshold , and a maximizer of . It starts in Prediction mode. When candidate arrives, it first switches to Secretary mode for good if deviates; then, in Prediction mode it hires if , and in Secretary mode it hires if and is the best so far (better than every earlier arrival). Hiring ends the process. Writing for the expected value of the hired candidate ( if nobody is hired), the algorithm is -competitive if for every instance.
With and , for every , all values and predictions, and every maximizer of ,
Both clauses are part of the goal: the constant for every instance, and for every bounding the prediction error.
The proof splits on whether is empty, whether is the best candidate , and whether and lie in . The milestones are its labelled steps, stated for general and :
The result. Theorem 1 shows that a single, simple algorithm is both consistent and robust: as the predictions become exact its ratio tends to , far above the barrier, and whatever the predictions, it never falls below . The same paper shows that the trade-off cannot be avoided entirely: no algorithm achieves together with a robust constant above (deterministic) or (randomized) (Theorems 2 and 3). The analysis also gives a template for the continuous-time analysis of mode-switching stopping rules.
Formalizing it. The theorem is proved in the paper, with a case analysis whose last step is numerical. No part is machine-checked. A complete formalization would contribute a continuous-time secretary model with iid uniform arrival times, the continuous-time Dynkin bound , and a checked version of the numerical step, whose margins are about . The argument has gaps that a formalization must close. The proof's claim of -competitiveness whenever is false for . Theorem 1 is not affected, since it asks only for , but for that maximum is slightly above and the six case bounds alone do not deliver it. The statement here is the theorem as printed.
The natural argument, "follow the prediction until a deviating candidate appears, then run Dynkin's rule", does not inherit Dynkin's guarantee. The Prediction phase may pass over the best early candidate, the switch time is random and correlated with which candidates have arrived, and may be hired even when it is not optimal. Each of the six cases therefore needs its own sufficient event, together with the distribution of the first arrival of and the fact that the arrival time of the best of the candidates before a given time is uniform. The final step requires a bound uniform in : monotonicity in plus finitely many evaluations, with very small margins.
Candidates are Fin n (0-based). The arrival law is Lebesgue measure on Fin n → ℝ restricted to the unit cube . Expectations are Bochner integrals against it, and probabilities are its Measure.real. The deviation test is the division-free , which agrees with the paper when . The prediction-error clause quantifies over every with for all . When all values are positive this is the paper's clause, and it also covers zero values, where the paper's is undefined. The benchmark is written as for every . is universally quantified over all maximizers of .
"Best so far" compares candidates in the strict order larger value, then smaller index, and is the top candidate of that order. The paper does not address ties, and both untied readings make Theorem 1 false: with all values equal, a strict comparison of values hires almost nobody. The mode at an arrival is Secretary when a deviating candidate has arrived at the same time or earlier, the candidate itself included. The value of a run sums the values of all candidates that are first to stop, which differs from a single hire only on the null set of tied arrival times.
The goal bounds the expected value of the hired candidate under the algorithm of p. 6, with both clauses. A formalization in which the value of a run is whenever someone is hired, in which is always hired, or in which the goal is reduced to the case does not state this theorem.
Infrastructure that a complete development needs, and that is reusable beyond this mission: order statistics of iid uniform times on (the law of the first arrival of a set, uniformity of the arrival time of the best candidate among those before a given time), the continuous-time Dynkin bound, and certified evaluation of alternating binomial sums. Proofs of individual cases and of the numerical milestone are welcome independently.
A single machine receives jobs over time. Each job arrives at its release time with a length and a cost function , and all three become known only at arrival. The machine may interrupt a job and resume it later (preemption). The objective is the total delay cost , where is the completion time of job . Weighted flow time (), weighted completion time and tardiness are special cases. With arbitrary nondecreasing the problem is the generalized integral completion time problem, GICS.
Even offline, with general nondecreasing costs and arbitrary release times, this problem is strongly NP-hard. The best known approximation is (Bansal and Pruhs, 2014). Online, no algorithm has a bounded competitive ratio on a unit-speed machine even for weighted flow time (Bansal and Chan, 2009). The standard remedy is speed augmentation: the online machine is times faster than the offline optimum it is compared with.
Prior speed-augmented results covered special cost structures. Im, Moseley and Pruhs (SICOMP 2014) treated with one function shared by all jobs. Angelopoulos, Lucarelli and Thang (Algorithmica 2019) treated convex or concave , identical job densities, and FIFO or HDF policies. Etesami (Operations Research, 2022; arXiv:1906.02644) gave the first speed-augmented competitive algorithm for job-dependent nondecreasing on a single machine, subject to a structural condition on the class of cost functions. This mission formalizes that result.
Jobs are with and . On each is nonnegative, nondecreasing and differentiable, with (§II, p. 5). A fractional schedule with machine capacity assigns a processing rate to every job and time. Rates vanish before , satisfy , and process every job fully: . After the integration by parts on p. 6 and the rescaling , the fractional cost is the linear objective
The benchmark is the infimum of this cost over all fractional schedules: the value of LP (1) for , and of the slower LP (21) for . Its dual (2) has one variable per job and a density on the time axis, with constraints for .
For a time , GFCS(s) is the offline problem in which a set of jobs, with lengths , all start at . Its optimal value is (Definition 3). An optimal integral schedule processes one job at a time.
Algorithm 2 re-solves at every arrival. When job arrives, it takes the jobs still alive, with their residual lengths, together with job . It solves GFCS() for them as if no further job would come, and follows an optimal integral schedule of that instance until the next arrival.
A class of cost functions is monotone substitute (Definition 5) if adding a job to an identical-release instance can only postpone the optimal processing of the existing jobs. The curvature of the class enters through
for every run of Algorithm 2 on an instance whose cost functions lie in a monotone substitute class. This is the statement that Algorithm 2 is -speed -competitive. The goal takes any with , not a closed formula for .
The result covers job-dependent nondecreasing cost functions. Previous speed-augmented guarantees needed a single shared function or a fixed convexity type. It applies to any monotone substitute class: dominating families, classes for which HDF or HRDF is offline-optimal, and classes with an insertion-type optimal offline policy (p. 20). Combined with the black-box reduction of Lemma 1, it gives a speed-augmented guarantee for the integral objective . For concave costs, and the bound becomes -speed -competitive (Example 3).
The result is proved in the paper, and no machine-checked proof of it or of any of its lemmas is known. The paper argues in a time-discretized network-flow model whose quantization error it describes only as "negligible" (Remark 2). A formal proof must therefore carry out the continuous version: strong duality for a semi-infinite assignment LP, the monotonicity of the optimal dual, and the bound (20) without the value function's differentiability.
Every LP in the argument has one variable per job and per time instant, so finite-dimensional LP duality does not apply directly. Dual attainment, and the existence of a dual with maximal , must be proved for this time-indexed LP. The paper's Lemma 4 argument splits the time axis into the set where the new dual exceeds the old one and its complement; in continuous time these are measurable sets defined only almost everywhere. The bound (20) is a one-sided derivative of the value function, and the paper uses it without proving differentiability. The final step is a layer-cake comparison: postponed processing intervals and a nonincreasing integrand give a smaller integral. It needs the right notion of postponement. Monotone substitution is used only there; the rest of the chain holds for every nondecreasing cost.
A first idea is to treat Algorithm 2 as a fixed policy such as HDF and analyze it with potential functions. That fails here, because the algorithm is defined only through optimal offline solutions, and their structure depends on the class of cost functions.
All declarations live in the namespace GenCostSched.GFCS and import one definitions file, GenCostSched.GFCS.Model.
Representation. Jobs are Fin n and times are real. The cost functions are the scaled of p. 6, supplied as data together with their first and second derivatives, which are tied to them by within-derivatives on .
Conventions committed to:
Readings:
Ruled-out trivializations. is an infimum over all fractional schedules of capacity , which form a nonempty set, never over an empty set or over Algorithm 2's own schedules. The re-solve at an arrival sees only the alive jobs and the new one, and its schedule must be optimal, not merely feasible. A sorry-free sanity file exhibits an instance, , and an explicit run satisfying every hypothesis of the goal.
Infrastructure. A complete development needs:
The first three are reusable for other continuous-time scheduling LPs. Milestones 1, 8 and 9 are self-contained measure theory, milestones 2–7 form the duality core, and milestone 10 assembles the chain.
A large language model (LLM) answers a request in two phases. In the prefill phase it reads the whole prompt; in the decode phase it generates the answer one token at a time, because each new token depends on all previous ones. Serving engines such as vLLM, SGLang and Sarathi-Serve run the GPU in iterations: each iteration processes one batch that may mix prefill tokens of some requests with single decode tokens of others, up to a token budget . Which tokens enter each batch is decided by a batch scheduling algorithm, and providers want to know how much traffic a given server can sustain and which scheduling rules achieve that.
Dai, Deng, Li and Peng (arXiv:2504.07347v3, 2026) cast this as a queueing problem: a two-class batch-service queue in which one batch couples the two classes through a shared budget, and a request contributes many tokens per batch in prefill but at most one in decode. Their Theorem 2 identifies the maximal throughput of a single server and shows that a broad class of practical schedulers attains it. The proof method is the fluid-limit approach to stability of stochastic processing networks (Dai 1995; Dai and Harrison, Processing Networks, 2020).
Time is divided into integer slots. A batch with token load (its number of tokens) takes
slots (eq. (4)). Here are integers and is a block size dividing (Assumption 1).
Requests are labelled in order of arrival. Request brings prefill tokens and decode tokens. The arrival counts of the slots are i.i.d. with mean , the sizes are i.i.d. with means , and the two sequences are independent.
The state at the start of a slot is
where is the remaining time of the current batch, the set of requests in the system, and the unprocessed prefill and decode tokens of request . When the algorithm picks subject to the following feasibility rules (eq. (6)):
The batch then runs for slots. When it finishes, requests with no tokens left depart, and new arrivals join at the end of every slot. The total number of unprocessed tokens is .
An algorithm is work-conserving if it forms a full batch () whenever the supply is at least . It is K-FCFS if, whenever a request receives a decode token, every request still in the system receives at least one token.
Part 2 is the corrected form of the paper's "the DTMC is positive recurrent". The labelled state cannot recur, because each new request carries a new label.
These follow the order of the paper's argument:
Theorem 2 gives a sharp stability threshold for a single LLM server: the arriving token workload per slot, , against the maximal processing rate of full batches. It shows that every work-conserving K-FCFS scheduler, a class containing Sarathi-Serve-style chunked-prefill schedulers, is throughput-optimal. Schedulers that do not mix prefill and decode tokens in one batch can lose throughput. The result is the base case for the paper's multi-server, multi-class and agent-network extensions.
The paper proves part (a) in a sketch and part (b) by the fluid-limit method, with a separate Lyapunov argument in Appendix C. No part of the result has a machine-checked proof. Several printed steps are false as stated:
A formalization fixes the exact statements that hold and supplies a complete argument.
Part (a) reduces to the rate bound, a pathwise count of completed batches, and the strong law. Part (b) is where the difficulty lies. A Lyapunov drift on the total token count fails directly: while a batch is in progress no tokens are completed, so the one-slot drift is positive whenever . A drift argument must account for the batch in progress. The naive bound "every slot completes tokens on average when the system is large" also needs the supply condition (9) to hold. Requests in decode contribute at most one token per batch, so many tokens can sit in few decode-phase requests. The fluid-limit route needs bounded overtaking, and the paper's prefill version of that is false.
The Lean development (namespace LLMThroughput.TokenBudget) commits to the following:
A finite set is essential. The set of all states with small token count is infinite once labels are included, and hitting it would be a much weaker claim. Quantifying over a single named policy instead of all work-conserving K-FCFS policies would also change the theorem.
A complete development needs:
ProbabilityTheory.strong_law_ae);The pathwise model and the bounded-overtaking lemma can be reused for other batch-service systems. Proofs of any milestone, and alternative proofs of part (b) (a direct drift argument on an augmented workload), are welcome.
In the a priori traveling salesman problem with independent activation, a tour through all customers must be fixed before it is known which customers need a visit; each customer is active independently with a known probability, and the fixed tour is afterwards cut short to the active ones. The model, introduced by Jaillet and by Bertsimas as the probabilistic TSP, describes routing planned once and executed many times. The quantity of interest is the expected length of the cut-short tour, and the benchmark is the smallest such expectation over all tours.
All known approximation algorithms for the problem build a master route solution: choose a set of customers, compute a TSP tour on (the master tour), and attach every other customer to a nearest customer of by a pair of parallel edges. Shmoys and Talwar (2008) choose by including each customer with its own activation probability. With a -approximate master tour (Christofides–Serdyukov) this gives a randomized -approximation. Blauth, Neuwohner, Puhlmann and Vygen (2023) show that sampling less than the activation probability is better, and give the guarantee .
Timeline:
A finite semi-metric space has , and ; distinct customers may be at distance . Each customer has an activation probability , and an instance with depot has a customer with . A tour is a cyclic order of all of ; for a set of active customers, is cut short to , and is its length. The a priori cost is , where contains each independently with probability , and
For , is the length of a shortest tour through and .
The sampling algorithm for with samples by including each independently with probability , computes an -approximate TSP tour on , and connects the rest. Its expected approximation ratio on an instance is at most
with . An instance is -normalized if it has a depot and every other customer has activation probability .
For and there is a constant such that on every instance with a depot
The constant is uniform over all instance sizes, semi-metrics and activation probabilities. The paper's certificate gives ; the goal keeps the stated .
The chain of the paper's proof, in attack order:
Theorem 3 is the mathematical content of the paper's headline result: together with the paper's depot reduction (Theorem 1) it gives a randomized polynomial-time -approximation for the a priori TSP, improving the that had stood since the Shmoys–Talwar analysis. It also separates the sampling rule from the activation probability: Theorem 2 of the paper shows that no sampling function beats , so the right choice of is a genuine question and Theorem 3 is its current best answer.
The proof method is reusable. It encodes an unbounded family of instances by finitely many aggregated variables (hop sums, then buckets), controls the truncation error explicitly, and reduces the guarantee to the feasibility of one dual solution. The same pattern proves the paper's master-route-ratio bound (Theorem 6). The result is proved on paper with a computer-generated certificate; no part of it has a machine-checked proof. A formalization makes the reduction chain (Lemma 9 to Corollary 16) checkable independently of the numerical certificate, and reduces the remaining trust to the feasibility of one explicit point.
The obvious argument compares the sampling algorithm with an optimum a priori tour on each instance, but the instance size is unbounded and the activation probabilities are arbitrary, so no finite optimization problem captures all instances directly. Three reductions are needed and each fails in a naive form: normalization (Lemma 9) requires replacing a customer by many copies whose activation and sampling probabilities match and only up to a factor ; the passage from -dependent problems to one linear program requires bucketing and the limit ; and truncating to buckets requires an error bound that uses only the triangle inequality.
The final step is not an argument but a certificate. A full proof of the goal must exhibit some feasible solution of (Dual-Sampling-LP) with at , , and check its feasibility, which involves exponential coefficients. The paper's certificate (computed with Gurobi; data and checker at doi:10.60507/FK2/JCUIRI) has and , about variables. A proof may use any certificate.
Everything is finite: the customers form a Fintype V, and expectations are finite sums over subsets with explicit product weights, without measure theory. The definitions cover the instance with depot (six named hypotheses: semi-metric, , ), tours as duplicate-free lists of all customers with cyclic cost and cutting short by filtering, the a priori cost and , , , the sampling cost in (2), the sampling functions and (with ), -normalized instances, the hop sums , (Sampling-OP), buckets, and , (Sampling-LP) and its dual.
Conventions committed to:
HasSum.Ruled out as trivializations: an or that takes a junk value ; dividing by ; a depot sampled with probability below ; a constant chosen after the instance; tours that omit customers; and Corollary 16 at .
No TSP algorithm, polynomial-time notion or numerical certificate is formalized. The semi-metric and finite-expectation infrastructure, and the LP weak-duality step, are reusable for other master-route and sampling analyses. Contributions are welcome on each milestone, and on a formally checked dual certificate.
An apportionment method distributes the seats of a house among states in proportion to their populations. Exact proportionality is impossible with integer seats, so methods are judged by axioms. Two axioms date back to the debates over the seats of the US House of Representatives. Quota compliance asks that each state receive its exact proportional share rounded down or up. House monotonicity asks that no state lose a seat when the house grows; the Alabama paradox of 1880, in which Hamilton's method took a seat from Alabama when the house was enlarged, is the classic failure. The two axioms can hold together. Balinski and Young (Mathematics of Operations Research, 1979) and Still (SIAM Journal on Applied Mathematics, 1979) characterized the methods satisfying both through a recursive, seat-by-seat construction. Gölz, Peters and Procaccia (EC 2022) later gave a description by a fractional matching polytope.
Cembrano, Correa, Schmidt-Kraepelin, Tsigonias-Dimitriadis and Verdugo (arXiv:2410.23869, Mathematics of Operations Research, 2025) give a third characterization, by a network-flow linear program. It replaces the recursive construction with the vertex set of a polytope that can be written down and optimized over. This mission formalizes that characterization, Theorem 3 of the paper.
An instance is a pair . Here is a vector of strictly positive integers (the populations of the states) and is an integer, the house size. Write ; the quota of state is .
A solution assigns to every instance one vector with . It is defined for every number of states and every population vector. It is quota-compliant if always. It is house-monotone if componentwise whenever . The set of apportionments such solutions produce is
For seats, the network-flow linear program (1)–(4) has a variable for each state and seat , subject to
Its feasible region is and its set of extreme points is . The count is the number of seats state holds after seats.
The lookahead is the number of seats the LP must model so that its first seats are exactly the house-monotone, quota-compliant ones. For a vector and , let . Let be the least with . Set unless , in which case . Then , , and
The Lean names are IsPop, Solution, QuotaCompliant, HouseMonotone, calA, K, calE, A, S, kStar, tau, Phi, all in the namespace MonoApport.Flow.
The result. Theorem 3 turns a recursive definition into a polyhedral one. The apportionments at house size that some house-monotone, quota-compliant solution can produce are the projections of the vertices of a network-flow polytope with seats. Optimizing a linear objective over all such apportionments is then a linear program of size . The paper also bounds the lookahead: for , and the bound is tight up to constants. Through the correspondence between methods and solutions (Lemma 2 of the paper), the theorem also characterizes house-monotone, quota-compliant methods. It underlies the paper's construction of randomized methods that are house-monotone, quota-compliant and ex-ante proportional (Theorem 4).
The formalization. The paper proves Theorem 3. None of the statements here has a machine-checked proof, and the Balinski–Young characterization is cited by the paper rather than proved in it. A formal development would check the full chain: total unimodularity of an interval-type constraint matrix, integrality of the polytope, the lookahead bound of Lemma 5, and the combination with the Balinski–Young construction. It would also make the network-flow polytope and the lookahead available to later work on apportionment.
The inclusion looks routine: the seat increments of a house-monotone, quota-compliant solution give a 0/1 feasible point. But that point must have seats, and it must be an extreme point, which requires the integrality of (1)–(4).
The reverse inclusion is the hard part. A vertex of the LP with seats need not extend to a quota-compliant sequence: a seat assignment can respect every quota bound up to and still force a violation a few seats later. The lookahead is designed so that this cannot happen. However, is defined by a recursion over extreme points of LPs of other sizes, and it is not monotone in : for the values are . An argument that truncates a vertex for seats to one for seats, or assumes , is therefore unavailable.
Closing the inclusion also needs the Balinski–Young construction never to get stuck: must be nonempty along every sequence it builds. The paper takes this from Balinski and Young without stating it separately.
Populations are p : Fin n → ℕ with IsPop p ( and every ); house sizes carry 0 < H. A solution is one Lean function Solution := ∀ {n}, (Fin n → ℕ) → ℕ → (Fin n → ℕ) defined on vectors of every length. quantifies over such families, exactly as in the paper; a per- sequence of apportionments would be a different object. House monotonicity is axiom (c) with three house sizes; the one-step form is Proposition 8, a milestone. LP points with seats are x : Fin n → Fin L → ℝ. Seats are 0-indexed, so column is seat , and the quota bounds at column use . Floors and ceilings are Nat.floor/Nat.ceil of the nonnegative rational quantity computed in . is Set.extremePoints ℝ (K p L). The minima and maxima defining and are sInf/sSup on , whose sets are nonempty, and finite where a maximum is taken, wherever they are used. The convention is the function ext. The goal compares subsets of : the image of under the cast equals .
The goal must not be read with integer vectors on both sides. Writing would silently ignore non-integral and empty the inclusion of its content.
A complete development needs:
Matrix.IsTotallyUnimodular;The first two are reusable well beyond apportionment. Proofs of any milestone are welcome, and so are proofs of the cited Balinski–Young theorem and of the properties of the paper uses (, and the finiteness and nonemptiness of the sets in its recursion).
The product-mix auction was developed in 2007–8 for the Bank of England (Klemperer 2010) to sell many differentiated goods (loans against different qualities of collateral) in a single round. Each bidder submits a list of simple bids, each naming a price for every good and a quantity, and the auctioneer chooses prices and allocations that respect every bid. Baldwin, Goldberg, Klemperer and Lock (arXiv:1909.07313v3, Mathematics of Operations Research, 2024) make the auction usable with positive and negative bids, a bidding language that expresses every strong-substitutes valuation (Baldwin–Klemperer 2019). The auctioneer then faces two computational tasks: finding a market-clearing price, and splitting the goods at that price among the bidders so that every bidder receives a bundle it demands. This mission formalizes the second task, the allocation algorithm ALLOCATE and its correctness and iteration bound (Theorem 19, p. 23).
There are goods and a notional reject good ; . A price is , extended by . A bid has integer entries and weight , with . At prices it demands the goods and is marginal if it demands more than one. Where no bid of a list is marginal, the list demands the bundle , with the good demands. In general the demand is the discrete convex hull of the set of bundles demanded at non-marginal prices arbitrarily close to . The indirect utility function is
and is valid if is convex. It is -valid at if is convex on the open -ball , and locally valid if it is -valid for some .
Each bidder has a valid list ; the aggregate list is their concatenation. The allocation problem (§2.5): given an integral price and a target bundle , find bundles with .
ALLOCATE works on generalised allocation problems (Definition 4), with partial allocations and residual supply . Its progress is measured by the marginal bids graph : the multigraph on with an edge labelled whenever bidder has a bid demanding both and . Each loop iteration calls FindParams, which returns either a demand cluster (a connected component of the -labelled edges) with at most one link good, or a cycle-link good of a multi-bidder cycle with an incident label . It then runs UnambiguousMarginals on the cluster or ShiftProjectUnshift on , followed by NonMarginals. ShiftProjectUnshift shifts 's bids by and finds a nearby price by submodular function minimisation (SFM) on the Lyapunov function . It then projects every bid, undoes the shift, and returns to .
For valid integral bid lists with weights , an integral and , any FindParams output rule meeting Lemma 10 and any SFM oracle that minimises submodular functions, there is
such that after loop iterations every bid list is empty, every SFM call made was on a submodular function, and the partial allocations satisfy with .
Theorem 19 is the paper's main contribution (p. 5). With the price-finding method of §3 it makes the strong-substitutes product-mix auction computable in polynomial time, using only the bids. The allocation step is the delicate one: at a market-clearing price, bidders cannot simply be given any bundle they demand (p. 12), and random perturbation would need exponentially small amounts. The authors report Haskell and Python implementations of both algorithms and experiments on random instances (pp. 5, 27–28).
The paper proves the result, but no part of it is machine-checked. The mission adds to the platform a bidding-language layer (bids, demand as a discrete convex hull, local validity) and an algorithmic layer (allocation problems, valid reductions, the marginal bids multigraph, an SFM oracle). Both layers are reusable for later work on product-mix auctions and on discrete-convex equilibrium computation. Formalizing the proof will also check two printed slips found during planning: the definition of a closed path in FindParams, and the second Lyapunov difference .
Dividing bid by bid fails: each bid's choice among its demanded goods is constrained by the others, and independent choices can leave (p. 10). The two procedures that allocate directly cover only demand clusters with at most one link good. When ties form a cycle through several bidders, the algorithm must change the problem without losing a solution. The step to justify is Proposition 14: after a -shift of one bidder, the residual supply is still demanded at a price of the special form . This needs local strong-substitutes valuations, the matrix identity of Lemma 26 and an integrality argument. The edge count drops in Lemma 17 because the shift enters a telescoped cycle identity exactly once. Local validity must also be tracked through every removal of bids (Proposition 6, Lemma 9), since global validity is lost after the first NonMarginals call.
Goods are Fin (n + 1), with 0 the reject good. Prices are Fin n → ℝ, extended by ; the ball is Metric.ball on Fin n → ℝ. Input bids are integral (IntBid). The run uses real bid vectors (Bid), because of the shifts, and does not force the reject entry to : ShiftProjectUnshift is read literally when . Bid lists are Lists. Bundles, partial allocations and residuals are ℤ-valued and carry a reject coordinate; the goal drops it. Demand is one definition, the discrete convex hull of nearby non-marginal bundles, used at every price.
FindParams is "not fully specified" (p. 23). The goal quantifies over every selector that returns what Lemma 10 allows, which covers every walk of FindParams and PriorityParams. Lemma 10 is posed with the corrected notion of a closed path; a counterexample to the printed one is in its statement. The SFM oracle is arbitrary on non-submodular inputs, and the goal asserts that every call it receives is submodular. Running time is rendered as the iteration bound together with the per-iteration structure (one selector call, at most two SFM calls). No machine model is formalized. Submodularity is the published NonmonotoneSubmod.Shared.Submodular.
The goal is not "an allocation exists" (that is Theorem 4) and not "the loop terminates" (that drops the bound). It is not posed for one fixed FindParams implementation or for an oracle correct on every input, which would narrow the quantifiers. It does not leave the oracle unconstrained without the genuineness clause, which would let a junk price through.
Contributions welcome: the bid-list layer (Proposition 6, Lemmas 9, 13, 16), the combinatorics of (Lemmas 10, 12, 17) and the matrix Lemma 26 are independent entry points.
Offline reinforcement learning and off-policy evaluation start from a single logged trajectory of a controlled system. The policy that generated the log is often unknown, history-dependent and not stationary. Model-based methods first estimate the transition probabilities of the system from this log, then plan or evaluate policies in the estimated model (Agarwal, Kakade & Yang, 2020; Li et al., 2024). How many samples that estimate needs is the question of Banerjee, Honnappa & Rao.
For an uncontrolled, geometrically ergodic Markov chain on states, Wolfer & Kontorovich (2021) showed that the transition matrix can be learned to accuracy in the -norm from of order samples, where is the smallest stationary probability, and that this rate is minimax. Banerjee, Honnappa and Rao extend this to controlled chains whose controls may depend arbitrarily on the past. Stationarity, irreducibility and aperiodicity then need not hold.
A controlled Markov chain with states and controls consists of:
Both processes are adapted to a filtration , and
The controls are otherwise arbitrary.
From a sample of length , the visit counts are and . The empirical estimator is , and its error is measured by
Three conditions control the chain:
The uniform mixing coefficient compares the conditional law of the window given the whole history up to with its unconditional law. With the paper defines
and , . Here depends on only.
(a) Sample complexity. There are a universal and a positive function such that every controlled Markov chain satisfying Assumptions 1, 2 and 4 has, for and ,
The printed threshold lacks the second and third terms and is false without them: i.i.d. uniform states satisfy all assumptions with , but the printed threshold is then , far below the samples that are needed.
(b) Minimaxity. This is the paper's Appendix G.3 Part 1. For (a universal threshold), and , let be the transition matrix on states whose first rows are and whose last row is perturbed by in consecutive pairs of coordinates (the page takes even; for odd the leftover coordinate is left unperturbed). These chains exist. They satisfy the three assumptions with , and . For and ,
Since on this family, the term of (a) cannot be improved beyond a universal constant.
Clause (a) gives an estimate of all transition matrices from one trajectory logged by an arbitrary adapted policy, with explicit dependence on the return-time constant , the visitation constants and the mixing constant. Error bounds for off-policy evaluation and for recovering optimal values follow from it in the paper's Section 5. Clause (b) shows that no estimator does better than the empirical one by more than a universal factor in the leading term.
Neither clause has a machine-checked proof. Four printed statements on the path are false as stated and are posed here in corrected form, each with a counterexample in its item:
Proposition 3 is posed in the regime where its printed bound holds. A complete formalization would give the first checked minimax result for estimating a controlled Markov chain. It would also give the first checked concentration inequality for visit counts of a non-stationary mixing process.
Under arbitrary adapted controls the visit counts are not sums of independent or stationary terms, and the number of transitions observed from a state is random and correlated with the transitions themselves. Applying a fixed-sample-size concentration bound row by row therefore fails. The deviation of around its mean has to be controlled by a Bernstein-type inequality for non-stationary, geometrically mixing bounded sequences, with constants that depend on the mixing rate alone. The constants must not depend on , or the chain. Such an inequality is not in Mathlib. The lower bound needs Fano's method, or an equivalent, for path laws of Markov chains.
Fin d and controls Fin k, with , and time is from .Filtration ℕ. It carries adapted , , row-stochastic matrices and the conditional transition law.A complete development needs several pieces of infrastructure, all reusable beyond this mission:
Contributions of any of these, and proofs of the milestones, are welcome.
A finite game can be split into simpler pieces. Candogan, Menache, Ozdaglar and Parrilo (Math. Oper. Res. 36 (2011)) showed that the space of finite games is the direct sum of potential, harmonic and nonstrategic games: potential games have pure equilibria and well-behaved learning dynamics, harmonic games generalize matching pennies, and nonstrategic games do not affect anyone's incentives. The decomposition is used to approximate a game by the closest potential game and to transfer equilibrium and dynamics results from the potential component to the original game.
Their decomposition depends on a uniform measure on each strategy set and an unweighted inner product. As a result it is not invariant under transformations that leave the strategic content of a game unchanged. The most basic such transformation is duplicating a strategy: giving a player a second, payoff-identical copy of one of her strategies. Abdou, Pnevmatikos, Scarsini and Venel (arXiv:1901.06048v2, 2020; Math. Oper. Res. 2022) introduce a weighted family of decompositions, parametrized by a measure vector and a co-measure vector, and show that duplication commutes with it once the weights are transformed accordingly. This mission formalizes that result together with the weighted decomposition it rests on.
There is a finite set of players. Player has a finite strategy set ; is the set of profiles , is without player , and is with player 's strategy replaced by . A game is a vector of payoff functions ; the games form a real vector space .
A measure vector assigns a strictly positive weight to every strategy; is the product measure and the total mass. A co-measure vector assigns to player a strictly positive function of the other players' strategies. A game is
Games carry the inner product .
Duplication. Collapse each strategy set by a map . The extended game is , the extended co-measure is , and an extension of is any strictly positive measure vector whose mass on each fibre is . Duplicating into is the case , , all other maps the identity: then .
Write for the -decomposition of . Then
stated as: a triple of games on is a -decomposition of if and only if it equals the extension of . Both directions are content: one is uniqueness for the extended weights, the other the invariance of each class.
every game having exactly one decomposition and the three classes being pairwise orthogonal. Proposition 2.10 () and Lemma 3.14 (each class is preserved by extension) are the other main milestones; Lemmas A.1–A.11 and Propositions A.3–A.9 of the appendix are the intermediate steps, in the order of the milestone list.
The result says that the potential, harmonic and nonstrategic parts of a game are properties of its strategic content and not of the way it is written down, provided the measure is split among copies of a strategy and the co-measure is copied. Duplicate strategies appear whenever a game is derived from an extensive form or a mechanism, so a decomposition that is not invariant under duplication assigns different "closest potential games" to the same strategic situation. The same weighted machinery gives the paper's invariance results for relabellings and scalings and the elimination of duplicates (Theorem 3.19, derived from Theorem 3.15).
All results are proved in the paper. None of them is formalized: the platform has the uniform-weight decomposition of Candogan et al. (Theorem 4.1 of that paper, proved), with an unweighted inner product and a pseudo-inverse-based definition of the projections, but no weighted classes, no co-measures and no statement about duplication. This mission adds the weighted definitions, the weighted decomposition with its uniqueness and orthogonality, and the commutation theorem.
The commutation is an immediate consequence of two facts, and both carry the work. The first is uniqueness of the -decomposition on the larger profile set: this is Theorem 2.11 itself, whose proof needs the weighted flow operators, their adjoints and the orthogonality of normalized potential and normalized harmonic games under . The second is that extension preserves each class, which fails for the obvious guess at the extended co-measure: the definition printed in the paper splits between the two copies, and with that choice a potential game's extension is no longer potential. Only the copied co-measure works. The weights also matter for normalization: without splitting between the copies the extended game is not normalized.
ι, strategy sets finite types S i, profiles ∀ i, S i, and is Function.update s i t. A game is ι → (∀ i, S i) → ℝ.μ i : S i → ℝ with strict positivity as a hypothesis; a co-measure γ i is a positive function of the full profile that is invariant under changing coordinate i.IsDecomposition μ γ g n p h in the order (nonstrategic, potential, harmonic) of (2.18); no decomposition function is defined, since Theorem 2.11 makes the triple unique.A statement asserting only that the extended triple is a -decomposition of would be Lemma 3.14 and not the goal: the goal also excludes every other decomposition.
The weighted classes, inner products and flow operators are reusable for the paper's other invariance results (relabelling, pseudo-translations, scalings, elimination of duplicates) and for weighted versions of the closest-potential-game problem. Proofs of any milestone are welcome; the appendix lemmas are independent finite linear-algebra statements.
Search games model a Searcher looking for an object or a person whose location is chosen adversarially: a lost hiker, a mine, a hidden explosive device, a fugitive. In the classic search game on a tree, a Hider stands still at a point of a tree network, and a Searcher starts from the root and moves at unit speed. The payoff is the time to find the Hider. Gal (1979) solved this game for every tree. Its value is the total length of the tree, and an optimal Searcher randomizes over depth-first searches.
In practice, searchers often get hints: a witness who saw the hiker turn left, a sensor reading, a dog that picks one trail. Such hints are useful but fallible. Alpern and Lidbetter (arXiv:2303.13378, Operations Research, 2025) model this by a signal at each branching point. The signal points to the branch containing the Hider and is correct with a known probability . They solve the resulting game exactly on every binary tree. The value, the optimal Hider distribution and the optimal Searcher strategy are all given in closed form by a recursion on the tree.
Timeline. Gal (1979) solved the game without signals on trees, with value . Biased depth-first strategies of the Searcher were introduced in other contexts by Alpern (2010) and by Alpern and Lidbetter (2014). Alpern and Lidbetter (2025) solved the game with signals of accuracy , which as reduces to Gal's.
A rooted tree is a finite tree whose arcs have positive lengths, with a distinguished root . Write for its total length and for the distance from the root to a node . Every node other than the root has degree three (a branch node) or one (a leaf node). The root has degree one or two, and in the second case it is also a branch node. At a branch node , the part of the tree beyond splits into two branches and .
The Hider picks a leaf node. The Searcher performs a depth-first search from at unit speed. On her first arrival at a branch node on the way to the Hider she receives a signal, either 1 or 2, naming the branch that contains the Hider. It is correct with probability and wrong with probability , where . She then chooses which branch to search first, as a function of the signal. There are four such actions: and ignore the signal, follows it, and does the opposite. If she enters the wrong branch first she searches all of it and returns, which costs twice its length. The payoff is the time until she reaches the Hider. The Hider maximizes and the Searcher minimizes its expectation.
The mean depth of with respect to a probability distribution on its leaf nodes is
The Hider distribution is defined by recursion on the tree. On a single arc it is the point mass at its leaf. At a root of degree one it is the distribution of the subtree. At a branch root with branches of lengths , call the favored branch if , where . Then
Write . At a branch node with favored branch , the favoring bias is
For every rooted tree with positive arc lengths and every :
All three parts are stated, for every tree and every in the model's range. Nothing is fixed to a special tree or a special .
The theorem gives a complete closed-form solution of a search game with imperfect information, on every tree. The value interpolates between Gal's (as ) and the mean depth (at ). It quantifies how much a signal of accuracy is worth to the Searcher. It also shows that always following the signal is almost never optimal: the Searcher should sometimes go to the favored branch without looking at the signal. The paper derives explicit formulas for penultimate nodes (Corollary 8), monotonicity of the value in (Proposition 9) and the value on trees of constant depth (Corollary 10) from it.
The result is proved in the paper. To our knowledge no part of it has a machine-checked proof, and Gal's theorem for the game without signals is not formalized either. This mission produces a formal model of depth-first search games on weighted trees together with the full solution of the signal game. The model consists of trees as an inductive type, leaves and branch nodes as finite types, and the expected search time of a pure strategy.
The natural induction on the tree has to compare games of different sizes. At a branch root, the Searcher's pure strategies on the whole tree are combinations of a root action and arbitrary pure strategies on both branches. Reducing this game to the matrix of Table 1 requires an argument that optimal play in the branches can be composed with the root choice in both directions. A Hider strategy must be shown to guarantee the value against every combination, not only against strategies of the β-form. The mixing weights of the Hider distribution also depend on mean depths that are themselves defined through the distribution, so the induction must carry the identity of Proposition 6 alongside the value. Solving the game then needs the sign of the slope and Lemma 2's bound on each branch. A Hider distribution proportional to lengths, which is optimal without signals, is not optimal here.
Trees are an inductive type RTree with constructors for a single arc, an arc leading to a subtree, and a fork with two branches. This also admits interior nodes of degree two and forks whose branches start with a fork, which is the paper's own conversion of arbitrary trees to binary trees by arcs of length zero. Every arc has positive length. Signals and branches are booleans, and an action is a map from signals to the branch searched first. A pure Searcher strategy assigns an action to every branch node. The payoff is the expected search time. Signals off the path to the Hider do not matter, so it is computed from the marginal law of each signal on the path, and no joint law is assumed. Mixed strategies are probability vectors over all pure strategies. Value and optimality are the published matrix-game notions ZeroSumLP.DantzigExt.MatrixGame (min-max and max-min strategies of a finite zero-sum game). On a tie branch 1 is favored, and then .
Neither the value nor the mean depth is defined by the formulas being proved. The value is the matrix-game value of the expected-time matrix. The mean depth is the sum of Definition 3, not the recursion of Proposition 6. The Hider's optimality must hold against every pure Searcher strategy.
A complete development needs finite sums over the leaves of a tree, the expected-time recursion, minimax for the game, and the induction of Theorem 7. The tree model and the fact that a finite game's value composes over subtrees can be reused for other search games on trees. Contributions to any milestone, or to Gal's theorem as a by-product, are welcome.
This problem asks for a formal proof of the complete conditional geometric K24 change-of-slice result, including its regularity obstruction. The source gives informal analytic arguments; this publication does not claim a new proof or a new unsolved conjecture for the standard perturbation lemma. It does not assert existence of the still-missing geometric organizer in the four-dimensional Einstein research program.
Let be a closed smooth real four-manifold with an actual common smooth circle action. Write for its normalized Haar average on the relevant tensor, covector, or vector bundle and . Let the positive metrics and be invariant under that same action; the actual nearby positive metric need not be invariant. The scalar is arbitrary. Define
where , is the symmetrized covariant derivative with factor , and . These are actual geometric differential operators, not freely supplied linear maps.
Fix the numerical data for a uniformly bounded local finite-cover system, metric ellipticity and coefficient bounds, , and a uniform pullback bound for the common action. These bounds are fixed before the conclusion constants are chosen. Covering degree is not globally bounded, and the downstairs overlap count is kept separate from the internal coordinate atlas on each covering manifold. The proposition requires all of the following.
Invariance makes the middle term vanish. On the genuine zero-Haar-mean tensor sector, identify the difference of the fixed-reference and re-anchored derivatives as
The target also includes the actual connection/Bianchi coefficient expansions, principal-symbol identification by a quadratic-jet test and its intrinsic norm bound, sector preservation and equivariance. It requires the displayed variation to be the Fréchet derivative in the specified section norms on a positive-radius metric neighborhood, not just a pointwise or directional derivative.
For every real , with the corresponding fixed local Sobolev coefficient/atlas bounds, require a uniform with
The Sobolev clause is not restricted to integer order and does not impose higher Hölder regularity on the metric. It uses local real-order metric and inverse-metric bounds; it does not impose a fixed global bound on the degree-dependent norm of the whole metric.
Prove the natural estimate by a uniform constant times . For the shifted pair, both metric differences must instead be controlled in . The actual Bianchi–Killing/rough-Laplacian identity is also included.
Geometric inverse transfer. In each stated pair of actual zero-mean section spaces, suppose the re-anchored projected operator is a bounded linear isomorphism with inverse bound (or ). If that bound times the norm of the actual difference operator is strictly below , prove that the fixed-reference operator is an isomorphism with inverse bound at most (respectively ), including surjectivity and the corresponding Banach-dual gap. Mere absence of kernel is not substituted for the initial isomorphism. Norm, completeness, Haar integrability/boundedness and projection facts needed for this argument are requested conclusions about the concrete spaces; they are not assumed copies of the desired theorem.
Actual flat-torus sharpness. On the genuine four-torus with coordinates of period , use the flat metric, the circle translation in , and
Require positivity of for , finite norms, , bounded norms, and a lower bound for the norm of the projected actual vector-operator difference tested on . Consequently no uniform shifted estimate using only the metric difference can hold. This is a statement about genuine torus tensors and operators, not an abstract sequence of scalar exponents.
Norm and formalization choices. The definition packages specify full big Hölder norms from actual iterated derivatives and top-order Hölder seminorms, hierarchical local finite covers, and real-order Bessel–Sobolev norms with explicit partitions. Sobolev carriers use the continuous/C² representatives justified by the requested ranges; their completeness and norm properties remain to be proved. The adapted Sobolev norm is an explicit upstairs sum and is not identified with downstairs independently of covering degree. Haar averaging is pointwise in finite-dimensional fibers, avoiding an unsupported assumption of norm-continuous action on big Hölder space. The projection bounds are and ; and apply only in the isometric case. Raw inverse, derivative and integral definitions are totalized in Lean, while positivity, regularity, integrability and the analytic properties are enforced by the full statement's hypotheses or required conclusions. Definitions have no admissions or new axioms. There is exactly one intentional unproved theorem placeholder.
Remaining application boundary. K24 does not construct the common marked action, the required same-window / closeness, or the adapted re-anchored inverse from an arbitrary Einstein degeneration. Those organizer inputs remain open. The nonlinear diffeomorphism-chart and quadratic-remainder applications in K16/K21 are separate supporting questions; they require their own loss-aware regularity hypotheses/proofs. Neither those applications nor the original Einstein conjecture is claimed proved by this publication.
The 3SUM problem — does an integer array contain three values, at three distinct positions, that sum to zero — is a canonical benchmark of fine-grained complexity. Hundreds of reductions sit beneath it in the 3SUM-hardness lattice, so its worst-case exponent governs the reported complexity of convex-hull degeneracies, motion planning, and many computational-geometry tasks. On the real-RAM side the best known bounds are barely subquadratic; on the integer side, Alman and Vassilevska Williams opened a line of subquadratic deterministic word-RAM exponents built on truly subquadratic triangle detection in lopsided graphs.
A recent development is that the entire algorithmic pipeline — data structure, compiled word-RAM program, and runtime certificate — has been written down in Lean 4 and machine-checked, turning a numerical-exponent claim into a verified theorem. Along the way a refinement ladder formed, each step exported as a theorem EndStatement.ThreeSum.SolvedInTime r against the same benchmark specification:
ThreeSum1960614 tree here);The benchmark model is the source word RAM of the Alman–Vassilevska Williams formalization (EndStatement, already on the platform in TrulySubcubicAPSP_SourceSpecification): a deterministic machine over signed words of width with arithmetic, memory, and conditional-jump instructions. One says SolvedInTime r when for every magnitude exponent there is a single finite program , a width bound , and a time function with for some — the rational-power encoding of — such that , run at every width , decides 3SUM on every instance of integers of absolute value at most within steps. Instances are functions Fin n → Int; yes requires the three summands at three distinct indices.
i.e. deterministic 3SUM in word-RAM steps. The constant is hard-coded: this mission certifies this exact exponent, the sharpest point of the current chain.
The proof is the ternary-radix refinement of the construction: the same color-coding data structure reorganized around base-3 digits, banks, and queries, compiled to an explicit machine program, with the runtime charged combinatorially stage by stage. The milestone list follows the costing chain of the source: radix-3 machinery and the ternary data structure, the principal-cost certificate (, the bank term ), the finite-block certificate (), the frontend budget (), the executed colored solver (), and the exported benchmark target ().
The result is, at the time of writing, the best formalized deterministic 3SUM exponent available anywhere: previous formalized entries on this platform bottom out at . Once proved end to end here it becomes the platform's record value for this benchmark, and every lemma of the ternary layer becomes reusable platform infrastructure — falsifiable, importable, and improvable by others, since a cheaper stage immediately yields a better SolvedInTime value by the same costing bridge.
Formalizing it also stress-tests something beyond the number: an end-to-end compiled program execution with a certified asymptotic runtime, not just an abstract algorithm. The runtime margins are certified against strict gaps ( at the largest scale), so the verification is quantitative, not just qualitative.
The difficulty is not one deep lemma but a long, load-bearing chain: thousands of small Meets-specifications about program fragments, the radix-3 generalization of the binary machinery, entropy and logarithm interval arithmetic for the exponent, and the assembly of a single compiled program whose correctness and runtime must both hold simultaneously. A tempting shortcut is to postulate the data-structure spec and prove only the runtime analysis — but the benchmark statement is about one concrete word-RAM program, so nothing may be assumed about the implementation: the compiler, the machine semantics, and the runtime ledger are all part of the statement's content.
This mission is a transplant of an existing, checked Lean 4 development (Apache-2.0) pinned to this platform's default environment (Lean 4.33.1, Mathlib 0df444a…). Statements keep the source's model and names; the benchmark Problem/SolvedInTime layer is reused from the platform's existing TrulySubcubicAPSP_SourceSpecification and the preceding 3SUM trees, and only the new ternary layer is added. No sorry, no assumed oracle, no weakening of SolvedInTime to a per-instance or per-width reading is admissible.
Online platforms, social networks and marketplaces run randomized experiments (A/B tests) to estimate the effect of a new feature. The standard analysis assumes that one unit's treatment does not affect another unit's outcome. On a network this fails: a treated user changes what their friends see, a treated seller changes what competing sellers sell. The resulting interference biases the naive difference-in-means estimator, often by more than the effect being measured.
Two classical answers sit at opposite ends of a trade-off. The difference-in-means (DM) estimator ignores interference: its variance is small, but its bias is first order in the interference strength. The Horvitz–Thompson (HT) estimator removes the bias by importance weighting over each unit's whole neighbourhood, at a variance exponential in the degree. Peng, Ye and Zheng (arXiv:2503.02271v1, ACM EC 2025) propose the Differences-in-Neighbors (DN) estimator, which sits in between: its bias is second order in the interference strength, and its variance is polynomial in the degree. DN extends the Differences-in-Q estimator for Markovian interference of Farias et al. (2022) to general interference graphs.
This mission formalizes DN's bias bound, Theorem 1 of the paper, and the steps of its proof.
There are units. Interference is an undirected graph without self-loops: is the set of neighbours of unit , and is the maximum degree. A treatment vector is , and unit has a potential outcome function , with observed outcome .
Assumption 1 (neighborhood interference). depends only on and on . The paper assumes this throughout.
The target is the average treatment effect
the average difference between global treatment and global control. The conditional outcome functions , are unit 's outcome when its own treatment is or , as a function of the other treatments.
The design draws i.i.d. Bernoulli, . The DN estimator is
Smoothness is measured by second-order finite differences. For and units ,
where is with entries set to . The function is -smooth if for all , , .
The proof uses the multilinear extension , the expectation of when the are independent Bernoulli.
Under Assumption 1 and the Bernoulli design, if and are -smooth for every unit , then
The proof has no numbered lemmas. The milestones are its displayed claims, in the order the proof uses them:
Milestone 6 corrects the paper. The page states the remainder without the factor of Taylor's theorem, which is false: a unit with two neighbours and at has error , while . With the restored, milestones 6 and 7 bound each treatment's error by , and Theorem 1's is their sum.
Theorem 1 is the main bias guarantee for DN. Specialized to the paper's outcome model with interference magnitude (Corollary 1), it gives bias , compared with for DM. Together with the variance bound of Theorem 2, it places DN strictly between DM and HT in the bias–variance trade-off, and it covers the Markovian interference models of Farias et al. as a special case of the graph.
The proof also shows how DN is derived: DN is the unbiased propensity-weighted estimate of a first-order Taylor expansion of the multilinear extension. Higher-order expansions give higher-order estimators with the same analysis.
As far as a search of Prove2Me shows, no network-interference model, neighbourhood potential-outcome framework or DN-type estimator has been formalized. The platform's experiment-design items are temporal (Markovian or switchback) interference models. The paper's result is proved on paper; it has not been machine-checked. The mission also states one correction (the factor above).
Most of the proof is exact finite algebra: the credit-assignment identity, the propensity-weight identities and unbiasedness are rearrangements of sums over using independence. The analytic step is the Taylor remainder. is a polynomial in variables, and Taylor's theorem must be applied along the diagonal segment from to . The second derivative along that segment must then be identified with the off-diagonal Hessian entries . One natural shortcut, bounding each Hessian entry separately and summing over all of , loses the restriction to . That restriction is where Assumption 1 enters, and it is what yields rather than . Without Assumption 1 the theorem is false: on the empty graph with two units and , the ATE is , , and .
ι with = Fintype.card ι, and treatments are ι → Bool. The graph is a Mathlib SimpleGraph, with = G.neighborFinset i and = G.maxDegree.f : ι → (ι → Bool) → ℝ. Assumption 1 is the predicate NeighborhoodInterference G f. It is a hypothesis of the goal and is omitted from milestones whose statements hold without it.mlExt h w is the multilinear extension, and bernExp p h = mlExt h (p, …, p) is the expectation under the design. Conditional expectations given set coordinate to (Function.update), which is exact by independence.condOutcome f i a, the function on the whole vector. Under Assumption 1 it depends only on .Two formalizations would make the goal a different theorem and are ruled out. In the first, the expectation is taken at a single fixed treatment vector instead of under the Bernoulli design. In the second, -smoothness is imposed on itself instead of on and : that also constrains the pairs , which are not second-order interference terms.
The development needs only Mathlib: finite sums over ι → Bool, HasDerivAt, and Taylor's theorem in one variable (taylor_mean_remainder_lagrange). Lemmas about multilinear extensions of functions on the Boolean cube are reusable beyond this mission. Proofs of any milestone are welcome, as are the variance bound (Theorem 2) and the clustered estimator results (Theorems 3–4) as follow-up statements.
Conglomerates and stand-alone firms finance projects differently. A multi-divisional firm runs an internal capital market: headquarters raises funds externally and then decides which division gets them. A stand-alone firm must raise capital project by project. A long line of work in corporate finance asks when the internal market is more efficient: Stein (1997) argues that headquarters can "pick winners", while managers with empire-building motives may over-invest.
Hwang (Management Science, 2025) adds voluntary disclosure to this comparison. Managers may disclose a project's profitability to investors at a cost, and investors set their financing terms from what is disclosed and what is withheld. Withholding information becomes a strategic choice, and the organizational form changes what a manager gains by disclosing. The paper's main result says exactly when a founder should prefer a single multi-divisional firm to two stand-alone firms.
A founder owns two projects . Each needs one unit of capital and pays , where and . The types are independent, with .
otherwise if some solves , otherwise . With one unit the manager implements the better project ( iff ). This choice is the internal capital allocation.
An equilibrium is a pure-strategy perfect Bayesian equilibrium. The disclosure strategy is a best response for every type. Investors act on admissible, Bayes-consistent beliefs. Ties are broken toward silence: a disclosure is made only if withholding it would strictly lower the manager's payoff. A structure's investment efficiency is the expected net cash flow of the implemented projects. Following the paper, each structure is evaluated at its equilibrium with the highest efficiency. These values are and . The founder chooses the structure with the larger value.
Assume . Then and exist and:
and everywhere else. The first region with included gives . On that line the two values are equal, although the printed statement claims a strict preference there.
The result. Proposition 3 splits the parameter space into three regions:
The comparison is the paper's answer to when internal capital markets create value under voluntary disclosure. Its extensions (§6) are measured against this baseline.
Formalizing it. The result is proved in the paper by hand. It has no machine-checked proof. The proof's selection argument, "the equilibrium with the highest efficiency", ranges over every equilibrium with arbitrary off-path beliefs, and it is easy to get wrong at the boundaries. A check of the printed statements against an exact enumeration of equilibria found that the strict preference in part (i) fails on . The uniqueness claims of Propositions 1 (ii), 2 (i) and 2 (iv) also fail on tie lines. A formal proof settles the corrected statement. The model, a finite signaling game with verifiable costly disclosure and break-even investors, can be reused for other disclosure models.
The selected values are maxima over all pure-strategy equilibria. The off-path beliefs are any admissible beliefs. An upper bound on therefore needs a classification of every equilibrium:
Lower bounds need explicit belief systems that support the selected equilibrium off the path. Each step mixes a combinatorial case split over types and disclosure vectors with real inequalities in . The regions of Proposition 2 meet along several curves. On each curve, every strict comparison must be checked again, because the corrections above sit exactly there. Comparing only the equilibria the paper names does not bound : an equilibrium outside that list could have higher efficiency.
Lean representation (namespace IntCapAlloc.OrgChoice):
Fin 2 → Bool. Project 1 is index 0. A message is Fin 2 → Option Bool.IsEquilibrium requires optimality against all four disclosure vectors and the tie rule per project. effSetM is the set of efficiencies of all equilibria. effSetS is the set of sums of two single-firm equilibrium efficiencies.IsGreatest, so existence is part of every claim.Conventions:
The goal is not trivial in any of the following ways:
Any of these would turn the goal into arithmetic.
Needed infrastructure: finite sums over Fin 2 → Bool, case analysis over messages, and real inequalities on the regions. Proofs of the milestones are welcome. So are general lemmas about the break-even rule (investment is monotone in the posterior mean) and about tie-breaking, which several milestones share.
A retailer that learns customer preferences online, for example an e-commerce platform choosing which products to display, observes purchases that are not all generated by the population it is trying to learn. Some arrivals are bots, fraudulent accounts or atypical buyers, and their choices can be arbitrary or deliberately misleading. Standard learning algorithms for dynamic assortment optimization under the multinomial-logit (MNL) model assume every customer follows the same choice model. Chen, Krishnamurthy and Wang (arXiv:1910.04183v2, Operations Research 2024) study what can be guaranteed when an fraction of customers are outliers controlled by an adaptive adversary.
The uncontaminated problem has an established regret theory. Agrawal, Avadhanula, Goyal and Zeevi (Operations Research 2019) proved an regret bound for an epoch-based UCB policy. Chen and Wang (Operations Research Letters 2018) gave a matching lower bound. Robustness to adversarial corruption was first analysed for multi-armed bandits by Lykouris, Mirrokni and Paes Leme (STOC 2018). The present paper carries that question to MNL assortment optimization, where one observation reveals information about a whole offered set.
There are items. Item has a known revenue and an unknown utility ; the no-purchase option has utility . In each of periods the retailer offers an assortment with . A typical customer buys item with probability and nothing with probability . The expected revenue of under utilities is
An outlier customer chooses from according to an arbitrary distribution . An adaptive adversary decides, from the whole public past (types, assortments and purchases), whether the period- customer is an outlier and which it uses, subject to sending at most outliers. Performance is measured by the TOTE regret (typically-optimal, typically-evaluated):
Algorithm 1 (active elimination) receives an upper bound . It runs in doubling epochs , , and keeps an active item set and estimates . In each epoch it computes, for every active item , the best assortment containing under the current estimates. It eliminates items whose best assortment falls below the best, and then offers for a uniformly drawn active . It re-estimates by the ratio of purchases of to no-purchases, and computes a new error bound .
There are universal constants and such that the following holds for every , , , and , every adaptive adversary with at most outliers and every tie-break in the argmax:
The second clause (6) states that if and , the regret is .
The theorem shows that a known contamination level costs an additive and otherwise leaves the uncontaminated rate intact up to logarithms. Proposition 1 of the paper shows that a cost linear in is unavoidable. Theorem 1 is also the base case of the paper's algorithm for unknown (Theorem 2), which runs copies of Algorithm 1 at geometrically spaced levels, and of its gap-dependent bound (Theorem 3).
The result is proved on paper, not formalized. The formalization would give the platform its first contaminated-bandit protocol with an adaptive adversary, and its first elimination policy for MNL assortment. During drafting, three printed statements were found to be false as stated (Corollary 1, clause (6), and line 14 of Algorithm 1); they are posed in corrected form. The printed proofs of Lemmas 3, 4 and Theorem 1 rely on the uncorrected Corollary 1. With the corrected Corollary 1, the printed argument gives Theorem 1 only with replaced by roughly in the term. No counterexample to Lemma 3, Lemma 4 or Theorem 1 is known. Completing their proofs at the printed strength is open work in this mission.
The estimator is a ratio of two counts. An adaptive adversary can choose which periods to corrupt, and it does so after seeing the past and which assortment is about to be offered. The counts are therefore not sums of independent variables. Bounding them needs a martingale (Freedman-type) concentration argument combined with a perturbation bound for the ratio, and the variance depends on the assortment used to estimate each item.
The natural route to Lemmas 3 and 4 is to bound the revenue error of an arbitrary candidate assortment by summing per-item errors, which is what Corollary 1 does. This route breaks for large . The per-item error carries the utility mass of the assortment that estimated item , not of the candidate assortment. Summing these errors therefore loses a factor . The page's argument therefore does not deliver the stated dependence, and a sharper joint concentration of the revenue estimate is needed.
Fin N, outcomes Option (Fin N) (none is no purchase), periods .ChoiceCDLP.MNL.mnlObjective w r 1 S.sel satisfying IsArgmaxSel, and every theorem quantifies over all of them.A complete development needs Freedman's martingale inequality for bounded increments with a predictable variance bound, which several Open platform items state. It also needs a perturbation analysis of ratio estimators and bookkeeping over doubling epochs. The concentration and summation lemmas are reusable for other elimination policies. Proofs of any milestone, and a corrected proof of Corollary 1's consequences at full strength, are welcome.
Retailers, airlines and platforms decide which products to offer by predicting how customers substitute among them. Such predictions rest on a discrete choice model: for every set of offered products, a probability distribution over what a customer buys. The classical models are built on random utility maximization (RUM): each customer draws utilities and buys the best offered option. Every RUM model satisfies regularity (adding a product never raises the probability of choosing an existing one), yet observed behavior violates it: the decoy (attraction) effect of Huber, Payne and Puto (1982) is a documented case where adding a dominated product increases the share of another.
This has driven a search for universal choice models, families rich enough to represent every choice model:
Chen and Mišić (arXiv:1904.11532v3) propose the decision forest model, a probability distribution over binary decision trees, which is estimable from transaction data, and prove that it is universal (Theorem 1, p. 11). This mission formalizes that theorem.
There are products and the purchase options , where is the no-purchase option. An assortment is any , the empty one included.
A customer choice model assigns to every assortment a probability distribution on , with for every product : a customer cannot buy a product that is not offered.
A purchase decision tree is a binary tree. Each split node carries a product (Requirement 1); each leaf carries a purchase option. A customer following and offered starts at the root, moves to the left child when the split's product is in and to the right child otherwise, and buys the option at the leaf reached; this option is . Two further conditions make the tree meaningful:
The depth of is the number of nodes on a longest root-to-leaf path, so a single leaf has depth . Let be the set of trees satisfying Requirements 1–3 with depth at most . For a finite forest and a probability distribution on , the decision forest model is
For every customer choice model there is a probability distribution over such that
The result. Theorem 1 says that a mixture of deterministic tree-shaped decision rules captures any choice behavior, including the decoy effect, preference cycles and every other violation of regularity, while each tree remains interpretable as a customer type. It justifies fitting decision forests to transaction data without first deciding which behavioral anomalies to allow, and it reproves that ranking-based models are decision forest models (Proposition 1, p. 9). The depth bound is the reference point for the paper's model complexity results (§4), which ask when much shallower forests suffice.
Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a reusable Lean vocabulary for choice models with an outside option, binary purchase decision trees and the requirements on them, which the paper's later results (Theorem 2 on depth for assortments, Lemma EC.1 on removing repeated products) and other nonparametric choice models can build on.
The paper calls the proof simple, and its individual steps are elementary; the difficulty is bookkeeping that the informal proof leaves implicit. The forest is indexed by all assignments of options to assortments, and the paper identifies leaves, assortments and tuple coordinates through left-to-right enumerations that a formal proof must make precise. The goal asks for a distribution over trees in , not over tuples: the constructed trees must be shown to satisfy Requirement 3 and to have depth , the tuples whose trees violate Requirement 2 must carry zero weight, and the weights must be transferred to trees without double counting. The final identity is a rearrangement of a sum of products over a function space with one coordinate held fixed, and it uses the absent-product clause and the normalization of at every assortment, the empty one included. A formalization that drops any of these points proves a different statement.
Lean conventions:
Fin N, so the paper's product is k - 1; options are Option (Fin N) with none the no-purchase option ; assortments are Finset (Fin N); probabilities are real numbers;P : Option (Fin N) → Finset (Fin N) → ℝ with IsChoiceModel P: nonnegative, summing to one over all options for every assortment (the empty one included), and zero on products outside the assortment;PTree N with leaf o and split p l r; the left child is taken when p ∈ S. Requirement 1 holds by typing; Req2 and Req3 are computed along paths; depth counts nodes, so depth (leaf o) = 1;FSet N d; the forest model (3) is forestProb F lam o S for a Finset of trees F and weights lam; a distribution over is a finite set of trees contained in FSet N (N + 1) with weights nonnegative on it and summing to one (equivalent, as is finite);o : Finset (Fin N) → Option (Fin N) is fullTree o, and its weight (EC.5) is prodWeight P o. Leaves are indexed by assortments instead of the paper's left-to-right enumeration.The goal rules out the trivializing formalizations: the trees must lie in (a distribution over arbitrary trees, or over trees violating Requirement 2, would be a different and easier statement); the choice model keeps the absent-product clause and the no-purchase option for every assortment; and the weights are nonnegative and sum to one, never signed.
Needed infrastructure is light: Mathlib's Finset sums and products over function types (Finset.prod_univ_sum, Fintype.piFinset), finiteness of trees of bounded depth over a finite label type, and induction on List.finRange N. Proofs of any milestone are welcome, as are proofs of the goal that bypass the milestones.
Fault-tolerant quantum computers implement Clifford gates cheaply and the non-Clifford T gate expensively, because T gates are obtained by magic-state distillation (Fowler, Stephens and Groszkowski). Single-qubit rotations by small, arbitrary angles appear throughout quantum simulation and must be compiled into Clifford+T circuits, so the T-count of a small rotation is a standard cost measure. Selinger's ancilla-free method uses about T gates for a -rotation by (arXiv:1212.6253), and the paper's own search puts optimal ancilla-free Clifford+T synthesis near (Sec. VI).
Wiebe and Kliuchnikov (arXiv:1305.5528) proposed non-deterministic circuits with ancillas and measurement, the gearbox circuit and its recursive composed gearbox circuit, which, like the linear-combination-of-unitaries circuits of Childs and Wiebe, turn a coarse rotation into a much finer one and whose failures are undone by a Clifford gate, so they can be repeated until they succeed. The cost of such a repeat-until-success scheme is a random variable. Theorem 2 of the paper computes its mean exactly and bounds its variance; this mission formalizes that result together with the circuit identities it rests on.
A qubit has basis ; a gate is a unitary with entry . Let and .
Gearbox circuit . Prepare ancillas in and a target in . Apply to the ancillas, then a -controlled on the target (active when every ancilla is ), then , and measure the ancillas in the computational basis. Outcome is success.
Composed gearbox circuit (Definition 1). is , and : the gate fed to the outer gearbox is the rotation the inner composed circuit enacts on success. Write for the angle with and, for ,
Cost. Level of is attempted until its measurement succeeds; the number of attempts is geometric on . Each attempt at level needs one successful copy of and one of its inverse. With the number of applications of before succeeds, Appendix A's equation (A1) reads
with distributed as and everything independent. Each uses one and one , so the number of applications of or is .
For every unitary and ,
and, for ,
Both clauses are stated as printed; the mean is exact for every .
The theorem shows that the composed gearbox reaches a rotation angle of order , doubly exponentially small in , while using applications of in expectation, with a variance of the same squared order. Since levels give angle , the gate cost scales like with a constant that depends on only through ; this is the basis of the paper's floating-point synthesis scheme, which combines a mantissa rotation with an exponent rotation produced this way (Sections IV–V).
The result has a complete written proof in Appendix A. As far as is known it has no machine-checked proof. The formalization adds three things: the circuit identities of Theorem 1 and Corollary 1 as exact matrix statements, including the boundary case ; the identification of the circuit's Born-rule success probabilities with the closed forms ; and the random-sum identities (A3), (A6) in a form where infinite moments cannot be hidden.
The computational parts are elementary but long. The real difficulty is that the theorem joins two models: a quantum circuit, whose success probabilities come from matrix entries of a post-selected block, and a nested random sum whose summands are themselves random sums. A naive approach postulates the success probabilities and proves a lemma about compound geometric sums. That approach proves nothing about the circuit: the content linking the two is milestone 3, which needs Theorem 1 at every level of the recursion and Corollary 1 to identify the gate fed to level . On the probabilistic side, the variance identity for a random number of independent summands requires finiteness of all second moments, and the bound requires unfolding a recursion whose coefficients vary with the level, which is where the monotonicity of enters.
States are vectors Fin 2 → ℂ; gates are Matrix (Fin 2) (Fin 2) ℂ, unitarity is membership in Matrix.unitaryGroup, and are indices 0, 1. The ancillas are Fin d → Fin 2, and the joint space is (Fin d → Fin 2) × Fin 2 with ancillas first; the controlled gate fires on the all-ones string. The rotation is the matrix , so is the rotation by . Because Lean's Real.tan returns at , the angles and are defined to be when the cosine vanishes, the paper's value ; the case is not excluded. is the recursively defined success unitary: the outcome- block of the one-ancilla gearbox fed with , normalized by the norm of its first column.
The number of applications of or used to enact is modelled by Appendix A's recursion (A1): Theorem 2 speaks of "a given attempt", but its proof defines as the count until succeeds, and that is the quantity formalized. Laws are Mathlib PMF ℕ with independence built into bind; the geometric law is Mathlib's geometricMeasure shifted to ; means and variances are ℝ≥0∞-valued sums.
Three trivializing formalizations are ruled out. The law of uses the circuit's Born-rule success probabilities, never supplied as an input, so Theorem 1 and Corollary 1 are needed for the goal. Moments are in , so a divergent variance is , never the junk value that would make the bound trivially true. The angle convention above excludes the false reading in Theorem 1 and Corollary 1.
Everything needed is in Mathlib: matrices, unitaryGroup, Real.arctan, PMF.bind/PMF.map, geometricMeasure. Reusable beyond this mission: the moments of the shifted geometric law and the mean and variance identities for a sum of a random number of i.i.d. summands, in ℝ≥0∞ form. Contributions to any milestone are welcome; the probabilistic milestones (3–6) do not depend on the circuit milestones except through part 1 of milestone 3.
Firms and public agencies often roll a new product, feature or policy out gradually: a few markets first, more later, every market eventually. When the rollout is itself an experiment, its schedule determines how precisely the effect of the treatment can be estimated. A staggered rollout is the common design in which treatment, once switched on in a unit, stays on. Examples are a ride-sharing feature introduced city by city, a hospital protocol adopted ward by ward, or a stepped-wedge clinical trial. The effect of such a treatment often builds up over several periods, so the analyst wants the instantaneous effect and the lagged ones. The design question is then: in which period should each unit adopt?
Xiong, Athey, Bayati and Imbens (arXiv:1911.03764, Management Science 2024) answer this question in closed form for the trace criterion. Their non-adaptive result, Theorem 3.1, says that an optimal rollout has a treated fraction that follows a fixed S-shaped curve in time, and that each adoption cohort balances the observed and latent covariates.
There are units and periods. A design assigns to every unit an adoption time , where means never treated. The treatment indicator is coded if and otherwise. The outcome model, (3.1) of the paper, is
It has unit effects , time effects , observed covariates with period-specific slopes , and known lags. Latent covariates load on random factors with covariance , and the noise has variance . The effects are estimated by generalized least squares on periods . The per-period error covariance is , and the errors are uncorrelated across periods.
By the Gauss–Markov (Aitken) theorem, which is proved on Prove2Me as VectorSpaceOpt.gauss_markov, the covariance of the GLS estimator is for the regressor matrix . The precision is therefore a deterministic matrix, (EC.2.1)–(EC.2.2): the Schur complement of the nuisance block. The T-optimal design problem (3.2) is
With , the paper defines a vector of length from explicit , ((EC.1.2)–(EC.1.3)). The S-shaped fraction of (3.4) has five stages: it is for , equals for , is linear, , for , is antisymmetric in the fourth stage, and is at the end.
Assume , , centred rows and , , and, when , . If
then for every design . Here is the set of designs whose treated fraction at every is , and , are the sets of designs whose adoption cohorts in periods have zero sum of (respectively ).
The theorem turns a combinatorial design problem over schedules into explicit conditions. The fraction of treated units follows a universal curve that depends only on , and the cohorts must balance the covariates. Two features are useful in practice. Without lags the optimal fraction grows linearly. With lags the optimal rollout starts and ends more slowly, which is what the extra stages capture. The paper uses these conditions to build practical designs (rounding the fractions to integers, stratifying on estimated latent factors) and an adaptive version.
The result is proved in the paper; this mission formalizes it. Formalizing it also repairs the record. Two statements in the printed proof are false as printed, and so is one display. The vector of Lemma EC.1.2 has an off-by-one, and its observed-covariate term is correct only when . The linear term of (EC.2.6) is summed over the wrong range. The mission states the corrected versions, each with a counterexample to the printed one. Theorem 3.1 itself is true as printed. Planning checked it by brute force on small instances, and checked the optimality of with an exact certificate for . As far as a search of Prove2Me shows, nothing about panel experimental design or GLS precision has been formalized there before.
The objective is a trace of a Schur complement, and the design enters through entries in a large regression. Expanding that objective into the separable form of Lemma EC.1.2 requires exact control of the projection onto the two-way fixed effects and the period-specific covariate slopes. This is where the printed lemma goes wrong. The relaxed problem in is a convex quadratic program with monotonicity and box constraints. Its solution is not linear when : the stage-2 values solve a linear system whose feasibility (bounds and monotonicity) holds only above a threshold in . That is the role of the cubic threshold. A natural first idea is that "spread adoption evenly" is optimal. It is optimal only for ; for the KKT system forces nonlinear stages at both ends. A second step must also be checked: the designs, whose fractions satisfy and whose cohorts satisfy the balance conditions, minimize all three terms at once.
Fin N and Fin T, with periods 0-based. A design is Fin N → WithTop (Fin T), with ⊤ for never treated, and .The comparison design ranges over all designs, never over or relaxed fractions. The coding is , not . The estimator uses only periods . Coding with or dropping the period-specific slopes would change and the covariate term, and would be a different theorem. The set can be empty for some , in which case the goal holds vacuously, exactly as the paper's "if" allows. A sanity file exhibits nonempty instances, at with and at , and reproduces a value of Example EC.1.4.
A complete development needs least-squares projections, Schur complements, centring matrices, and a KKT certificate for a monotone-constrained quadratic program. The first three are reusable well beyond this mission. Contributions to any milestone are welcome.
Ride-hailing, car-sharing and bike-sharing platforms, as well as scrip systems, move a fixed stock of reusable resources around a network. Each customer that is served relocates one unit, from a pick-up location to a drop-off location. The operator decides, customer by customer, whether to serve and with which unit. Supply can run dry at a location, which forbids serving from there. Demand also varies over the day, and the operator rarely knows the arrival rates.
Kanoria and Qian (arXiv:1903.02764v4; Management Science, 2024) propose Mirror Backpressure (MBP), a policy that uses only the current queue lengths and never estimates the rates. They prove that it is near-optimal against the best policy that knows the rates. Earlier guarantees for closed networks, such as Banerjee, Freund and Lykouris (arXiv:1608.06819), need exact knowledge of stationary rates and bound only the steady state. Classical backpressure (Tassiulas and Ephremides, 1992) and the drift-plus-penalty method (Neely, 2010) address open networks, where the no-underflow constraint is handled by idling, not by a fixed stock of units.
A closed network has a finite set of nodes and identical supply units. The state is the vector of queue lengths . In each period exactly one customer arrives. Her type lies in a finite set and is drawn from a probability vector , independently of the past. Type has nonempty pick-up and drop-off neighborhoods .
After seeing , the controller drops the customer or serves her with a pair . Serving collects a payoff , with , and moves one unit from to . Serving from requires : this is the no-underflow constraint. A feasible policy may randomize, depend on the whole history and the period, and know the rates.
Write for the expected payoff of in periods from . The benchmark is , and a policy is evaluated from its worst initial state, . The loss is .
The rates vary -slowly if . The connectedness
is the smallest rate of demand that can carry supply out of any proper node set. Condition 1 requires in every period, and .
MBP normalizes queue lengths as with , and uses the congestion function . For a type- customer it picks maximizing the score over . It serves with that pair if the score is nonnegative and , and drops the customer otherwise.
There are a universal and such that for every instance and every ,
The constants are existential and fixed before the instance. A sharper constant is a stronger result that does not invalidate the goal.
The milestones follow the paper's proof.
Theorem 1 gives a finite-, finite-horizon guarantee for a policy that is blind to the arrival rates. Its steady-state per-customer loss is for stationary demand, the same order as rate-aware state-independent policies. Under imperfect rate estimates, any state-independent policy suffers a loss of order one (Banerjee, Kanoria and Qian, 2018, Proposition 4). The bound holds for arbitrary slowly varying demand. It does not degrade in the large-market regime where and the demand grow together.
The theorem is proved in the paper; nothing in it is formalized anywhere. This mission would give the platform its first controlled closed-network model: demand types with pick-up and drop-off sets, the no-underflow constraint, and history-dependent randomized policies over a finite horizon. It would also add a fully machine-checked drift-plus-penalty argument with an underflow term. One printed statement is corrected: Lemma 1 as printed has with coefficient , which a two-node instance refutes. The milestone uses , and Theorem 1 is unaffected.
The natural route is the backpressure argument: score each pair by payoff plus congestion difference and bound the Lyapunov drift. That argument assumes that serving from an empty queue is either impossible or harmless. Here the no-underflow constraint binds. The congestion-adjusted score can be positive at an empty queue, so the policy is forced to drop customers that the fluid solution would serve. Virtual-queue workarounds fail in a closed network because fake units never leave. Linear congestion costs, as in regular backpressure, can lose a constant per customer.
The proof needs three ingredients. First, a potential whose gradient is the steep congestion function. Second, the observation that the dual gap is very negative exactly when some queue is short. Third, a growth estimate with the offset showing that absorbs once . The finite-horizon benchmark separately requires a flow-decomposition argument and LP sensitivity in the rates.
Fintypes, with 1 < Fintype.card V. Decisions are Option (V × V). Periods are numbered from , with rates phi : ℕ → Ty → ℝ.The statement has a trivializing formalization that is excluded. If or could depend on , or , the choice would make and the theorem empty. Likewise, a benchmark restricted to Markov or deterministic policies, or a supremum over an unconstrained set, would change what is proved.
The definitions of the closed network, the static planning LP with its relaxed flow balance, acyclic flows and the partial dual are reusable for other closed-network and ride-hailing results. Contributions are welcome on every milestone. The LP lemmas (4–6, strong duality, Lemma 2, Proposition 4) are independent of the policy and can be attacked first. Platform results LinearOptimization.lp_strong_duality and LinearOptimization.network_flow_decomposition_including_zero are available as tools.
Assortment optimization is the problem of choosing which items to offer a customer who buys at most one item, when each item has a fixed, exogenous price. It is one of the central problems of revenue management: the customer's behaviour is described by a choice model, and a large literature computes optimal assortments under specific models, from the general discrete choice framework of Talluri and van Ryzin (2004) to the Markov Chain choice model of Blanchet, Gallego and Goyal (2016) and Feldman and Topaloglu (2017).
An assortment is one way to sell. A seller can also run a lottery, or ask the customer for their preferences and allocate at random. Ma (arXiv:2105.10433) asks when offering an assortment is already the best a seller can do among all such selling schemes. It is the ordinal analogue of the single-buyer auction setting of Myerson (1981), where an optimal mechanism is a posted price. The answer measures what assortment optimization computes: when assortments are optimal, the optimal assortment's revenue is the economic limit of the seller's revenue, not only the best value within one restricted class. The paper shows by a four-item example (Example 1, p. 2) that a top-2 lottery can strictly beat every assortment, so the question has content.
There are items with prices . A buyer's private type is a list , a strictly ordered subset of (most preferred first; items not on the list are worse than buying nothing). Lists are drawn from a list distribution: a finite support with probabilities summing to . Write for the 'th item and for the first items.
Offering an assortment , the buyer buys the first item of on their list; is the probability that this is , and . is the largest .
A mechanism assigns, on report , item with probability . It is IC (incentive compatible) if for every , reporting truthfully maximizes the probability of receiving one of the buyer's favourite items:
, and is the optimal value of this linear program. Every assortment is an IC mechanism, so .
A prefix is an ordered subset of ; is the probability that the list starts with , and is realizable if . For nonempty , is its last item and the items before it. is the probability that is the first item of on the list, given that the list starts with . The future from dominates the future from if for all and . The distribution has history-monotone futures if, for all realizable with and as sets, the future from dominates the future from .
For a list distribution with history-monotone futures and any prices , there is an assortment with
The proof passes through a chain of relaxations , where maximizes a revenue over increasing set functions and over monotone stopping policies on the tree of prefixes. The milestones, in attack order:
History-monotone futures hold for Markov Chain choice models (hence MNL), for Elimination by Aspects, and for MNL mixed with singleton lists (Propositions 4–6). Theorem 2 therefore says that for these widely used models no lottery or other IC selling scheme beats the best assortment, and the many algorithms that compute optimal assortments under them compute the seller's optimal revenue over all mechanisms. Without the condition the conclusion fails (Example 1).
The result is proved on paper; no machine-checked proof exists. A formalization contributes a verified development of the relaxation chain (mechanisms, set functions, stopping policies on a prefix tree), which applies to any list distribution, and pins down the hypotheses of two intermediate statements that are false as printed (Lemma 1 and the "Moreover" clause of Proposition 3; see below).
The natural argument is an exchange argument: if a policy stops on a prefix but continues on with the same endpoint, history-monotone futures should make it profitable to stop on as well. This fails: a policy can earn strictly more by continuing from a dominated future than from a dominating one (p. 19, discussing Example 2), because which items it later stops on depends on the history. A pairwise comparison of prefixes is therefore not enough: the condition has to be used on all prefixes with a given endpoint at once, and the relevant quantity is not the revenue of a prefix's future but its price net of the future revenue of an assortment. The relaxation from set functions to boolean set functions (Proposition 3) is a further step that a direct argument does not supply.
Items are Fin n (0-based), lists are List (Fin n), and a list distribution is a finite support of Nodup lists with positive weights summing to one; and the empty list are allowed. Prices satisfy , the paper's standing assumption. A mechanism is a function of a list and an item, of which only the values at , are read. Realizable prefixes are the nonempty prefixes of support lists; domination, history-monotone futures, adjusted prices and tiers quantify over realizable prefixes only, so a conditional probability is never taken at . Quantifying over all prefixes would compare Lean's against positive probabilities and make the hypothesis fail for almost every distribution. Stopping policies are Bool-valued.
The goal states attainment: some is the greatest value of over IC mechanisms. A weakened IC constraint (only , or only ) would admit first-best mechanisms and make the goal false; constraint (3) is stated for every and every .
Two printed statements are corrected. Lemma 1 holds only when is the all-1 function for every , as in the proof of Theorem 2; it fails for and . The "Moreover" clause of Proposition 3 needs ; it fails for . Each corrected item lists its counterexample.
All definitions live in one module (AssortOpt.HMF.Setting); the list-distribution, mechanism and stopping-policy layer is reusable for the paper's other results (Theorem 1 on Markov Chains, Propositions 4–9, the approximation bounds of §5). Proofs of any milestone are welcome, as are follow-up missions on those results.
Quantum information carried by continuous variables, such as the quadratures and of an optical mode, is cheap to manipulate with beam splitters, squeezers and homodyne detectors, but these Gaussian tools cannot protect Gaussian states against Gaussian noise: Niset, Fiurášek and Cerf proved in 2008 that no Gaussian error-correcting code can do better than direct transmission against Gaussian channels (arXiv:0811.3128). Peter van Loock's note (arXiv:0811.3616) shows that this no-go does not cover non-Gaussian noise: a stochastic error that displaces a mode by a fixed amount with probability turns a Gaussian state into a discrete mixture, and against it a purely Gaussian three-mode repetition code (offline squeezing, two beam splitters, homodyne detection, feedforward) reduces the error probability from to .
The example is the continuous-variable analogue of the three-qubit bit-flip code. Unlike that code, it identifies double errors as well as single ones, so it improves on direct transmission without the qubit code's requirement .
A single optical mode is described by its Wigner function , a real function on phase space ; three modes by a function of and . Units are those in which the vacuum has variance .
An error pattern is a set of erring channels. After decoding it shifts the signal by and the ancillas to a syndrome point . The paper's feedforward for pattern is a linear function of that undoes the signal shift at .
For every measurable that equals on the Euclidean disc of radius around , for each pattern :
and this limit exceeds the exact direct-transmission fidelity if and only if .
The paper asserts the comparison "for any " against , an approximation valid for . With the exact direct fidelity the claim fails for small and large (, : against ), so the goal poses the comparison in its exact, corrected form. It holds for every and, for each , once is large enough.
The displays the derivation passes through, in order: the encoded state (6); the eight-term expansion (7) under three independent channels; the decoded state (8); the syndrome table, which shows that only "no error" and "error in every channel" share a syndrome; the homodyne marginal with feedforward (9); and the delta-function limit of the squeezed-ancilla marginals as .
The result. The code reduces the error probability of a stochastic displacement channel from to using only Gaussian operations, which shows that the Gaussian no-go theorem depends on the noise being Gaussian. The syndrome table also shows that a continuous-variable code has more distinguishable error subspaces than its qubit analogue: double errors are identified and corrected.
Formalizing it. The paper's derivation is a chain of displayed formulas with no stated decision regions and no fidelity formula. A formal version fixes what the feedforward is allowed to know (only the measured ), turns "the Gaussians become delta functions" into a limit theorem, and replaces the comparison with by an exact criterion. To our knowledge none of these statements has been machine-checked.
Eqs. (6)–(9) are Gaussian algebra and Gaussian integrals: tedious but mechanical. The difficulty is the limit. The feedforward is one function of , not a different correction for each error pattern as Eq. (9) is printed, and it is pinned down only near the seven distinct syndrome points. Passing to needs the squeezed marginals to concentrate on those points while the integrand, which involves the arbitrary measurable elsewhere, stays controlled. The fidelity limit then needs a second exchange of limit and integral over phase space.
(Fin 3 → ℝ) → (Fin 3 → ℝ) → ℝ, with the paper's mode at Lean index . Units: vacuum variance .Online retailers display hundreds of products in a list or a grid, and most visitors never scroll far. A customer who finds nothing appealing near the top leaves without engaging at all, so the order of the first few slots decides whether a visit turns into a click, and through it into a sale. Ferreira, Parthasarathy and Sekar (SSRN 3395992; Management Science, 2021, doi:10.1287/mnsc.2021.4130) model this with a first impression window: each customer is guaranteed to look at a number of top positions, and is hooked if she clicks at least one product there. The retailer wants a ranking that hooks as many customers as possible, without knowing customer preferences in advance, learning them only from observed clicks.
The paper shows that the offline problem, with full knowledge of the customer distribution, is NP-hard (Proposition 1), that a greedy ranking hooks at least half as many customers as the best ranking (Theorem 1), and that a learning algorithm built on any off-the-shelf PAC bandit algorithm matches that factor up to an arbitrarily small additive error (Theorem 3). This mission formalizes the last result for general customer populations.
There are products . A ranking is a permutation of ; is the product in position . A customer type is a triple :
Customers arrive with types drawn independently from an arbitrary distribution on types; the three components may be correlated. A customer facing inspects positions in order. If is the set of products she has clicked so far, she clicks the product in front of her with probability . Clicks beyond position are ignored. She is hooked, , if she clicks some product in positions . The objective is the expected hook , the expectation taken over the type and the clicks.
The marginal benefit of placing product right after a partial ranking is . The Simple Learning Algorithm (Algorithm 2) fills ranks in order. At rank it runs an -PAC algorithm for the multi-armed bandit problem (Definition 1, after Even-Dar, Mannor and Mansour 2006: with probability at least it returns an arm whose mean is within of the best) on the products not yet ranked. The reward of arm is for the current prefix , and the algorithm places the returned product at rank .
For and any -PAC black box with and , with probability at least the returned ranking satisfies
The result says that learning costs nothing in the approximation factor. The best known factor for general customer populations is the greedy algorithm's ½, and a retailer who knows nothing about attains it up to by plugging in any PAC bandit algorithm. Sample-efficient best-arm algorithms such as LUCB can be used unchanged, and the learning phase is times the black box's sample complexity (Corollary 1). The same template is reused later in the paper for the threshold-acceptance and revenue variants.
On the formal side, the mission produces a reusable model of position-based browsing with biased sequential clicks, with a proof that the bias functions do not affect the hook probability (milestone 1). It also produces a statement of an "approximate greedy" guarantee that does not pass through submodularity: the paper notes (p. 25) that the hook objective is not presented as a submodular set function. The paper's proofs are on paper only. No machine-checked version of any result of the paper is known.
The obvious route to the ½ factor is to view as a monotone submodular function of the set of displayed products and invoke the greedy guarantee. That route fails here: the objective is a function of an order, the bias functions make clicks depend on earlier clicks, and windows vary across customers. Comparing two rankings on the same customer needs a joint law of her clicks under both, which the model does not supply; the paper fixes a coupling (p. 53), and the coupled events must agree with the sequential law, which is where enters. And the probabilistic step on p. 59 that writes a conditional probability as holds only type by type, so (26) has to be argued per type before averaging. On the probabilistic side, the black box's guarantee holds conditionally on the random prefix built so far, and the union bound must be taken over ranks after averaging over prefixes.
Products are Fin n and rankings are duplicate-free lists of length . Ranks are 0-based in Lean (the paper's rank is index ). Probabilities are real numbers. A type is the structure CustomerType n with every constraint above as a field. The type distribution is a probability measure on a measurable space together with a type map . The added hypothesis TypeMeasurable τ asks that every coordinate of the type be measurable; the page treats as a random variable, and without measurability the Bochner integrals would be . The expected hook is computed from the sequential click law with bias (an explicit sum over click patterns inside the window), not from a closed form. The comparisons in (6), (10) and (26) use the paper's coupling (p. 53): one Bernoulli like-variable per product, shared by all rankings. The maximum in (23) is over unranked products, as in Algorithm 2.
The black box is formalized through its guarantee. A SimpleLearningRun is a random output ranking whose rank- product, conditionally on every prefix already fixed, fails to be -approximately best with probability at most . This is Definition 1 applied at each call (p. 58). The black box's sampling and its sample complexity are not modelled, since they enter only Corollaries 1–2. The goal rules out three trivializing readings. It does not assume that all ranks are good with probability , which is the conclusion of (24). The expected hook is not the closed form , which would make the bias decorative. And the optimal ranking is quantified over every ranking inside the event, not chosen after .
Not formalized: Theorem 3 part 2 (independent , factor , not proved in the paper), Theorems 1, 2, 4, 5, Proposition 1 and the sample-complexity and regret corollaries. Proofs of any milestone are welcome. Milestone 5 at contains Theorem 1 and could seed a follow-up.