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?
A central dispatcher that routes jobs to parallel servers is the basic model behind web server farms, cloud schedulers and call centers. When the servers have different speeds, and the speeds are not known to the dispatcher, two classical policies behave very differently. Random routing is cheap but unstable as soon as some server is slower than the average load. Join-the-shortest-queue is stable but needs the dispatcher to know every queue length at every arrival. Gamarnik, Tsitsiklis and Zubeldia (arXiv:2007.07219, 2020; Mathematics of Operations Research, 2022) ask how much memory and how many messages a dispatching policy needs in order to stay stable for every vector of server rates. A policy with that property is called maximally stable.
The paper gives two answers. A policy with one remembered server ID and an arbitrarily small message rate is maximally stable (Theorem 2.1). Conversely, a broad class of symmetric policies with bits of memory and a message rate of is unstable for some rate vectors (Theorem 2.2). This mission formalizes the positive result.
There are servers, indexed (Fin n in Lean). Each has an infinite-capacity FIFO queue. Server works at rate , and the total capacity is normalized to :
Jobs arrive as a Poisson process of rate with , and job sizes are i.i.d. exponential with unit mean, so a busy server completes jobs at rate .
The single-ID policy works as follows. The dispatcher stores the ID of one server and sends every arriving job to it. Each server sends its current queue length to the dispatcher as an independent Poisson process of rate . When server 's message arrives, the dispatcher replaces by exactly when .
Under these assumptions the system is a continuous-time Markov chain on : the vector of queue lengths (jobs in queue or in service) and the stored ID . Its transition rates are
and every other transition has rate . In Lean the generator is gen n lam α μ, and the stability region stabilityRegion n lam α is the set of for which this chain is positive recurrent.
For every , every and every ,
The rates are arbitrary in . The message rate may be arbitrarily small, and the load arbitrarily close to .
With , and the Lyapunov functions
the milestones, in order, are:
The result. Theorem 2.1 shows that maximal stability costs very little: bits of memory and an average message rate of , which can be made as small as desired (Remark 2.1). Together with Theorem 2.2, it locates the threshold at which limited memory and communication start to cost stability. Small message rates do have a price: the paper notes that the steady-state delay then degrades. The stability guarantee itself, however, does not depend on how small is.
Formalizing it. The theorem is proved in the paper (Appendix A), but it has no machine-checked proof. A formal proof needs a Foster–Lyapunov criterion for continuous-time Markov chains on a countable state space. That criterion is not on the platform and not in Mathlib: the only drafted Foster criterion on the platform is for discrete-time, aperiodic chains on . Building it against the published return-time definition of positive recurrence is reusable for every queueing-stability mission that follows.
The drift identities (A.3) and (A.4) are per-transition bookkeeping. The quadratic function alone does not work: its drift contains , and when the stored server's queue is long compared with the others it is not offset by , because the rates are heterogeneous. The memory term , scaled by , is what turns the message mechanism into negative drift. The other hard step is the conclusion itself. Passing from "drift at most outside a finite set" to positive recurrence of a continuous-time chain with unbounded state space requires the continuous-time Foster–Lyapunov criterion, which the paper cites (its reference [4], Foster 1953) and does not prove; the continuous-time version needed here is developed by Meyn and Tweedie (1993).
(Fin n → ℕ) × Fin n, with 0-based server indices. The parameters are lam (), α (, one positive real for the fixed ) and μ : Fin n → ℝ.MatrixAnalytic.Tree.IsPositiveRecurrentProcess: every state is recurrent with a finite expected return time, computed through the jump chain and the holding rates.HasSum, so convergence is part of each claim.max x 0 on reals, and is if 1 ≤ q j then 1 else 0. and are Finset.sup'/inf', so the milestones that use them assume ([NeZero n]). The goal holds for every , including .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.
The stochastic multi-armed bandit is the basic model of sequential decision-making under uncertainty: in each round an algorithm chooses one of arms, observes a random reward from that arm's distribution, and tries to play the best arm as often as possible. Since Lai and Robbins (1985) the standard of quality has been the expected regret, and an algorithm is called optimized when it attains the Lai–Robbins constant exactly. KL-UCB (Cappé et al. 2013) and Thompson sampling are optimized in this sense, and they are widely used in recommendation, clinical trials and online experimentation.
Fan and Glynn (arXiv:2109.13595v8, Operations Research 2025) ask what such optimality costs for the distribution of the regret. Their answer: every optimized algorithm has a heavy regret tail, polynomial rather than exponential, and in common families exactly truncated Cauchy. A practitioner who runs an optimized algorithm once, rather than averaging over many runs, is therefore exposed to large regret with polynomially small probability, and the paper shows that this makes optimized algorithms fragile under slight mis-specification.
Timeline. Lai and Robbins (1985) proved the lower bound for consistent algorithms in one-parameter families; Burnetas and Katehakis (1996) extended it to general models with . Audibert, Munos and Szepesvári (2009) showed polynomial regret tails for UCB-type algorithms. Fan and Glynn (2021–2024) proved that the polynomial tail is forced by optimality itself, for every optimized algorithm and every environment.
A bandit environment is , a tuple of probability laws on . An algorithm is a sequence of probability kernels: the arm of round is drawn given the past arms and rewards, and the reward is drawn from . This induces a law on histories. is the number of plays of arm in the first rounds, the mean of , , and the regret is . The -th-best arm is ; the paper assumes the arm means are pairwise distinct.
Fix a base distribution on , with cumulant generating function and natural parameter set , which contains a neighbourhood of . Tilting gives the laws ; their means form the mean set , and is the tilt with mean . The model is , and is the Kullback–Leibler divergence.
An algorithm is -optimized (Definition 2) if for every and every sub-optimal arm ,
is discrimination equivalent (Definition 3) if whenever in . Gaussian, uniform and every continuous family with a CGF finite on qualify.
For every and every arm ,
If is discrimination equivalent, then uniformly for
and (7) holds with right side . No constant is fixed: the statement asserts the shape of the tail for every optimized algorithm.
The result. Theorem 1 shows that logarithmic expected regret and light regret tails are incompatible: under discrimination equivalence the tail of , hence of the regret, decays exactly like up to order . Every higher moment of the regret then grows polynomially, and the paper derives from this that optimized algorithms lose consistency under arbitrarily small mis-specification (§4). Theorem 4 turns the same mechanism into a quantitative trade-off between regret tail and expected regret, of which the Lai–Robbins and Burnetas–Katehakis bounds are the case .
Formalizing it. The result is proved on paper; nothing of it is machine-checked. The mission states the first results on the platform about the distribution of regret rather than its expectation, on the published canonical bandit model. It adds a one-dimensional exponential family on arbitrary base laws, a likelihood-ratio change of measure for adaptive histories, and a random-index law of large numbers, all reusable for other bandit lower bounds. Three printed statements are false as written and are posed corrected (see the milestone notes), so the formal development also records the precise hypotheses under which the paper's arguments go through.
The naive route to a tail bound uses expected regret: Markov's inequality gives , an upper bound. The theorem is a lower bound, and no estimate on expectations yields one. It requires constructing an auxiliary environment in which the best arm is tilted below the second-best, changing measure along a history whose length of play per arm is random and chosen adaptively, and controlling the log-likelihood average over that random number of plays. That last step needs a weak law of large numbers for the sample means of an arm under an adaptive policy, together with the fact that the number of plays at the auxiliary environment concentrates around , which itself comes from a second change-of-measure argument (Theorem 4). Finally the bound at the single point must be spread uniformly over a window of thresholds that grows with .
Environments are the published StochasticBandit K (arms Fin K), algorithms the published BanditPolicy K, and restricted to the first rounds is banditMeasure ν π T; is armPullCount. is defined by integrability of , tilts by Measure.tilted, by klDiv and by the published banditDInf, all valued in with . Means of environments are pairwise distinct, as on p. 7; Definition 2 quantifies over such environments.
Every statement of the form "" is posed in power form: for every beyond the exponent, eventually (resp. ). A log-ratio formalization would be trivially true when because Real.log 0 = 0, and a real-valued exponent would turn an empty infimum into ; both are ruled out. Theorem 4 and Lemma 6 are posed for a class of environments closed under the replacement used in their proof, which specializes to the printed .
Not formalized: Lemma 2 (its printed scope includes environments where the paper's justification fails), Lemma 1 and Propositions 1–2 (sufficient conditions for discrimination equivalence), Theorem 2 (KL-UCB upper bounds), §4 (mis-specification), §6 (modified UCB). Contributions of proofs of any milestone are welcome, as is general infrastructure: the likelihood-ratio identity for banditMeasure and laws of large numbers along random indices.
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 Einstein metric is a smooth positive-definite Riemannian metric whose Ricci tensor is a constant multiple of the metric. This mission asks whether negative Einstein curvature can coexist with simple connectedness and vanishing second real homology on a closed four-manifold. It contains one geometric conjecture. The separate K24 change-of-slice program has its own research specification and is not a second goal of this mission.
Let be a closed, connected, orientable smooth manifold of real dimension four. Here closed means compact without boundary. Let be a smooth Riemannian metric. Suppose one real number , independent of the point, satisfies , and suppose , equivalently . Prove or disprove:
The conclusion is nontriviality, not infinitude. There is no assumption about sectional curvature, curvature pinching, symmetry, volume, collapse, or a prescribed decomposition. The target is not restricted to the standard smooth sphere: the potential class of arbitrary smooth homotopy four-spheres must be respected.
The mission reuses the published EinsteinFour definition bundle, then adds NegativeEinsteinFour. Smooth metrics live on the actual tangent bundle. The negative Einstein condition uses one spatially constant negative scalar and the coordinate Ricci tensor, with the sign convention giving positive Ricci curvature on the round sphere. Orientability is encoded by a clopen orientation component selection in the orthonormal-frame bundle. The second-homology condition uses the actual real singular homology object being zero; the conclusion uses the actual based fundamental group.
The exact environment is Lean leanprover/lean4:v4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. Both definition files and the conjecture declaration compiled successfully on October 23, using precompiled Mathlib artifacts. The definitions contain no sorry; the conjecture has the required unproved placeholder. Independent Astra Ultra blind read-back and subsequent source comparison found no substantive mismatch in the hypotheses, conclusion, curvature convention, or boundary cases. Formal equivalence lemmas connecting the coordinate model to conventional intrinsic formulations are not included as separate Lean results.
Successful declaration compilation does not prove the conjecture. Future contributions must preserve its assumptions and scope. A disproof must construct a counterexample to the fully quantified statement, and a reduction must explicitly identify every remaining open child theorem.
A data structure can hide each stored share individually while revealing their joint value through its visible layout. This distinction matters when a ledger publishes both a collection of shares and the markers identifying which cells were filled by genuine insertions. The GBFPlus protocol records cross-domain transfers in ledger attestations and uses a shared word containing an adjacent-domain identifier. Alexander Richard Towell's note identifies an allowed singleton snapshot in which its occupied cells reveal that identifier directly. The note also gives a sufficient occupied-count certificate for recovering an aggregate from a larger batch. These are the two results targeted here. Towell, v1.0.0
The observer in that setting is a reader of a permissioned ledger. Public visibility means visibility to such a reader, not unrestricted Internet access. The source protocol's construction, publication rules and adjacent-domain recovery checks provide the context; the contribution is limited to the particular metadata and view analyzed in the note. Qin et al., GBFPlus
A snapshot is an array of cells. Each cell is either empty or occupied by a -bit word. An occupied all-zero word is distinguishable from an empty cell. Public parameters include the share count , with , and the identifier width , with .
A row consists of a set of exactly distinct positions, a -bit prefix and an -bit adjacent-domain identifier . Its target is their concatenation . The array starts empty. A successful insertion reserves an empty selected cell, retains existing occupied words, fills the other empty selected cells with free words, and sets the reserved cell to the residual required by the target. If every selected cell is already occupied, the insertion fails and leaves the array unchanged. These operations follow the construction preceding the note's two propositions. Towell, Section 2
An honest history is a finite sequence of attempts satisfying those rules at every step. Its successful rows and count are derived from that sequence; an independently asserted integer is not substituted for . Let be the final occupied set, , and its occupied words. The public recovery statistic is
The statistic takes the snapshot and public widths. It does not take a secret prefix, query token, selected support or insertion history as an input.
The goal is Proposition 1, singleton disclosure: for every honest history with exactly one successful row,
It quantifies over every admitted position set, prefix, pivot and free-share realization. The Lean statement names the sole row by requiring that the derived successful-row list is its singleton list. Towell, Proposition 1
The supporting milestones are:
The positive-count condition is retained in this proposition. Its conclusion is an aggregate, not recovery of the individual identifiers or their multiset. Towell, Proposition 2 and its proof
The singleton identity identifies an adjacent-domain identifier from a complete share set exposed by occupancy. The larger-batch certificate establishes a narrower aggregate observation when the public occupied count matches the authentic successful count times the share count. It does not characterize every possible disclosure and does not estimate how often the certificate occurs. A deployment interpretation still needs the source's visibility and publication premises. Towell, Sections 1–2
Both propositions already have written proofs in the archived preprint. The accompanying source supplement provides finite computational checks. The remaining work here is to verify their universal statements from an explicit insertion model and preserve that construction-to-statement connection. The draft model has compiled concrete examples, including the published seven-cell array and an occupied zero word; the four theorem items remain open formal obligations. No new mathematical discovery or independent human proof review is claimed.
The risk lies in changing what constitutes a snapshot or an honest insertion. Treating a zero word as empty changes the occupancy count. Allowing later writes to replace occupied shares can invalidate earlier row equations. Supplying an unrelated count can make the certificate appear applicable when the claimed aggregate is wrong. Assuming all final row equations as part of the definition of honesty would also remove the construction obligation that the mission is intended to check.
The recovery function must remain independent of hidden row data even though the theorem's conclusion refers to the identifier that was inserted. The model must admit genuine executions, including singleton, disjoint and overlapping histories, and must distinguish a legitimate full-support failure from an arbitrary skipped insertion.
The shared namespace is GBFPlus.OccupancyDisclosure. A configuration stores positive prefix and suffix widths; their sum is . Words are pairs of finite coordinate vectors over . Componentwise addition is XOR, and concatenation places the prefix coordinates before the suffix coordinates. Cells use optional words, so occupancy is represented independently of payload value. Supports are finite sets of valid cell indices with exact cardinality ; successful occurrences retain their multiplicity in an ordered list.
Free words and valid pivots are explicit inputs. Universal quantification covers each realization; no probability distribution is needed for these identities. Honest histories are checked transition by transition from the empty state, without assuming the conclusions. The model uses Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474.
Ledger read access, authentic publication, genuine occupancy and timeout rules admitting singleton release are external premises of the source interpretation. The formalization does not model cryptographic position derivation, authentication, ledger execution, the separate data-identifier privacy game, publisher identification, full paths, scan costs or a complete repair. Contributions closing the stated obligations or extracting reusable finite-share and occupancy lemmas are welcome. Alexander Richard Towell supplies the source research and direction; substantial OpenAI Codex assistance in model construction, checks and proposal preparation is disclosed. Independent AI read-backs accompany the draft items and do not substitute for human review.
A quantum channel is conjugate degradable if the channel's environment can be simulated up to complex conjugation using the channel's output. For all such channels, the quantum capacity can be evaluated using a single-letter formula. In this article we introduce conjugate degradability and establish a number of its basic properties. We then use it to calculate the quantum capacity of N to N+1 and 1 to M universal quantum cloning machines as well as the quantum capacity of a channel that arises naturally when data is being transmitted to an accelerating receiver. All the channels considered turn out to have strictly positive quantum capacity, meaning they could be used as part of a communication system to send quantum states reliably.
This mission is the statement-level formalization of Conjugate Degradability and the Quantum Capacity of Cloning Channels (arXiv:0909.3297v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §II.C, Eq.(4): single-letter capacity of conjugate degradable channels (§II.C, Eq.(4): single-letter capacity of conjugate degradable channels, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum hypothesis testing is one of the most basic tasks in quantum information theory and has fundamental links with quantum communication and estimation theory. In this paper, we establish a formula that characterizes the decay rate of the minimal Type-II error probability in a quantum hypothesis test of two Gaussian states given a fixed constraint on the Type-I error probability. This formula is a direct function of the mean vectors and covariance matrices of the quantum Gaussian states in question. We give an application to quantum illumination, which is the task of determining whether there is a low-reflectivity object embedded in a target region with a bright thermal-noise bath. For the asymmetric-error setting, we find that a quantum illumination transmitter can achieve an error probability exponent stronger than a coherent-state transmitter of the same mean photon number, and furthermore, that it requires far fewer trials to do so. This occurs when the background thermal noise is either low or bright, which means that a quantum advantage is even easier to witness than in the symmetric-error setting because it occurs for a larger range of parameters. Going forward from here, we expect our formula to have applications in settings well beyond those considered in this paper, especially to quantum communication tasks involving quantum Gaussian channels.
This mission is the statement-level formalization of Gaussian hypothesis testing and quantum illumination (arXiv:1608.06991v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Compatible ordinary diagonalization and Gibbs-matrix equivalence (Appendix A, (A4)–(A13), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
10 results of the paper are not stated yet, because the library lacks an interface they need:
We consider quantum channels with two senders and one receiver. For an arbitrary such channel, we give multi-letter characterizations of two different two-dimensional capacity regions. The first region is comprised of the rates at which it is possible for one sender to send classical information, while the other sends quantum information. The second region consists of the rates at which each sender can send quantum information. For each region, we give an example of a channel for which the corresponding region has a single-letter description. One of our examples relies on a new result proved here, perhaps of independent interest, stating that the coherent information over any degradable channel is concave in the input density operator. We conclude with connections to other work and a discussion on generalizations where each user simultaneously sends classical and quantum information.
This mission is the statement-level formalization of Capacity Theorems for Quantum Multiple Access Channels: Classical-Quantum and Quantum-Quantum Capacity Regions (arXiv:quant-ph/0501045v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: regularized cq capacity (Theorem 1: regularized cq capacity, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
A monopolist selling to a large market of unit-demand consumers with a known demand curve cannot do better than posting a single price (Myerson 1981; Bulow and Roberts 1989). When the demand curve itself is uncertain, consumers' valuations are correlated through the aggregate state, and the picture changes. Crémer and McLean (1985, 1988) showed that with Bayesian incentive compatibility and only interim participation constraints, the seller can extract the entire surplus through side bets whose payments may far exceed a consumer's valuation. Such payments are not enforceable when a consumer can walk away from a deal that charges more than the good is worth to them.
Segal (2003) imposed ex post individual rationality together with ex post (dominant-strategy) incentive compatibility, and showed that as the number of buyers grows the optimal mechanism converges to state-by-state monopoly pricing: post, in each demand state, the monopoly price of that state's demand curve. Dominant-strategy incentive compatibility rules out most price discrimination. Peck and Rampal (2021) ask whether Segal's answer survives when incentive compatibility is weakened to the Bayesian (interim) notion, which leaves room for discrimination. Their Proposition 1 claims that it does, under four conditions on demand and beliefs. An earlier note by the same authors (Peck and Rampal 2019) shows that it fails when a single-crossing condition on beliefs (Condition 2 below) is dropped.
There are two demand states, low (state 1, probability ) and high (state 2, probability ). Valuations lie in with . In state the mass of consumers with valuation above is , so , and the demand density is . A consumer who knows their valuation updates their belief about the state in proportion to . The density ratio is . The firm has zero marginal cost and learns the state by aggregating reports.
A deterministic direct mechanism assigns to each state and report an allocation and a payment . It is anonymous: it depends only on the inferred state and the consumer's own report. It is ex post individually rational (EIR) if for all and both states, and Bayesian incentive compatible (BIC) if for all
The firm's profit is .
The conditions are: (1) each is with on ; (2) on ; (3) on ; and (4) either (i) on , or (ii) on . Under (4)(ii), every type assigns the low state the higher posterior probability. A monopoly price maximizes over . SBSMP sells in state to every at price .
Under Conditions 1, 2, 3 and 4(ii), SBSMP is BIC and EIR, and for every deterministic BIC and EIR mechanism ,
The goal does not claim uniqueness of the optimal mechanism, which the paper neither states precisely nor proves.
The milestones are the paper's own steps:
The goal is a BIC–DIC equivalence for an environment with correlated types and ex post participation. The paper describes it as the first such result: earlier equivalence results either assume independent types or rely on interim participation and large payments. When the conditions hold, a monopolist facing aggregate demand uncertainty gains nothing from the extra room for discrimination that Bayesian incentive compatibility allows, so Segal's ex post optimal mechanism remains optimal.
Formalizing the result adds three things. It checks a proof that is incomplete in print (see below). It separates the branch of the proposition that is true from the branch that is false. And it provides a reusable layer for mechanism design with a continuum of consumers and an aggregate state: demand curves and densities, deterministic anonymous mechanisms, EIR, posterior-weighted BIC, profit as an integral, and state-contingent posted prices. No part of the paper has been machine-checked before.
Status. The proposition is stated in the paper with Condition 4 as the disjunction of (i) and (ii). The Condition 4(i) branch is false, so this mission does not pose it. Take , , and , which satisfy Conditions 1–3 and 4(i). Consider the mechanism that
It is EIR, and BIC because every type is exactly indifferent between its two purchase options. Its profit is , which exceeds SBSMP's . The printed argument breaks where it treats a lower bound on the state-1 price of as a BIC constraint (§A.5.2(iv), Claim 3(iv)).
The Condition 4(ii) branch held in every exact computation on discretized instances: SBSMP was optimal among all BIC and EIR mechanisms in 34 of 34 random instances. Its printed proof has a gap. In Claim 5, the bound of (A.46) sets the state-1 price of the lowest type of equal to . Under 4(ii), BIC allows that price to be strictly larger, so is not an upper bound. A solver must supply a correct argument for excluding mechanisms in which only and are nonempty.
The class of competitors is large: , and can be arbitrary sets, and payments on arbitrary functions. The natural first step proves an interval structure and then optimizes over a few thresholds. That step does not go through in general. BIC alone does not force the interval property when all three sets are nonempty, and the paper instead compares against bounding mechanisms that need not be BIC. Statements that "the optimal mechanism" has a given set nonempty are fragile, because moving a single indifferent type changes them without changing profit. Excluding under 4(ii) is exactly the step where the printed bound fails. Reading SBSMP's optimality off the ex post (DIC) problem is also not enough: BIC permits strictly more mechanisms, and the 4(i) counterexample shows that the extra mechanisms can win.
Fin 2: index 0 is the paper's state 1 (low), index 1 is state 2 (high). The economy is a structure with vlo vhi α₁ : ℝ and D : Fin 2 → ℝ → ℝ. Valid records , and . These are added explicitly: EIR is unsatisfiable at negative types, and is the model's meaning of .Bool, which is "deterministic". EIR and BIC quantify over all . SBSMP charges to non-buyers.sSup, or by asserting only that SBSMP is feasible. Each of these would change the theorem.Warnings about health, financial or environmental risks are among the most common policy instruments: cigarette packs carry risk statements, doctors tell patients which risk group they belong to, and retirement planners report survival probabilities. Standard decision theory says that more accurate information can only help a decision maker. That conclusion fails when the decision maker has present bias, a stronger preference for immediate gratification than his own later selves would endorse (Phelps and Pollak, 1968; Laibson, 1997). For such a decision maker, learning that a harmful habit is only moderately risky can trap him into consuming even though, from an earlier perspective, he would rather abstain.
Mariotti, Schweizer, Szech and von Wangenheim ask how information about an individual risk should then be disclosed. They combine the quasi-hyperbolic model of self-control of Carrillo and Mariotti (2000) with the Bayesian-persuasion framework of Kamenica and Gentzkow (2011), and characterize the information structure that maximizes the decision maker's own long-run welfare, an information nudge. This mission formalizes that characterization.
A decision maker lives at dates 0, 1, 2, 3. At dates he chooses (consume or abstain). Consumption yields utility 1 immediately and, with probability , a cost two periods later. With a present-bias parameter and a discount factor , his date-0 and date-1 utilities are
with . The risk type is unknown; the prior is any probability distribution on , discrete, continuous or mixed, with distribution function . Two cutoffs organize the analysis:
Given a mean belief , both of the decision maker's selves consume if and abstain otherwise (Lemma 1); the date-0 self would prefer to abstain whenever .
A persuasion mechanism is a measurable , the probability that a type- decision maker receives the recommendation "consume". It is incentive-compatible if both recommendations are followed:
each constraint being void when its denominator vanishes. The designer maximizes the date-0 welfare, which up to a positive constant is . A cutoff mechanism recommends consuming with probability to the lowest types: with ,
The paper's Assumption 1 is and .
Under Assumption 1:
Optimality is over all incentive-compatible mechanisms. Uniqueness of is among .
The result shows that the welfare-maximizing disclosure policy for a present-biased agent is coarse and has a simple shape. It never reveals the type fully. It tells the lowest-risk types to consume and the highest-risk types to abstain, with randomization at most at one type. When harmful consumption cannot be avoided, the warning to abstain is pooled so that the abstaining group's mean risk is exactly , just alarming enough to be credible. The paper's comparative statics in the present bias, the alternative objectives of §5 and the traffic-light nudges of §6 are all built on this characterization.
The result is proved in the paper; to our knowledge it has not been machine-checked. A formalization adds a fully explicit treatment of priors with atoms, where the cutoff mechanism randomizes and the conventions , matter, and of the degenerate cases in which a recommendation is never sent. It also produces a reusable "bathtub" lemma (Lemma 2) and a monotonicity result for upper-tail conditional means for general distributions on the line, neither of which is in Mathlib.
The design problem is an infinite-dimensional linear program with a strict inequality constraint, so existence of an optimum is not automatic: a strict constraint can make the supremum unattained (the paper's §5 lobbyist problem has exactly this defect). The reduction to cutoff mechanisms requires the minimization in Lemma 2 for arbitrary distributions, including atoms at the quantile, and uniqueness up to null sets. The second half of Proposition 2 depends on how the upper-tail conditional mean behaves as a function of the mass of the tail: continuity across atoms, the limit at the top of the support, and monotonicity that becomes non-strict when there is an atom at . A naive argument that treats as continuous and invertible covers none of these cases.
The goal is not trivialized: optimality ranges over all incentive-compatible measurable mechanisms, not only cutoff mechanisms; (6) is not weakened to ; and is asserted to exist, not assumed.
A complete development needs the theory of the quantile function and of left limits of distribution functions for general measures on , the bathtub principle, and continuity of . These parts are reusable beyond this mission. Proofs of any milestone, and of auxiliary facts about distribution functions and quantiles, are welcome.
Minimizing a nonsmooth, nonconvex Lipschitz function is intractable in general, so nonsmooth optimization asks for a weaker certificate: a point near which a small convex combination of nearby subgradients exists. Such a vector is a Goldstein subgradient, a notion going back to Goldstein in the 1970s. Zhang, Lin, Jegelka, Sra and Jadbabaie (2020) gave the first dimension-free complexity analysis for finding a small Goldstein subgradient, using a directional subgradient oracle and a randomized line search. Concurrent work by Jordan, Lin and Zampetakis and by Kornowski and Shamir (2022) proved negative results for the general dimension-independent question with deterministic methods.
Kong and Lewis show that the obstruction disappears once the nonconvexity of the objective is measured. A simple deterministic bisection replaces the random line search, and the number of oracle calls is bounded explicitly in terms of a nonconvexity modulus . For difference-of-convex objectives (piecewise linear functions among them, which are not weakly convex) this gives an deterministic method, and in the weakly convex case (arXiv:2210.00652, abstract).
is a real inner product space with norm , possibly infinite-dimensional and not complete. is convex and is a real function on , bounded below.
Started at with and with any , if , Algorithm 4.1 stops at a point with , , within
oracle calls. The paper prints the first factor as . That expression is at a minimizer, and the bound fails there: a run started with a large subgradient needs at least one call. The page's own proof gives the corrected count.
The milestones follow the paper's proof:
The theorem gives a deterministic, dimension-independent oracle complexity for Goldstein stationarity, with the dependence on nonconvexity isolated in one scalar, . The paper bounds for weakly convex functions (Proposition 6.2), for difference-of-convex functions (Proposition 6.3, Corollaries 6.4–6.5) and for semi-linear functions, so explicit rates follow for each class. The univariate result, Corollary 5.6, is a complexity bound for a bisection line search in its own right, and Example 5.9 shows it is optimal among line searches.
The result is proved in the paper; no machine-checked version is known. The mission produces a formal model of the oracle, the Goldstein set, the concave deviation and the full run of Algorithm 4.1, with every oracle call counted. It also states the corrected constant. Formalizing the proof checks that the bound survives a stricter accounting than the paper's, which counts only line-search evaluations, not trial points or re-initializations.
Two counting arguments are glued together, and each has a gap that the prose skips.
First, the bisection bound needs the convex perturbation of the concave deviation to control the bisection through Theorem 5.2. The induction there restarts the method on a half-interval, and its sub-run re-evaluates an endpoint that the outer run evaluated already. Aligning the counts takes care.
Second, the global bound multiplies the number of phases by the number of line searches per phase and the cost per line search. The phases are separated by reductions, and a line search may stop at its first evaluation. The algorithm's iterates must also be shown to stay where the hypotheses apply: in , below , with segments of length inside .
The tempting shortcut is to take the printed bound and the paper's count of line-search evaluations at face value. Both are off at the edges.
[NormedAddCommGroup X] [InnerProductSpace ℝ X], with no completeness and no finite dimension.X → ℝ constrained only on . The oracle identity is required only at points of , along directions that stay in for small steps.sInf (f '' C) with BddBelow (f '' C).ℝ≥0∞. "Finite " is ≠ ⊤, and the bound uses its real value.HasDerivWithinAt on closed intervals. Their finiteness is an added hypothesis.Nat.floor/Nat.ceil.A trivializing formalization is ruled out: the goal is a bound fixed before the run, on the actual run that bisects with the rule and updates by shortest vectors. Mere existence of a point with a small Goldstein subgradient, or termination without a bound, are weaker statements and are not the goal.
Infrastructure needed: one-sided derivatives of convex functions on intervals, monotonicity of their difference quotients, and a counting argument over a state machine. Proofs of the univariate milestones (Lemma 5.1, Theorem 5.2, Corollary 5.6) are reusable for other line-search analyses. Contributions of any milestone are welcome. Not formalized here: Propositions 2.4, 3.2, 5.5, 6.2, 6.3, Theorem 4.3 (termination under semismoothness), Theorem 5.7 and the appendix on distributional second derivatives.
The Hahn–Banach theorem extends every bounded linear functional on a linear manifold of a normed space to the whole space, with the same norm. For bounded linear operators into an arbitrary Banach space, and for bounded bilinear maps, nothing of the kind holds in general: there is no Hahn–Banach theorem for bilinear functionals. Extension problems for bilinear and multilinear forms have been studied under many restrictions on the spaces involved — forms on , the case , characterizations of through extendible forms, and conditions linked to integral representations on injective tensor products (see the survey in §3 of the paper).
C. S. Kubrusly (arXiv:2110.03102, Mathematica Slovaca 72 (2022)) puts the condition on the domains only. For linear manifolds and of Banach spaces, every bounded bilinear map on with values in an arbitrary Banach space extends to exactly when the closures of and are complemented. This generalizes an earlier sufficient condition for bilinear forms (Hayden, 1967, restated as Theorem 5.1 of the paper) in three directions: it is an equivalence, it covers vector-valued maps, and the norm-one condition on the projections is needed only for norm preservation, not for the existence of an extension.
Let be or . A linear manifold of a normed space is a linear subspace, not necessarily closed; a subspace is a closed linear manifold; is the closure of .
A bounded bilinear map is a map linear in each variable with
The space of these is ; is the space of bounded linear operators with the operator norm. A map extends , written , if the two agree on .
A subspace is complemented if it has a subspace (a closed linear manifold) as an algebraic complement: and . A projection with range is an operator with and .
Let be linear manifolds of Banach spaces .
(a) For :
(b) If and for projections with , then every has an extension with .
The theorem turns a question about all bilinear maps and all Banach targets into a geometric property of two subspaces. Consequences in the paper include an unconditional extension theorem for bilinear maps on products of arbitrary linear manifolds of Hilbert spaces (Corollary 5.3, where every closed subspace is complemented by its orthogonal complement), and, through the identification , extension results for bounded operators on projective tensor products (§6). The norm statement (b) isolates exactly where norm-one projections enter; the paper shows by a two-dimensional example that its converse fails.
The result is proved in the paper; to our knowledge it has not been machine-checked. Mathlib contains the linear theory used along the way (closed complemented submodules, extension of uniformly continuous linear maps from dense subspaces, the Hahn–Banach theorem), but not this bilinear extension theorem or its characterization of complemented closures. The mission produces a formal statement and proof of the equivalence, the norm-preservation clause, and the classical linear-extension characterization of complemented subspaces used in the necessity direction.
Two steps resist the obvious arguments. First, a bounded bilinear map is not uniformly continuous on , so extension by continuity to does not apply directly, and the norm identity on the closures has to be obtained some other way. Second, the necessity direction needs the classical fact that a closed subspace of a Banach space is complemented when every bounded operator from it into every Banach space extends; the paper cites this (Megginson, Theorem 3.2.17) without proof, so a formalization has to supply it. The naive reading "complemented means some algebraic complement exists" is not the notion: every subspace has an algebraic complement, and the content lies in the complement being closed.
The field is any RCLike 𝕜 ( or ). Linear manifolds are Submodule 𝕜 X, not assumed closed; the closure is M.topologicalClosure. Bounded bilinear maps are curried continuous linear maps M →L[𝕜] N →L[𝕜] Z, and is Mathlib's operator norm; Proposition 4.2 (a milestone) is what makes this encoding agree with the paper's bilinear norm. Complemented means closed with a closed algebraic complement (IsClosed, IsCompl); a bare algebraic complement would make the notion trivial and is ruled out. A projection onto is a continuous linear operator mapping into and fixing pointwise. Extensions are stated pointwise on .
Conventions committed to, each disclosed in the item statements:
Out of scope: Corollary 5.3 (Hilbert spaces), Remark 5.4 and §6 on projective tensor products. Reusable beyond this mission: the linear extension characterization of complemented subspaces (milestone 4) and the norm-preserving extension of bilinear maps to closures (milestone 5). Proofs of any milestone are welcome independently.
Envy-free cake cutting asks for a division of a divisible resource, modelled as the interval , among agents with individual preferences so that no agent prefers another agent's share to its own. For a single cake and contiguous pieces, the existence of envy-free divisions goes back to Stromquist (1980) and to Su's Sperner-lemma proof (1999).
Multi-layered cake cutting, introduced by Hosseini, Igarashi and Searns (2020), models resources made of several parallel copies of a time line: meeting rooms booked over a day, or a facility with several machines shared in time slots. A bundle receives a piece of every layer, and it is feasible only if its pieces in different layers do not overlap in time, since one group cannot use two rooms at once. Igarashi and Meunier (arXiv:2106.02262v4, Mathematics of Operations Research, 2025) prove that envy-free feasible divisions exist when the number of bundles is a prime power, and they divide the agents into groups of almost equal size, each group sharing one bundle.
Timeline:
A piece is a finite union of pairwise disjoint closed subintervals of . An -layered cake has layers , each a copy of . A layered piece has one piece per layer; it is non-overlapping if is empty or finite whenever . A multi-division is a -tuple of layered pieces covering every layer, with entries meeting in at most finitely many points of each layer. It is contiguous if each is an interval, feasible if each is non-overlapping, and obtained with long knives if there are positions , the same in every layer, such that every is one of the intervals .
Each agent has a choice function that returns, for a multi-division , the set of preferred layered pieces. It is invariant under permuting the entries of , and it prefers at least one entry of . Layered pieces are compared by the pseudo-metric , where is Lebesgue measure. An agent has closed preferences if, whenever multi-divisions converge entrywise to a multi-division and for all , also . One agent is the birthday agent : the division is computed without its preferences, and it may pick any bundle afterwards.
Let with a prime power, and let all agents have closed preferences. Then there is a feasible, contiguous multi-division into layered pieces, obtained with long knives, such that for every there is an assignment with
The multi-division is fixed before the birthday agent chooses. The group sizes count the birthday agent.
For and , Theorem 1 is the Avvakumov–Karasev theorem: an envy-free division exists even when agents may prefer empty pieces, provided the number of agents is a prime power. For general it gives envy-free divisions among groups, and for a feasible schedule of parallel resources. The paper derives from it the existence of proportional feasible multi-divisions for every with (Theorem 5).
None of these results has been machine-checked. A formalization would add, beyond Theorem 1 itself, a Lean model of multi-layered cake cutting with choice-function preferences, the chessboard complex with its free group action, and an integral rounding lemma for bipartite assignments with a reserved slot. No statement of Volovikov's theorem or of its consequences exists on the platform yet; Lemma 1 would be the first.
The classical route encodes divisions by points of a simplex and applies Sperner's lemma. In the layered setting the induced coloring need not satisfy Sperner's boundary condition, even for monotone preferences (p. 6), and without hungriness it fails already for one layer. The proof therefore relies on Volovikov's Borsuk–Ulam-type theorem for -actions and on the -connectivity of the chessboard complex ; Mathlib has neither. The prime-power hypothesis is essential: for one layer and not a prime power, Avvakumov and Karasev show that envy-free divisions need not exist without hungriness, and Lemma 1 itself fails already for . Passing from triangulations to the limit needs closedness of preferences and the continuity of the encoding (Lemma 3), whose proof must handle several simplices of the configuration space accumulating at the same limit point.
Layered pieces are Fin m → Set ℝ, multi-divisions Fin q → Fin m → Set ℝ, choice functions maps from multi-divisions to sets of layered pieces. "Disjoint interiors" and "non-overlapping" are encoded as finiteness of intersections, which is equivalent for finite unions of closed intervals. The pseudo-metric sums (volume (symmDiff …)).toReal over the layers. The birthday agent is an arbitrary b : Fin n; "prime power" is IsPrimePow q; group sizes are cardinalities of fibres over all of Fin n.
Three readings are disclosed:
The chessboard complex is realized concretely in , with columns indexed by , so the bijection of the page is the identity.
Trivializing formalizations are ruled out. Without the covering clause the empty multi-division would satisfy everything. An agent preferring nothing would make the goal false. Choosing the multi-division after the birthday agent's choice () is a weaker theorem. The goal states .
A complete development needs:
These pieces, and the cake model, are reusable beyond this mission. Contributions are welcome on any milestone.
Interior-point methods for convex programming, introduced in their modern form by Nesterov and Nemirovski, run Newton's method on a barrier function of the feasible set. Their complexity analysis rests on a single analytic property of the barrier, self-concordance: the third derivative is controlled by the second, . This inequality is invariant under affine changes of coordinates, and it is tied to the affine structure of the space.
Hildebrand (arXiv:1909.01883v2) observes that the feasible sets of conic programs carry more structure than that. A feasible set of a conic program is a slice of a cone, and the barrier used on it is the restriction of a logarithmically homogeneous barrier of the cone. Restricted barriers of this kind satisfy a sharper, projectively invariant inequality, which the paper calls projective self-concordance. Estimates used in the analysis of interior-point methods (Dikin ellipsoids, outer approximations of the feasible set, short-step path-following parameters) improve when this extra information is used; Sections 3–8 of the paper develop those consequences.
All of those developments rest on one characterization, Theorem 1.5: a function on a convex set is projectively self-concordant with parameter exactly when its logarithmically homogeneous extension to the cone over the set is self-concordant, with the sharp relation . This mission formalizes that theorem and the steps of its proof.
Let be an open convex set and a function. Write , and for the first three derivatives of at in direction .
In the Lean development these are ProjCond1, ProjCond3, AffCond1, AffCond3, conicExt, homExt and pmu in the namespace ProjSelfConcordant.ConicExt, with derivatives dk k g x h.
With and ,
Both directions are required, and each side is the conjunction of the two conditions, as on the page.
Theorem 1.5 identifies projective self-concordance with a familiar object, so every later result of the paper can be read either on the set or on the cone. Corollary 1.6 derives from it the passage between projectively and affinely self-concordant barriers on the same set. The improved inner and outer approximations of Section 3 and the duality theory of Section 5 are stated for projectively self-concordant functions, and Theorem 1.5 is what makes them applicable to the restrictions of standard conic barriers (log-det, logarithmic barriers of the orthant, the second-order cone barrier). The constant is sharp: for slightly above the sextic takes negative values.
The result is proved in the paper. As far as is known, neither it nor the general theory of projective self-concordance has a machine-checked proof; the platform's self-concordance vocabulary covers the affine notion only. A formal proof contributes reusable calculus for logarithmically homogeneous functions on cones (the derivatives of , and the homogeneity of and ) and a certified treatment of the sextic inequality that fixes the sharp constant.
The argument has two different parts. The first is multivariable calculus: computing the second and third Fréchet derivatives of at points of the slice , along directions with a component in , and transferring them along rays by homogeneity. In Lean this means iterated derivatives of compositions with the nonlinear map , restricted to an open set on which is only , and with derivatives taken in a product space.
The second is real algebra. The affine condition (3) along a two-dimensional slice is a degree-six polynomial inequality in ; after normalization it becomes nonnegativity of for all , and the content of the theorem is that the set of for which this holds is exactly . Checking finitely many values of gives only necessity; sufficiency needs a certificate of nonnegativity at the endpoints and an argument for the interval in between. Direct expansion produces sextics whose nonnegativity is not visible term by term.
The equivalence is between conjunctions of conditions (1) and (3). Splitting it into one equivalence for each condition is not what the page claims: the conditions (3) are only meaningful where the forms of condition (1) are nonnegative.
EuclideanSpace ℝ (Fin n) and is ℝ × EuclideanSpace ℝ (Fin n), first coordinate . The product carries the sup norm; Fréchet derivatives do not depend on the choice of norm in finite dimensions.ContDiffOn ℝ 3 f D.iteratedFDeriv ℝ k g x (fun _ => h). Positive definiteness is strict positivity of the quadratic form on nonzero vectors. Tangent vectors range over the whole ambient space.Real.rpow. Condition (3) appears only in conjunction with condition (1), under which its bases are nonnegative.Contributions are welcome on either layer, and alternative proofs of the sextic bounds (for example sum-of-squares certificates) are as useful as transcriptions of the paper's argument.
Dynamic traffic assignment predicts how travellers choose routes and departure times when travel times depend on the traffic itself. Its central solution concept, the dynamic user equilibrium, asks that no particle of flow can lower its cost by switching to another route or departure time. Existence of such equilibria in continuous time is classical: Friesz et al. (Oper. Res. 1993) gave the variational-inequality formulation, and Zhu and Marcotte (Transp. Sci. 2000) proved existence from Lions' theorem on variational inequalities.
Real networks also carry side constraints: hard limits on how much traffic an edge may hold (road volume caps, parking, the battery and charging limits of electric vehicles). In static models, side-constrained equilibria go back to Larsson and Patriksson (Transp. Res. B 1999) and to Marcotte, Nguyen and Schoeb (Oper. Res. 2004). For the dynamic model, Zhong et al. (Transp. Res. B 2011) claimed existence through a variational inequality over the constrained flow set. Graf and Harks (arXiv:2211.03194, Operations Research 2024) show that this claim fails: with volume constraints the feasible set need not be convex. They replace the variational inequality by a behavioural definition of equilibrium and prove the first existence theorem for the non-convex volume-constrained case. That theorem is the goal of this mission.
There are finitely many commodities and finitely many walks ; each walk belongs to one commodity, denotes the walks of commodity , and a walk is the list of its edges . Time runs over a horizon . A walk inflow gives the rate at which flow enters walk at time . With departure time choice, the feasible inflows are
where is the volume of commodity and bounds the inflow rate of walk .
The traffic model supplies four functions of the inflow: the effective walk delay , the cost of entering walk at time ; the arrival times at which a particle entering at time enters the -th edge of ; the edge loads ; and the capacities . The capacity-feasible inflows are .
A -deviation from walk removes a small inflow from and adds it to , delayed by : . A correspondence lists the admissible deviations, and is an admissible alternative to at time , written , if arbitrarily small admissible deviations concentrated arbitrarily close to exist. A flow is a side-constrained dynamic equilibrium (SCDE) if
Two choices of matter here. In a strong dynamic Larsson–Patriksson equilibrium (strong LPDE) a deviation onto is admissible if every edge of has strict slack, , at the time the deviating particle would enter it. In a strong dynamic Marcotte–Nguyen–Schoeb equilibrium (strong MNSDE) slack is not required on a common prefix of and when .
Under the paper's assumptions (A2), (A3), (A5), (A9)–(A19) and continuity of the capacities (A22),
The assumptions are qualitative (continuity, uniform convergence along weakly convergent inflows, causation, an outside option, bounded delays on ); no constants are fixed.
The result. Theorem 7.6 is an existence theorem for a model whose feasible set is not convex, where the standard route through variational inequalities is closed: the paper's counterexample (§4) shows that the variational-inequality approach of Zhong et al. does not give existence. The paper argues that the Vickrey point-queue model and the linear edge-delay model satisfy its assumptions (Lemma 7.10, whose proof defers to earlier work, and Corollary 7.11), and the equilibrium notions it produces (strong LPDE, strong MNSDE) are the dynamic counterparts of the established static side-constrained equilibria.
Formalizing it. The result is proved in the paper but nowhere formalized. A formalization adds a reusable layer for continuous-time traffic equilibria: walk inflows, weak convergence in , deviation operators, admissible deviations and SCDE, and Lions' existence theorem in , which does not exist on the platform or in Mathlib. A related item on the platform, FrieszDUE.PIE.theorem_2_pie_vip, characterizes route-departure equilibria by a variational inequality in a model without rate bounds; it is not the statement of Theorem 3.3 here.
The obvious approach is to solve the variational inequality over the constrained set . It fails twice: need not be convex, so Lions' theorem does not apply, and even a solution need not be an SCDE because small deviations from a feasible flow can leave . The paper therefore penalizes capacity violations in the cost, , and passes to the limit . The hard steps are the limit arguments: showing that the weak limit of penalized equilibria is feasible, and that an improving admissible deviation for the limit would produce an improving deviation for some penalized equilibrium. Both combine weak convergence of inflows with uniform convergence of loads, arrival times and delays; the second also needs strict slack to survive the passage to the limit.
Inflows, deviations and test functions are real functions on (representatives), not classes. The bounds defining hold almost everywhere, and inflows vanish outside ; the support and size conditions on hold pointwise on the chosen representative, as the paper prescribes on p. 33. Weak convergence is convergence of for every with square-integrable components. The deviation (17) is read additively, also when . Arrival times use a 0-based node index: Lean's tau h p j t is the paper's . Delays are real-valued. The condition , which §7 adds implicitly to every deviation set, is written out.
Every SCDE statement includes , and the admissible alternatives are built from genuine deviations: a measurable with , supported in , with . A formalization in which is always empty, or in which the SCDE predicate omits feasibility, would make the goal trivial and is ruled out; a sorry-free sanity file exhibits a feasible flow with a non-empty that is not an SCDE, and a model satisfying every hypothesis of the goal.
Three choices differ from the printed theorem. (A22) continuity of every capacity on is added: Theorem 7.6 assumes only that capacities are non-negative and non-decreasing, but two steps of its proof (that satisfies (A4), and the transfer of strict slack in Claim 7) need continuity, and the paper itself assumes (A22) in Theorem 7.9. (A17) is posed for all rather than , because the proof applies it to infeasible flows. Measurability of the arrival times is a standing convention. Only the model with departure time choice is posed; the half of Theorem 7.6 with fixed inflow rates is not.
A complete development needs: weak sequential compactness of in ; Lions' theorem in (Brouwer is available as AGT.brouwer_fixed_point); the bathtub argument behind Theorem 3.3; and the limit arguments of Claims 5–7. Lions' theorem and the weak-compactness facts are reusable beyond this mission. Proofs of individual milestones, in any order, are welcome.
A portfolio loss often depends on several risk factors whose individual distributions can be estimated well but whose joint distribution cannot. Regulators and risk managers then ask for the worst-case risk: the largest value a risk measure can take over all joint laws compatible with the known marginals. For Value-at-Risk and Expected Shortfall of sums this question has a long literature on risk aggregation (Embrechts, Puccetti, Rüschendorf, Wang and others). Ghossoub, Hall and Saunders (arXiv:2010.14673v1, published in Mathematics of Operations Research, 2023) treat a general loss of two Polish-space-valued risk factors and the whole class of spectral risk measures, which contains Expected Shortfall and, for constant weight, the expectation. Their main result is a duality theorem in the style of Kantorovich duality for optimal transport.
Let and be Polish spaces with their Borel -algebras, and probability measures on them, and the set of couplings: probability measures on with marginals and . A loss is a function .
For a coupling , the generalized inverse of is for . A spectral function is a bounded, increasing, right-continuous with , and the spectral risk measure is
Expected Shortfall is the case . Two measures on carry : , with distribution function (so may be positive), and , the probability measure with .
The Maximum Spectral Measure is the primal value
For a threshold function define the cost , and let be the pairs with for -a.e. and -a.e. . The dual value is
The assumptions are: (A.1) is upper semicontinuous; (A.2) with lower semicontinuous integrable ; (A.3) with upper semicontinuous integrable , both bounds for -a.e. and -a.e. ; (A.4) is bounded and right-continuous.
The goal asserts only the equality of values. It does not assert attainment in the primal or the dual; the paper does not claim dual attainment (Remark 3).
The theorem gives a computable upper bound mechanism: every dual feasible triple certifies an upper bound on the worst-case spectral risk, and the bounds are tight. For it is Kantorovich duality for the cost ; for Expected Shortfall the infimum over collapses to one real threshold, which the paper exploits in §5 for stability and asymptotic results. The ingredients (the ES-mixture representation of spectral risk measures, the Rockafellar–Uryasev formula, interchange of infimum and integral for normal integrands) are standard tools of risk measure theory that are reusable well beyond this paper.
The result is proved in the paper, not formalized anywhere known. A complete development adds a machine-checked version of Kantorovich duality for upper semicontinuous costs with integrable bounds and almost-everywhere constraints, which the platform currently has only for continuous nonnegative costs with bounded continuous potentials (MongeKantorovichYao.monge_kantorovich_duality). Related platform work includes the Open goal RiskFunctionals.Distortion.choquet_representation, a lower-tail analogue of milestone 3 for distortion acceptability functionals, and RUCVaR.MinFormula.theorem_10, the Rockafellar–Uryasev formula on a finite-dimensional carrier.
The informal derivation on p. 7 exchanges a supremum over couplings with an infimum over threshold functions, an infimum with an integral, and two integrals, and then applies Kantorovich duality to a cost that depends on . Each exchange needs a reason. The supremum–infimum exchange needs a minimax theorem over the weakly compact set against an infinite-dimensional convex set of 's, with upper semicontinuity in that holds only for , not on the larger natural domain . The infimum–integral exchange must cope with the atom of at , where the pointwise infimum need not be attained, and with the factor , which is unbounded near . Applying Kantorovich duality to needs the cost to be upper semicontinuous with integrable bounds, which is Lemma 1. Lemma 3 of the paper () is false in general and is not part of the mission; Lemma 4 holds without it.
The development is in the namespace MaxSpectralRisk.Duality over Mathlib. Couplings are the published MongeKantorovichYao.transferencePlans μ ν. A spectral function is a StieltjesFunction ℝ that vanishes on and integrates to over ; this builds in A.4, since monotonicity bounds it on and values on are never used. is its Stieltjes measure restricted to and has density against ; milestone 1 checks the paper's distribution-function description. , and the auxiliary , take values in EReal; and are when their integrand is not integrable, matching the paper's . Integrals over against are Lebesgue interval integrals. Weak convergence of couplings is convergence in Mathlib's ProbabilityMeasure topology. "For -a.e. and -a.e. " in A.2, A.3 and means "off with ".
That reading is essential: a -almost-everywhere dual constraint can be violated on the support of a coupling (the diagonal of under Lebesgue marginals), which breaks weak duality. Equally, a dual over constant only, over bounded only, or values computed as real sSup/sInf (which return on unbounded sets) would not be the paper's problem.
Contributions are welcome at every level: the Stieltjes and integration-by-parts facts behind milestones 1 and 3, the convex analysis of milestone 2 and Lemma 2, a general Kantorovich duality for semicontinuous costs (reusable for any optimal transport mission), and the minimax theorem behind Proposition 3.
Many economic and managerial decisions are choices of a mixing weight: how much effort to put on one sale rather than another, how much wealth to put in a risky asset, how to split a portfolio between two contracts. A natural comparative-statics requirement is that if one of the two options is improved in every state of the world, the decision maker should put at least as much weight on it. Ghili and Klibanoff (Management Science 67(12), 2021) call this property monotonicity in optimal mixtures and ask which models of decision making under ambiguity satisfy it.
Subjective expected utility satisfies it. The models used to describe ambiguity-averse behavior, such as the maxmin expected utility model of Gilboa and Schmeidler (1989), Choquet expected utility of Schmeidler (1989) and α-MEU of Ghirardato, Maccheroni and Marinacci (2004), are widely applied in contracting, finance and operations. Whether they predict that "surely better" options receive more weight is a basic question for any such application. The paper's first main finding is that, for the c-linearly biseparable class of Ghirardato and Marinacci (2001), which contains all three, the answer is negative as soon as the decision maker is ambiguity averse toward a single event.
The setting is an Anscombe–Aumann framework. is a finite set of states; an event is a subset and is its complement. is the set of simple lotteries over prizes. An act is a map , and acts are mixed statewise: . For lotteries , the binary act gives on and off .
All preferences are in the MBA class of Cerreia-Vioglio et al. (2011): an act is evaluated by , where is a nonconstant affine utility and is normalized, monotone and sup-norm continuous. Under this representation an act may be identified with its utility profile , where is a convex subset of with at least two points.
A capacity is a set function with , and whenever . A preference is c-linearly biseparable if there is a capacity such that
represents the preference over all binary acts with , for all events . The number classifies the attitude toward bets on : below is ambiguity aversion, equal to is neutrality, above is ambiguity loving.
For acts , the set of optimal mixtures is the set of all such that is optimal in . For , in the set order if , imply and . Monotonicity in optimal mixtures restricted to a set of acts requires for all with in every state .
Fix any event and a c-linearly biseparable preference with capacity .
The theorem gives a sharp dividing line inside a large and heavily used family of ambiguity models. Ambiguity aversion toward even one event is incompatible with monotonicity in optimal mixtures for MEU, Choquet EU and α-MEU. The immediate corollary in the paper (Proposition 1) is that an MEU preference satisfies the property on bets on exactly when all its priors agree on the probability of . In applications such as the paper's sales-agent model, this means that improving the compensation for one task in every state can lead an ambiguity-averse agent to reduce effort on it. The result also separates these models from the smooth ambiguity model, for which the paper proves a compatibility result (Theorems 3–4).
Theorem 2 is proved in the paper; it has not been machine-checked. The mission produces a Lean development of the Anscombe–Aumann setting in utility space, capacities, MBA and c-linearly biseparable preferences, optimal-mixture sets and the set order, together with a checked proof of both directions. This layer is reusable for Proposition 1 and for other results on comparative statics under ambiguity.
The obvious route through comparative statics does not apply. The Milgrom–Shannon monotonicity theorem needs a single-crossing or supermodularity property of the objective in , and the c-linearly biseparable functional restricted to a segment is only piecewise linear, with a kink where utilities on and coincide. Exhibiting a violation requires solving the maximization of a minimum of two affine functions on exactly, and constructing acts whose slope falls strictly inside a window determined by and , inside an arbitrary convex utility range.
The converse is not the mirror image of the first direction: the functional is then convex along segments, optimal sets can be whole intervals, and indifferences among , and are where the argument is delicate. Remark 2 of the paper gives a capacity with , for which the converse fails, so the condition cannot be dropped.
v : S → ℝ with values in a set U : Set ℝ. U is assumed convex and to contain two distinct points, which is exactly the range of a nonconstant affine utility on simple lotteries. Mixtures are α • f + (1 - α) • g, and " for all " is ∀ s, f s ≤ f' s.S is a Fintype. An empty S makes the capacity conditions unsatisfiable, as on the page.U^S. On a finite S the product topology is the sup-norm topology.V and of W over binary profiles of all events, together with a capacity. The Ghirardato–Marinacci axioms are not encoded.Supermodularity.Lattices.InducedSetOrder on ℝ.Contributions welcome: proofs of the milestones, and reusable lemmas on maximizers of minima and maxima of affine functions on intervals.
Product development is often organized as a search over prototypes: several candidate designs exist, each must be built or tested at a cost before its quality is known, and the firm wants to end up launching the best one without spending too much on testing. When each test reveals the true quality of a prototype, this is Pandora's box problem, solved by Weitzman (Weitzman 1979): attach to every box an index, its reservation price, open boxes in decreasing order of the index, and stop as soon as the best value found exceeds every remaining index.
In practice, tests are rarely perfect. Simulations, virtual prototypes, consumer panels and outsourced test platforms return a noisy measurement of a prototype's value, not the value itself. Bhaskaran and Erat (Bhaskaran and Erat 2025) ask what the optimal sequential testing policy is when each evaluation only yields a signal correlated with the true value. Extensions of Weitzman's model are known to be fragile: with learning across alternatives (Erat and Kavadias 2008) or with the option to select an alternative without inspecting it (Doval 2018), index policies stop being optimal. Theorem 1 of the paper shows that measurement noise is not such a perturbation: an index policy remains optimal once the indices are computed from the right distributions.
There are prototypes, . Prototype has a true value and, when evaluated, yields a measurement . The pair has a joint density on with , and different prototypes are independent. Evaluating prototype costs , paid once.
The firm sees only measurements. It evaluates prototypes one at a time, in any order and adaptively; it may stop at any time, including before any evaluation. On stopping it launches one of the evaluated prototypes, receiving its true value, or launches nothing and receives the outside option . Its net payoff is the value received minus the evaluation costs paid, and a policy is judged by its expected net payoff.
The paper's objects are:
the expected true value of prototype given the measurement ;
In the Lean development these are Model, Policy, run, netPayoff, Admissible, value, Q, g, V, B and fidelityPolicy in the namespace NoisyPrototyping.ReservationPolicy.
The fidelity-adjusted reservation price policy evaluates the prototypes in the order and, after the -th evaluation (), stops and accepts if (always at ), and otherwise evaluates prototype . The goal states that is admissible and that, for every admissible adaptive policy ,
Theorem 1 says that the qualitative structure of Weitzman's solution survives imperfect evaluation. The evaluation order is fixed in advance, by indices that depend only on each prototype's cost and on the joint law of its value and measurement; the stopping rule is a threshold rule applied to a monotone transform of the measurements. Everything the paper does afterwards rests on it: the Gaussian closed form of Theorem 2, the comparative statics of Propositions 1–3 in the fidelity of the test, the choice of fidelity in Propositions 4–6, and the pricing of an outside test platform in Propositions 7–8.
The result is proved on paper by reduction to Weitzman's theorem. Weitzman's theorem itself is neither proved nor posed on the platform (searched October 2026), so the formalization produces two things: a formal proof of optimality of Pandora's rule, in the version with recall, any order, free stopping and an outside option; and a formal account of the reduction from noisy to perfect evaluation, which the paper presents as two short claims.
The natural first idea is to declare that "the firm only cares about " and apply Weitzman directly. Two steps of that argument need work. First, the policies of the noisy problem see the measurements , which may carry more information than when is not injective, so the class of policies in is richer than in ; showing that this extra information is useless requires the independence of prototypes and a conditioning argument for adaptive, history-dependent stopping. Second, the replacement of by in the payoff must be justified for an adaptive launching decision, not for a fixed prototype. Weitzman's theorem itself is not in Mathlib, and its optimality claim ranges over every adaptive policy, so it cannot be checked by comparing finitely many candidate rules.
Prototypes are indexed by Fin N from ; the paper's reordering is a bijection σ : Fin N ≃ Fin N along which the prices are non-increasing (ties in any order), and the paper's is R (σ n). The law of is a probability measure on ; the outcome of all prototypes has the product law, which encodes independence. The goal and Claims 1–2 assume this law has a measurable density . A history records evaluated prototypes and their measurements only; a policy maps histories to evaluate , launch or stop with nothing; each prototype is evaluated at most once, and illegal decisions end the run with nothing. A policy is admissible when the evaluation order and the final decision are measurable events and the net payoff is integrable; values are Bochner integrals of the net payoff.
Disclosed readings: independence across prototypes; ; ; formula (1) with in the denominator (the page prints , which would not give a conditional expectation); as the law of (formula (2) as printed lacks a Jacobian factor). The proof's simplifying assumption that is increasing onto is not made.
The statement admits trivializing encodings, and they are excluded: policies cannot see true values (that would make the problem full-information, where is not optimal); is the explicit formula (1), not a conditional expectation by definition; enters as the hypothesis that it is the least root, never through a choice function; and competitors are compared only when admissible, while the admissibility of is part of the conclusion.
A complete development needs: the conditional expectation of a coordinate under a joint density; conditioning arguments for adaptive policies on a product space; and Weitzman's theorem. The last two are reusable beyond this mission, for any search or bandit model with independent alternatives. Proofs of the milestones in any order are welcome, and a proof of the Weitzman milestone is the most reusable contribution.
Products with positive network effects (messaging apps, online games, social platforms) are known to support higher profits: a buyer's utility grows with the number of other buyers, and a seller can monetize that complementarity (Katz and Shapiro 1986; Candogan, Bimpikis and Ozdaglar 2012). Ajorlou and Jadbabaie ask whether a seller of a product without such an effect can create one artificially, by announcing a sales-based rebate: every buyer pays the market price and later receives a reward that depends on the realized sales volume (arXiv:1902.09646v4, Management Science, 2023).
Because consumers are uncertain about a common quality component and about each other's valuations, the purchase decision becomes a global game with correlated private valuations, in the sense of Carlsson and van Damme (1993) and Morris and Shin (1998). A natural first guess is that a rebate increasing in sales volume, which imitates a positive network effect, should help the seller. The paper's Theorem 2 says the opposite: when the price is already optimal, no increasing sales-based reward program is profitable. This mission formalizes that result and the identities on which it rests.
A firm sells one product at a market price to a unit mass of consumers. Consumer values the product at , where the common quality has the Gaussian prior and the taste is idiosyncratic. Write
A consumer who observes holds the posterior . Valuations are ex ante , with density , where and are the standard normal density and distribution function.
If consumers buy exactly when (a threshold strategy with cutoff ), the sales volume at quality is . A reward program is a function of the sales volume; at cutoff it induces the reward as a function of the quality. The cutoff is an equilibrium for when
The firm's expected profit is
With no reward the cutoff is and the profit is . Assumption 1 says that maximizes the no-reward profit . A reward program is profitable at an equilibrium cutoff if (2) strictly exceeds the no-reward profit at .
Under Assumption 1, for every weakly increasing reward program and every equilibrium cutoff of (1) for ,
The result. Theorem 2 separates two effects that are easy to conflate: an inherent network effect raises profit, but an induced one, paid for through a rebate increasing in sales, lowers the expected net price exactly at high valuations and so cannot beat the optimal plain price. It is the negative half of the paper's design question; the positive half (optimal programs are decreasing in sales volume, "full refund or nothing", §III–§IV) is built on the same representation (9) of the profit by valuations, which is a milestone here. Lemma 1 is the paper's general criterion for when any reward program beats the equivalent plain price, and applies beyond monotone programs.
Formalizing it. The results are proved in the paper (body p. 16, appendix p. 29); no machine-checked version is known. The formal work consists of the Gaussian conditioning identity behind (9), the Gaussian integral of on p. 7, the shift argument for Lemma 5, and the assembly into Theorem 2 with every hypothesis made explicit. The model layer (Gaussian prior, posterior, threshold equilibria) is reusable for the paper's other results and for related global-game pricing models.
The paper treats (9) as a change of conditioning, but it is where the posterior formula of p. 9 must be shown to be the actual conditional law of the quality given a valuation, inside an integral restricted to valuations above the cutoff: the profit (2) integrates over qualities, the right side of (9) over valuations, and connecting them requires Fubini over the joint Gaussian law of together with the factorization of the joint density into times the posterior density. The strict part of Lemma 5 needs more than "a shift of an increasing function is larger": the increase must happen on a set of positive Gaussian measure, which uses that a monotone non-constant function differs between two shifted Gaussian laws. Theorem 2 also uses that the equilibrium cutoff lies in , which is where the bound and Assumption 1 interact.
The model is a structure with fields and a validity predicate , , which every statement assumes (implicit on the page). Laws are Mathlib's gaussianReal, with variances passed through Real.toNNReal; expectations are Bochner integrals of bounded measurable integrands. and are the published BlackScholesModel.stdNormalCDF and stdNormalPDF. The reward program is a function ℝ → ℝ constrained to on , "increasing" means weakly increasing on , and is defined from and the same cutoff used in (1) and (2). In milestones 2–5 the reward is a general measurable function with values in , the paper's . Lemma 5 is posed on with " non-constant": non-constancy of on does not survive composition with , whose range is . Assumption 1 enters only through its maximization clause over prices ; its first-order characterization is not posed. Integrals are over the open half-line.
Three formalizations would trivialize or alter the goal and are excluded: restricting to strictly increasing programs (which drops constant rebates), decoupling from the equilibrium cutoff, and comparing the profit with the price- profit instead of the no-reward profit at the market price .
Contributions welcome: proofs of the milestones in any order, in particular the Gaussian identities (milestones 1 and 2), which are of independent use for Gaussian signal models, and general lemmas on Gaussian shifts of monotone functions.
Forecasting competitions ask many forecasters to report probabilities for many future binary events and award a single prize to one of them. They are used to identify and reward accurate forecasters: the Good Judgment Project gave "superforecaster" status to the top 2% by quadratic score, and data-science platforms run similar leaderboards. The usual rule ranks forecasters by the average of a proper scoring rule and pays the top scorer. A proper scoring rule makes truthful reporting optimal for a forecaster paid in proportion to their score, but a winner-take-all prize changes the incentives: a forecaster who is behind gains by reporting more extreme probabilities, because the competition rewards variance as well as accuracy.
Witkowski, Freeman, Wortman Vaughan, Pennock and Krause (arXiv:2101.01816; Management Science, 2023) design single-prize mechanisms that are strictly incentive compatible (truthful reporting is the unique optimum, whatever the forecaster believes about the others) and that select the most accurate forecaster. Their first mechanism, ELF, borrows a lottery from the competitive scoring rule of Kilgour and Gerchak (2004) and is truthful for arbitrarily correlated events, but it cannot select the best forecaster with probability above . Their second mechanism, I-ELF, is the subject of this mission: it is both truthful under a natural independence assumption and accurate as the number of events grows. The paper also proves that no deterministic mechanism is strictly incentive compatible and that no mechanism can be accurate in the limit for every joint law of the events, so both restrictions in the main theorem are needed.
There are forecasters and events with outcomes . Forecaster holds beliefs and reports . A scoring rule scores a report against an outcome ; it is strictly proper if whenever , and we write when its values lie in .
The ELF lottery on one event gives forecaster the winning probability
The Independent-Event Lotteries mechanism runs one ELF lottery per event, producing an event winner with , and then selects the forecaster who won the most events, breaking ties uniformly at random. The mechanism requires when and (values strictly below on reports in ) when .
Accuracy is measured by the expected score under a joint law of the outcomes. A joint law of the outcomes and the other forecasters' reports is belief independent if the per-event pairs are independent across ; within an event, reports and outcome may be correlated arbitrarily.
For strictly proper and measurable in the report:
The goal fixes no constants: it asserts the shape of the guarantee, not the rate.
Theorem 6 rests on Theorem 2 (single-event ELF is strictly incentive compatible for arbitrary correlation between reports and outcome) and on four steps of its proof (p. 34): the factorisation of I-ELF's selection probability under belief independence, the uniform transfer of expected event-winning probabilities, and the weak and strict monotonicity of the most-wins rule under such a transfer. Theorem 7 rests on Proposition 2, the one-sided Hoeffding inequality as stated on p. 35, eq. (9), the bound , and the explicit lower bound
Theorems 6 and 7 are also milestones on their own.
The theorem gives a single-prize competition that forecasters cannot profitably game, under any beliefs about others that respect independence across events, and that selects the most accurate forecaster with probability tending to one. The explicit rate in the proof of Theorem 7 tells a competition designer how many events are needed for a given accuracy gap and confidence. The incentive guarantee holds in dominant strategies and without risk neutrality, since forecasters care only about the probability of being selected.
The results are proved in the paper. None of them has a machine-checked proof that we know of, and the platform has no formal model of forecasting competitions, scoring-rule lotteries, or selection by most wins with random tie-breaking. A formal development would provide reusable definitions of strictly proper binary scoring rules and of lottery-based selection, and a checked version of an argument (pivotality of an event under uniform tie-breaking) whose case analysis is easy to get wrong.
The incentive half is not linear. Under ELF, a forecaster's selection probability is an expectation of a lottery that is affine in their score, so properness transfers directly. Under I-ELF the selection depends on the whole vector of event winners through an arg max with ties, and correlation between others' reports and outcomes could make an event's lottery depend on the rest. Belief independence removes the correlation across events. Strictness then needs an event to be pivotal with positive probability, and that fails when a scoring rule can reach : a forecaster sure to win two events can make a third irrelevant (the paper's footnote 10). The accuracy half needs concentration of the number of events won, with the constants tracked through the of the lottery.
Forecasters are Fin n with , events Fin m, outcomes Fin m → Bool (true means occurred), reports real numbers constrained to by hypotheses. A scoring rule is R : ℝ → Bool → ℝ; it is assumed measurable in the report so that selection probabilities under a law of the reports are well-defined expectations. I-ELF's selection probability is an explicit finite sum over event-winner vectors with uniform tie-breaking. A belief-independent law is the product (Measure.pi) of per-event joint laws of the outcome and all reports on that event; the selecting forecaster's own coordinate is overwritten by their report. Independent outcome laws are parametrised by their marginals . Limit accuracy is stated for the selection probability of an arbitrary mechanism, with the threshold chosen before , , the reports and the forecaster. Theorem 7 and its lemmas assume only , not strict properness, which the proof does not use.
Trivialising readings are excluded: incentive compatibility is strict (weak compatibility holds even for rules reaching ); others' reports are random and may correlate with the outcome within an event, not fixed; the limit-accuracy threshold may not depend on or the reports; and the selection rule is "most event wins", not the event-lottery average of multi-event ELF.
A complete development needs finite product measures and integrals of products, sub-Gaussian concentration for bounded independent variables (available in Mathlib), and a combinatorial analysis of the arg max under one changed coordinate. The definitions of scoring rules and lottery mechanisms are reusable for other elicitation and competition results. Proofs of any milestone are welcome, as are alternative arguments for the pivotality step.
Assembly projects such as aircraft programs or large software releases split work among several contractors, each responsible for one component. The finished product can only be as advanced as its least-developed component, so the contractors play a minimum-effort game (also called a weakest-link game): the project's value depends on the minimum of the efforts, while each contractor pays for its own effort. Such games have a continuum of Nash equilibria, ranked by payoff, and laboratory evidence since Van Huyck, Battalio and Beil (1990) shows that groups often settle on low-effort equilibria, with larger groups faring worse.
An original-equipment manufacturer (OEM) can affect coordination through the information it shares. Zhang, Shokoohyar, Qi and Katok, Coordination for Assembly (Manufacturing & Service Operations Management, doi:10.1287/msom.2023.0342), study a periodic information-feedback mechanism: the project runs over periods, and at the start of each period every contractor sees every contractor's progress. Their theoretical prediction, tested in the laboratory, is that the number of feedback periods relative to the number of contractors decides whether coordination succeeds. This mission formalizes the negative half of that prediction: with too few feedback periods, the selected equilibrium is the worst one.
There are contractors and periods. Each contractor's total effort lies in and its effort in each period lies in , with , where is the OEM's target level. All contractors start at zero effort. In period each contractor observes all efforts so far and then all simultaneously choose ; the effort level of contractor after period is .
The project level is , the OEM's payoff is , and contractor receives the share of it and pays per unit of effort:
The parameters satisfy .
A history is the list of effort profiles played so far; a strategy maps each history to the current period's effort. A subgame-perfect equilibrium (SPE) is a strategy profile from which no contractor gains by deviating after any history. For a history , write for the set of final level vectors reached by continuing some SPE from .
A subgame-perfect secure equilibrium (SPSE) (Definition 2 of the paper's Online Appendix) is an SPE such that, at the start of every period along its own path, each contractor's own final level maximizes its worst-case profit
among the levels that contractor attains in some SPE continuation. This is the paper's condition (24): among equilibria, contractors favour the one that protects them against the other contractors' least favourable equilibrium behaviour.
If , then an SPSE exists in which every contractor exerts the minimum effort in every period, every SPSE has this property along its path, and the project level is minimal:
The result says that frequent progress reports are not enough by themselves: when there are fewer feedback periods than contractors minus one, the secure refinement of subgame perfection selects the lowest project level, the same outcome as without feedback. It is the theoretical half of the paper's comparison between feedback regimes, which the laboratory experiment then tests with groups of two and four contractors and 1 to 6 feedback periods.
The result has a printed proof in the paper's Online Appendix. No machine-checked version exists. Formalizing it pins down a solution concept (an SPE refined by a maxmin criterion over the set of equilibrium outcomes of each subgame) whose verbal definition admits several inequivalent readings, and fixes which one the proposition holds for.
The companion part (ii) of Proposition 2, for , is false as printed and is not part of this mission: with , , , , , , , the profile with path is an SPE with project level , and no SPSE reaches , although part (ii) predicts that level at . Corollary 2 and Proposition 3, which rest on part (ii), are omitted for the same reason.
The existence half is a statement about whole strategy profiles, including play after every history off the equilibrium path. The constant profile that plays after every history is not an SPE when : after a history that leaves one contractor strictly behind with one period to go, that contractor gains by catching up. An SPE with the all-minimum path must therefore prescribe different, history-dependent behaviour off the path, and the count of tied contractors is what keeps a single deviation from breaking the tie at the bottom.
The SPSE condition quantifies over the set of all SPE outcomes of each subgame, so neither half can be checked by looking at one profile: both existence and uniqueness require knowing that the all-minimum outcome lies in that set at the relevant histories.
All quantities are real numbers; there is no probability. Contractors are indexed by Fin M and periods are 0-based (pathHist σ n is the history before the paper's period ). A history is a List (Fin M → ℝ) and strategies are arbitrary functions of the history: under feedback every past effort is observed, and restricting to state-dependent or open-loop strategies would change the set of SPEs that the definition compares against.
Committed conventions:
N + 1 ≤ M;Trivializing encodings are ruled out: the SPSE carries the SPE clause, the condition is neither dropped nor imposed at every history (under which no SPSE would exist), and the goal includes an existence conjunct, so it cannot hold vacuously.
The development needs the game, its SPE and SPSE (one definition file in the mission), and arguments about backward induction in a finite-horizon game with continuous actions. Proofs of the milestones, of the goal, and reusable lemmas about cumulative-effort games are all welcome.