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?
Online marketplaces such as Airbnb, Amazon, eBay, Preply or Upwork earn most of their revenue from transaction fees: a seller who sells through the marketplace pays a fee on every sale. Many of these sellers also run their own sales channel, and a buyer who discovers a seller on the marketplace can often complete the purchase directly with that seller, avoiding the fee. This is marketplace leakage (also called disintermediation or showrooming of the platform). Marketplaces respond with measures the paper lists on its first pages: bundling transaction-related services, restricting buyer–seller communication before a transaction, and penalizing sellers caught taking clients off the platform.
Hagiu and Wright (Marketplace Leakage, Management Science, 2023) build a minimal model of this tension. Their baseline analysis answers the first question any of the later strategies depends on: if the marketplace can only choose its fee, what fee does it set, how much leakage remains in equilibrium, and how do these respond when buying directly becomes more costly for buyers? This mission formalizes that baseline result, Proposition 1 of the paper, for uniformly distributed switching costs.
There is one marketplace , one seller and a unit mass of buyers, each wanting one unit of 's product. Every buyer values the product at ; 's marginal cost is , with ; the outside option is worth .
can sell through , paying a fee per transaction, or through its direct channel, which carries no fee. It sets a price on and a direct price . A buyer who buys directly bears a switching cost ; in this mission is uniformly distributed on with , so its CDF is
The timing is: sets ; observing , sets its prices; buyers then choose. The paper's Lemma 1 lets one fix , so only chooses . A buyer buys directly iff , so a share of buyers — the leakage — buys directly. 's profit at fee is
and earns . A direct price is seller-optimal at if it maximizes over . An equilibrium outcome is a pair with , seller-optimal at , such that no other fee , followed by a seller-optimal response, gives more.
For every an equilibrium outcome exists, and every equilibrium outcome satisfies
with leakage . As increases, the fee weakly increases, the direct price and the leakage weakly decrease, and the marketplace's profit strictly increases.
Proposition 1 is the baseline against which the paper measures every anti-leakage strategy: investment in transaction benefits, communication bans, referral fees and price-parity clauses are each compared with the fee-only outcome , and Proposition 3 of the paper uses the closed form (6) directly. The result also has a substantive message: a fee-setting marketplace never eliminates leakage, but never lets it become total, and it gains from higher switching costs even though its own fee response offsets part of their effect on leakage.
The proposition is proved in the paper by elementary calculus. To our knowledge it has no machine-checked proof. Formalizing it produces a checked version of the baseline game, a verified statement of the seller's best response and the marketplace's value as functions of the fee, and a template that the companion missions on this paper reuse.
The seller's problem is not a smooth concave program: the clamped distribution creates a kink at , below which every buyer switches and the profit is linear in . The first-order condition is the optimum only while ; above that the optimum sits at the kink. The marketplace's objective inherits a kink at , and its feasible set adds a corner that binds exactly when . Negative fees are feasible and must be ruled out. The comparative statics compare equilibrium objects across two parameter values that may lie in different regimes, so the statement cannot be read off one formula.
All parameters are real numbers, with the standing assumptions and as explicit hypotheses. is the clamped uniform CDF above. The statements use the reduced seller problem (1) with , as the paper does after Lemma 1; Lemma 1 itself, which concerns the full game in which also chooses , is not posed. Seller-optimality is an optimality predicate over , and the equilibrium is an optimality predicate over feasible fees (negative fees included); "max" is attained, not a supremum. The displays (4) and (5) are stated for , which is what they require; the paper's preface "Assuming " is not needed and does not exclude .
Trivializing formalizations are ruled out: the seller's response and the marketplace's profit are not defined by the closed forms (4)–(5), the marketplace's value is not an unattained sSup, the equilibrium fee is not selected by Classical.choose, and the comparative statics are stated about equilibrium outcomes at two values of , not about the formulas alone.
The development needs only Mathlib's real arithmetic, min/max and order lemmas. A proof of the seller's best response for a clamped uniform distribution is reusable in the companion missions on transaction benefits, communication bans and price parity, which restate the same model. Proofs of any milestone are welcome independently.
Quantum state tomography reconstructs an unknown -dimensional quantum state from measurements on many copies of it. For qubits, , so the number of copies a tomography procedure needs grows exponentially in , and lower bounds on that number decide how far experiments can scale. In many experiments the only measurements available are Pauli measurements: each qubit is measured in the eigenbasis of one of .
Flammia and Liu, Direct fidelity estimation from few Pauli measurements (arXiv:1104.4695, Phys. Rev. Lett. 106, 230501, 2011), show that the fidelity of an experimental state with a target pure state can be estimated with far fewer copies than full tomography needs. To make the comparison meaningful they also prove that full tomography of a pure state with Pauli measurements requires copies. That lower bound has two steps. The first builds a large family of nearly orthogonal pure states whose Pauli expectation values are all small, so that Pauli measurements extract little information about which state is present. Its engine is Lemma 1 of the paper (p. 7), the subject of this mission. The second step, an information-theoretic argument over a noisy classical channel, is not in scope.
Fix qubits and put . States are unit vectors , ; the overlap is conjugate-linear in .
The single-qubit Pauli matrices are , , , . A Pauli label determines the -qubit Pauli operator (with ). There are labels; the all-zero label gives . Every is Hermitian and unitary, so the Pauli expectation is a real number in .
A Haar-random state is a vector drawn from the uniform (rotation-invariant) probability measure on the unit sphere of , a real sphere of dimension . The constants of the lemma are
with the natural logarithm and a parameter.
Let be states with . Then there is a state with
These are (31) and (32) of the paper. The goal is an existence statement with no measure in it.
Every constant is the paper's; none is replaced by an unspecified absolute constant.
The result. Lemma 1 is a packing statement: applied repeatedly, it yields states that are pairwise almost orthogonal and whose non-identity Pauli expectations are all . Such states are hard to tell apart with Pauli measurements, since each measurement outcome is nearly unbiased. The paper converts this into the copy lower bound for full tomography with Pauli measurements (pp. 3, 7–8). Since direct fidelity estimation of an arbitrary pure state uses copies (for fixed accuracy and failure probability), the lower bound is what shows that the scheme beats tomography followed by a fidelity computation by a factor of about .
Formalizing it. The lemma and its proof are published, but none of it is machine-checked: Mathlib has no Pauli operators, no concentration of measure on spheres with explicit constants, and no Levy lemma. A formal proof needs a concentration inequality on the complex unit sphere with the explicit constant (or any sharper one), the vanishing of the means by symmetry, and the union bounds. Each milestone is a reusable fact about Haar-random states.
The two union bounds (35) and (38) and the Lipschitz estimates (33) and (36) are elementary. The central difficulty is the tail bounds (34) and (37). The paper obtains them from Levy's lemma, which it cites (P. Lévy, 1951) and does not prove; Levy's lemma rests on the isoperimetric inequality on the sphere, which Mathlib does not have, and (37) concerns a quadratic form of rather than a linear one. Both tail bounds also need a working theory of the uniform measure on the complex unit sphere (rotation invariance, the distribution of a coordinate), little of which exists in Lean today.
A second difficulty is that the printed proof does not cover every parameter. The union bound produces a good only when . For small , or small with few given states, the goal is still true, but a complete proof must handle those cases separately; they are not in the paper.
Q n = Fin n → Fin 2, Pauli labels P n = Fin n → Fin 4, states live in EuclideanSpace ℂ (Q n), and is the entrywise product of single-qubit Pauli matrices (the Kronecker product). is the real number ; is Real.log; ⟨φ|ψ⟩ is Mathlib's inner ℂ φ ψ.Measure.toSphere of an additive Haar measure on (as a real vector space), normalised to total mass one. The paper's "Haar-random vector in " is read as this measure on the unit sphere of .Many service relationships are dynamic contracts in which the principal cannot observe the agent's effort, only its noisy consequences. Cao, Sun and Tian (Management Science, 2024) study such a relationship when the principal can suspend the agent and must pay a fixed switching cost to restart work. Suspension is a punishment that does not end the relationship, and it is used in practice for platform workers, contractors and franchisees. The paper shows that, when the switching cost and the revenue are low, the optimal contract has a control-band structure: the agent's promised utility is kept inside an interval, the agent is suspended when it falls below the lower end, and work resumes at the upper end. Two-threshold policies of this kind are standard in optimal switching problems with switching costs (Duckworth and Zervos, 2001; Vath and Pham, 2007), whose verification arguments the paper compares with its own.
This mission is the fourth of a series formalizing the analytic core of the paper. It covers the low-switching-cost region (Area III of the paper's Figure 2).
A Poisson process of arrivals brings revenue each. The base arrival rate is ; if the agent works, at cost per unit of time, the rate becomes . Write . The principal's cost rate while the agent works is , restarting work costs , and the principal and the agent discount at rates . Assumption 1 is . The constants are
The promised utility is the state. For a function on with left derivative , the paper's operators are
for the working state and the suspended state . A pair satisfies the optimality condition (20)–(22) if , , and .
Two families of functions enter. In the suspended state, (24) solves with . In the working state, for , is the solution of the delay differential equation (25), in which is coupled to the look-ahead value , with beyond ; is its concavification (Lemma 2), linear below a threshold . Lemma 3's is the unique with under Condition 1.
The parameter regions are Condition 1 ( or ), Condition 2 (its negation) and Condition 3: Condition 1 and , or Condition 2 and , with (28), (K1) and (33) explicit thresholds.
The paper uses three different hats: Definition 1's payment threshold , Lemma 3's upright , and Proposition 6's bold , the upper end of the control band.
Under Condition 3 there are parameters satisfying Proposition 6 such that
satisfy (20)–(22).
Under Condition 3 there is with , and value matching and smooth pasting at both thresholds:
Lemma EC.4 (the first step of the EC.3.9 construction), Proposition 6, and the two hardest parts of (20) at the constructed tuple: Lemma EC.12 ( on ) and Lemma EC.13 ( below ). The other steps of the construction are posed as further statements of the mission without milestone status: Lemma EC.7 (the root of under Condition 1), Lemma EC.8 and Lemma EC.11 (the Condition 2 counterparts of EC.4 and EC.7).
Proposition 7 is the analytic certificate behind the paper's Theorem 5: combined with the verification Theorem 1, it shows that the control-band contract is optimal in the low-cost region, and that the principal's value is . Without it the third case of the paper's main Theorem 2 is unproved. The construction of Proposition 6 also gives a computable description of the band, which the paper uses for its numerical illustrations.
The results are proved in the paper's e-companion; none of them has a machine-checked proof. This mission states the analytic part as Lean targets. The delay-ODE layer (existence, uniqueness and shape of ) is shared with the first mission of the series, and Proposition 7's proof depends on it. The stochastic contract model, the verification theorem and the optimality Theorems 1–5 are not formalized in this series.
Each piece of (20)–(22) is a one-variable inequality, but the functions are not explicit. is defined through a delay equation, and the band's endpoints are defined implicitly through four nested steps: matching at , a range bound , an upper threshold and a root of a gap function . The natural argument, convexity or concavity of on the suspension region, fails: on the function mixes with the look-ahead value and is not convex (p. 28), so the convexity arguments of the switching literature do not apply. The paper's proof of this single inequality occupies EC.3.12, with eight auxiliary lemmas.
Functions are ℝ → ℝ and every statement quantifies over . The standing assumptions are , , , and Assumption 1; and are disclosed additions. Conventions:
The tuple is never defined by the property that (46) satisfies (20)–(22); the construction definitions are Steps 1–4 of EC.3.9 only, and the goal requires all of Proposition 6's conclusions. The second claim of Proposition 7, (48) on the contract's utility, is out of scope.
A complete development needs existence, uniqueness and regularity for the linear delay equation (25) (reusable for other delay problems), implicit-function arguments for , and the sign analysis of EC.3.12. Proofs of single milestones, and of the delay-ODE lemmas of the series' first mission, are welcome.
Digital businesses (search engines, social networks, marketplaces) record what their users do and decide how well to protect what they record. Both choices affect users: stored data can improve the service, and it can also be accessed by adversaries such as hackers, fraudsters or data brokers, whose activity harms users. Regulation of data collection and data protection (the GDPR, the CCPA, liability rules for breaches) presupposes an answer to a basic question: in which direction does a profit-maximizing business's data strategy deviate from the one a benevolent planner would choose?
I. P. Fainmesser, A. Galeotti and R. Momot, Digital Privacy (Management Science 69(6), 2023; author manuscript SSRN 3459274), answer it in a model where users, adversaries and the business all respond to each other. Their Theorem 2 shows that the deviation is not arbitrary: one combination of errors never occurs, and the sign of the error is pinned down completely for a business whose revenue depends only on usage. This mission formalizes those two claims.
A data strategy is a pair : the share of each user's activity that the business stores, and a protection level , which costs . The parameters are real numbers: a network effect , the users' marginal benefit from stored data , the cost , the revenue model , and the planner's weight .
Given , a unit mass of identical users choose activity levels and a large population of adversaries decide whether to access the stored data. The resulting equilibrium (Proposition 1 of the paper, display (3)) has average user activity
The value at is the activity when nothing is stored, the value the paper uses where (3) reads . From one builds the consumer surplus (4), the business's profit (2) and the planner's objective (7):
The revenue model interpolates between a purely usage-driven business (, revenue proportional to activity) and a purely data-driven one (, revenue proportional to stored data ). A business optimum maximizes over the feasible set ; a social optimum maximizes over the same set. The business under-collects if and over-protects if , and so on.
The paper's Theorem 2 (p. 13) reads:
Relative to the socially optimal strategy, the equilibrium data strategy of a purely usage-driven business (P = 0) prescribes under-collection and under-protection of users' data, i.e., ξ* ≤ ξ^W and C* ≤ C^W. The equilibrium data strategy of a business with any data-driven component in its revenue model (P > 0) never prescribes under-collection and over-protection of users' data i.e., it is never the case that ξ* ≤ ξ^W and C* ≥ C^W with at least one of the inequalities being strict. Any other direction in which the optimal business's data strategy deviates from the socially optimal strategy is the outcome for some specification of the business's revenue model and values of other model parameters.
The goal is its first two sentences, for every business optimum and every social optimum:
The third sentence is established numerically in the paper (Figure 3) and is not a target.
The result. Theorem 2 identifies the one inefficiency that no revenue model produces: a business never stores too little data while protecting it too much. All other combinations occur for some parameters, so a regulator cannot infer the direction of a business's error without knowing its revenue model; but for a purely usage-driven business the direction is known, and it is too little protection. This underlies the paper's discussion of policy in §6, where the instruments considered (liability for data breaches, taxes on data) are compared by how they move towards .
The formalization. The result is proved in the paper (App. A.4, with Proposition 5 in Online App. C.5); it has not been machine-checked. The paper's argument for the purely usage-driven case refers to first-order conditions and does not treat the boundary strategies (, ) or parameter corners () separately; a formal proof has to handle them. A complete development also yields reusable facts about the equilibrium activity : its sign, its behaviour in for fixed , and the monotonicity in of the activity-maximizing collection level.
Both optima are defined only implicitly, as maximizers over a non-compact feasible set of a non-concave objective, and neither has a closed form that this mission may use. The comparison must therefore work from the optimality inequalities alone. The tempting approach, comparing first-order conditions, does not give a global statement: and may have several local maxima, the maximizers need not be unique (both optima are in a whole region of parameters), and the constraint binds for large protection. In the purely usage-driven case the profit and welfare share their maximizers in for each fixed , but turning that into a comparison of with requires control of how the maximizing moves with , including at .
All objects are real-valued functions of explicit real parameters and of the strategy , in the namespace DigitalPrivacy.Welfare, which imports , CS, the feasible set and the business optimum from the shared module DigitalPrivacy.Strategy.Setting. The equilibrium activity takes the value at for every , as in the paper; Lean's default is not used. Optima are predicates (IsBusinessOpt, IsSocialOpt): a feasible point at which the objective is at least its value at every feasible point. Theorem 2 quantifies over every pair of optima and asserts neither existence nor uniqueness. The P > 0 clause keeps the "at least one strict" condition; without it the clause is false, because both optima coincide at in part of the parameter space.
The standing assumptions are the paper's ranges , , , , with two disclosed strengthenings: (with , , , every is both a business and a social optimum and the sentence fails) and (with the planner's problem is the business's, and step (11) does not hold). Proposition 5(i) is stated with the printed ranges, included. No other hypothesis is added, so the hypotheses on the optima cannot be made vacuous by the encoding; a sanity check exhibits parameters at which is both a business and a social optimum.
A complete development needs elementary real analysis of the rational function on and nothing beyond Mathlib. Proofs of the milestones, of lemmas about , and alternative arguments for the goal are all welcome. The paper's proofs are in App. A.4 (pp. 33–35) and Online App. C.5 (Online pp. 8–9).
Two classical online selection problems sit at opposite ends of an information spectrum. In the secretary problem items arrive in uniformly random order, only their relative ranks are observed, and the best possible probability of stopping on the best item tends to . In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee against the expected maximum is the constant of Hill and Kertz (1982), shown tight by Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017).
Correa, Cristi, Epstein and Soto (arXiv:2011.06516) interpolate between the two with the -sample-driven optimal stopping problem. Each of items is sampled independently with probability ; the decision maker observes the relative rankings of the sampled items, then faces the remaining items online, observing relative rankings, and makes irrevocable stop/continue decisions. Stopping on the item of overall rank earns a reward , with . At and this is the secretary problem; for adversarial the optimal guarantee tends to as , the i.i.d. prophet constant.
For known , the paper writes a linear program over the stopping probabilities of rank-based algorithms (after Buchbinder, Jain and Singh, 2014) and takes its limit as . The analysis rests on one structural result, Theorem 2: this limiting program can be restricted, without loss, to solutions of an explicit threshold form, so that the optimal algorithm stops on an item of current rank after a time . This mission is that theorem.
Fix . Time runs over (time is the fraction of the items seen so far; the sample accounts for the first fraction in the limit), and ranks refer to the relative rank of the current item among all items seen so far. A candidate solution is a function , the density of stopping at time on an item of relative rank .
The cumulative mass of is . A solution is feasible for the continuous linear program CLP when , each is integrable on , and
For the negative-binomial term is , the probability that a NegativeBinomial variable is at most , and
is the limit of the probability that the algorithm stops on an item of overall rank at most . The objective of CLP is for a non-increasing sequence , so any solution that increases every is at least as good.
A threshold sequence is a non-decreasing with ; put .
For every feasible there are a feasible and a threshold sequence with for all , such that for every and
Theorem 2 turns an infinite-dimensional linear program over functions of two variables into the reduced problem RP, an optimization over a single non-decreasing sequence of thresholds. Every quantitative result of the paper is read off RP: the optimal ratio for each , its limit as (Theorem 8, mission II of this series) and the explicit lower bound (Theorem 9, mission III). It also identifies the optimal rank-based algorithms as threshold rules: accept the current item if it is among the best seen so far, where grows at the times .
The result is proved in the paper. It has not been formalized, and neither has any part of the continuous-LP approach to secretary and prophet problems. The formal development produces a reusable layer: continuous stopping LPs with extended-real cumulative constraints, monotonicity of negative-binomial distribution functions in both parameters, and a rearrangement argument for integrals against monotone weights.
The obvious argument is to improve greedily: push each component's mass as far right as the constraint allows. One step is easy, but the step changes the constraint itself, since the envelope depends on all components. The proof iterates, needs the thresholds to be monotone in , and must pass to a limit in with a dominating function that exists only because the smallest threshold is bounded away from . The limit thresholds need not be monotone in , and the components must then be reordered using Lemma 18. Finally, (5)–(6) are an integral equation in which each component depends on the sum of all others; identifying their unique solution with (7) needs both a uniqueness argument for a linear ODE and a telescoping computation.
q : ℝ → ℕ → ℝ, a representative of an element of . Ranks, , , are 1-based; is never used. Constraints are imposed pointwise for all , as printed.Many service relationships pay an agent per unit of output whose arrival is random: a salesperson closing deals, a call-centre worker resolving tickets, a contractor delivering jobs. When effort is unobservable, the classical tool for keeping an agent motivated is the threat of termination after poor performance. In practice firms often use a milder punishment, suspension: the agent is sent home for a while and later called back. Restarting work is not free, and each restart costs the firm a fixed switching cost.
P. Cao, P. Sun and F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost (Management Science, 2024), characterise the optimal dynamic contract in this setting. The optimal contract depends on the size of the switching cost: when it is large the firm should not hire, when it is moderate the firm should keep the agent working forever, and when it is small the firm uses a control-band contract with suspension episodes. Their proof is "guess and verify": a stochastic verification theorem (their Theorem 1) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value, and Propositions 2–7 exhibit such pairs in each parameter region.
This mission formalizes the certificate for the medium-switching-cost region under Condition 2 (Area II of the paper's Figure 2), where the agent is never suspended.
The principal faces a Poisson stream of arrivals, each worth revenue . Without effort the arrival rate is ; an agent who exerts effort, at cost per unit time, raises it to . Write . The principal's total cost rate while the agent works is , every start of work costs a switching cost , and the principal and agent discount at rates . Assumption 1 is .
The paper's derived constants are
together with the revenue thresholds (28) and (34) and the switching-cost threshold (33). Condition 2 is and : the agent is much more impatient than the principal and revenue is high.
The state variable is the agent's promised utility . Two operators act on functions of , where is the left derivative:
The first is a delay-differential operator for the working state, the second a first-order operator for the suspended state. A pair satisfies the optimality condition (20)–(22) when , , and .
The suspended-state equation with is solved by (24). In the region of this mission the paper builds
from parameters chosen so that pastes smoothly onto the line at and ends at at .
Under Condition 2 and , for every triple with , , and
the functions above satisfy (20)–(22).
Lemma 5 guarantees that the goal is not vacuous.
Proposition 5 is the analytic half of the paper's Theorem 4: combined with the verification theorem, it shows that in Area II the principal's optimal value is attained by a contract that pays the agent per arrival and never suspends. The threshold separates this region from the control-band region of Proposition 7, so the explicit formula for is the boundary of the phase diagram.
The result is proved in the paper. No machine-checked version exists. A formal proof checks a delicate sign argument near , where has infinite slope, and it checks the threshold , whose printed formula contains an error (see Formalization scope). The paper's companion identity (41), , is about the utility of a contract and is not part of this mission; its deterministic half is immediate from (39).
The cases and are algebraic. The difficulty is : there is the curve , and lands beyond (Condition 2 gives ), so couples the curve with the constant . Positivity there needs more than the sign of the smooth-pasting slope: it uses the lower bound on in (35), which is exactly where the threshold enters. A direct sign check at alone does not cover the interval. The existence lemma requires monotonicity of , whose expression mixes powers with a linear factor.
All functions are ℝ → ℝ and every quantifier ranges over ; powers are Real.rpow. The standing assumptions , , , , are one hypothesis Standing; and are read off the model and stated explicitly. The left derivative is derivWithin f (Set.Iic w) w, following the paper's convention on p. 15. Condition (20) is posed for only: at the right derivative of is , so the paper's (20) there is an extended-real statement and Lean's junk derivative would make it false. (21) and (22) are posed as printed.
The threshold of (33) is corrected: the printed bracket contains , but the paper's own proof identifies with of (EC.69), which gives . With the printed term Lemma 5 fails (for , the printed value is , the corrected one ). Equation (36) is printed with a free that should read . The range , given by the proof, is stated.
The goal quantifies over all triples satisfying Lemma 5's conclusions; such a triple is unique, so this is the paper's claim, and Lemma 5 rules out a vacuous goal. Dropping the bound in (21), the condition (22), or the lower bound on would trivialize or change the statement.
The development needs the derivative of , sign analysis of explicit real functions, and the intermediate value theorem. The Setting file is shared with the other missions of this series and will be consolidated. Proofs of the milestones in any order are welcome; (EC.67) is a self-contained calculus exercise.
One-way vehicle-sharing systems (car sharing, bike sharing, ride-hailing fleets) set a price for every origin–destination trip. Prices decide which trips are taken, and so they decide where vehicles end up. Pricing that depends on the current position of every vehicle is in principle optimal, but its state space grows combinatorially with the fleet. Practitioners therefore use static prices, which depend only on the origin and destination. The question is how much revenue, throughput or welfare such prices give up.
Benjaafar and Shen (SSRN 3998297; Technical Note, Operations Research, 2023, doi:10.1287/opre.2023.2446) answer this with explicit lower bounds on the performance ratio of the static policy obtained from a fluid relaxation. Banerjee, Freund and Lykouris (arXiv:1611.07624) proved the earlier guarantee, which requires the fleet size to be at least and the workload to be at most . Benjaafar and Shen give two bounds that hold for every . The first is (their Theorems 1–2), and it degrades when total demand grows with . The second, Theorem 3, does not depend on demand or travel times at all. This mission is about Theorem 3.
There is a finite set of locations and vehicles. Trip requests from to arrive as a Poisson process of rate , and is the set of pairs with demand. The graph is strongly connected. A trip from to lasts a random time with mean . A static policy is a matrix of quantiles: is the fraction of customers who accept the posted price. Each accepted trip earns a reward , and is concave. A customer who finds no vehicle at the origin is lost.
Problem (2) is the fluid relaxation, in which vehicles are always available:
The first constraint balances the flows, and the second caps the workload (the mean number of vehicles in transit) by a budget . Let be an optimal solution that induces a strongly connected network.
Under a static policy the vehicles move in a closed queueing network. Each location has a single-server pick-up queue with service rate . Each pair has an infinite-server transit queue with mean service time . This network is of BCMP type, so its stationary law has product form. With a positive solution of the traffic equations (9), a state with vehicles at location and in transit from to has weight . The availability is the stationary probability that location holds at least one vehicle. The reward rate of the policy is Equation (3):
For , , optimal for (2), inducing a strongly connected network, with :
The paper states the bound for , where is the optimal dynamic policy. It passes from one ratio to the other with Proposition 1, (p. 6), whose proof needs the stationary analysis of arbitrary state-dependent policies. Proposition 1 is not part of this mission. The goal implies the paper's Theorem 3 once Proposition 1 is available.
The bound tends to at rate , uniformly in demand rates, travel times and the reward functions. It is the regime-free counterpart of the bound: that bound is better for light demand, this one for heavy demand (Remark 7). Remark 6 reports that it is also numerically tighter than the guarantee of Banerjee et al., and unlike that guarantee it applies to every fleet size.
Formalizing it adds several things to the platform. The first is availability in closed networks of single-server and infinite-server stations, defined from the product form. Two classical facts about this model follow: availability is equal across locations under balanced flows, and it satisfies the mean-value recursion (5). Milestone 4 is a concavity statement about the throughput of a closed network in its population, and for it contains the concavity of the Erlang-B carried load in the number of servers. The paper does not prove it; it cites George and Xia (2011) and Shanthikumar and Yao (1988). None of these results is formalized anywhere that this mission is aware of, so the mission formalizes a proved result, not an open problem.
The algebra at the end (milestones 6–7 and the substitution ) is elementary. Two steps are not.
Equation (5) is stated as a relation between availabilities, but its content is an identity between normalizing constants of the product form. The paper derives it from the arrival theorem and Little's law, and neither is available. A direct proof has to compute under balanced flows, which takes a counting argument over the state space. Equal availability likewise needs the positive solution of (9) to be unique up to scale on a strongly connected network.
Concavity of is the hard milestone. A natural first attempt is induction on the recursion: if is non-increasing up to , show that the next increment is no larger. The map is increasing and convex in its argument, and convexity points the wrong way, so increments do not propagate directly. The published proofs go through the closed-network interpretation, not through the recursion.
The Lean development lives in VehicleSharePricing.DemandFree. Locations are a Fintype with Nonempty, and is its cardinality. Λ, μ, q are real matrices on all pairs, and entries outside enter only multiplied by . Strong connectivity is the transitive closure of the positive-flow relation (Relation.TransGen). This guarantees at every location, even for . Availability is the product-form busy probability of the general definition ProductFormNetwork, applied to the induced network. That law is a definition that records the paper's appeal to BCMP (p. 6), not a theorem of this mission. Theorems quantify over every positive solution of (9). is Equation (3) with per-location availabilities. The sequence is defined by its recursion, which is correct because it is a proof device, not the availability of . All arithmetic is in , and appears only under .
Two trivializations are ruled out. Defining by the recursion (5) would make milestones 1–3 empty, and defining as would make milestone 1 empty. The hypothesis is added because the ratio is otherwise .
The proof of the goal uses only feasibility of and the strong connectivity of the induced network; optimality is kept because it is the paper's hypothesis. Contributions are welcome on any milestone. A library for normalizing constants of closed product-form networks, and the concavity of throughput in the population, would be reusable well beyond this paper.
One-way vehicle-sharing systems (car sharing, bike sharing, on-demand fleets) move a fixed fleet of vehicles among locations. Customers take a vehicle at one location and leave it at another, so prices shape both revenue and where the fleet ends up. The optimal dynamic pricing policy, which reacts to the current position of every vehicle, solves a dynamic program whose state space grows combinatorially in and . Static policies, with one fixed price per origin–destination pair, are simple to compute and to operate, and the question is how much they lose.
Benjaafar and Shen (SSRN 3998297; Operations Research, 2023, doi:10.1287/opre.2023.2446) take the static policy that solves a fluid relaxation, Problem (2), and bound its performance ratio. When induces a strongly connected network, Theorem 1 gives the ratio . Waserhole and Jost (2016) observed that the best static policy may deliberately disconnect the network: prices that make some trips unattractive can leave two or more separate networks. The fleet then has to be split among the pieces, and Theorem 1 no longer applies. This mission formalizes Theorem 4 of the paper (§6, p. 18), which shows that the same guarantee holds in that case, provided the vehicles are allocated optimally among the networks.
There are locations and vehicles. Trip requests from location to arrive at rate , and is strongly connected. A trip on lasts on average . A static policy is a vector of quantiles (the fraction of customers who accept the price), and earns per trip, with concave.
Problem (2) maximises the fluid reward over balanced flows ( at every location) with workload , where . Let be an optimal solution.
The policy splits the locations into networks with location sets () and pair sets : accepted demand only joins locations of the same network, and within each network it is strongly connected. With vehicles, network is a closed queueing network: a single-server pick-up queue at each location (rate ) and an infinite-server transit queue on each pair. Its stationary law is the BCMP product form, with loads computed from a positive solution of the traffic equations (9). The availability is the stationary probability that a location of network has a vehicle.
An allocation with earns (Equation (3)), and Problem (8) chooses to maximise it. Write , for network 's share of , and .
The paper's Theorem 4 opens with , where is the reward of the optimal dynamic policy. That inequality is Proposition 1 (, p. 6). It needs the stationary distribution of the network under an arbitrary state-dependent policy, a controlled-Markov-chain development that is not part of this mission. The goal is the rest of the chain, and it implies the paper's theorem once Proposition 1 is available.
The result. Theorem 4 removes the connectivity assumption from Theorem 1. A static policy chosen by the fluid relaxation may disconnect the network, and it then still earns at least of the fluid optimum, uniformly in the demand and reward data. The bound tends to as for fixed and . Milestones 6–7 hold for arbitrary weights, location counts and workloads, so they apply to any separable allocation problem whose pieces satisfy recursion (5).
Formalizing it. The result is proved in the paper; nothing here is open. No part of it is machine-checked so far. The mission adds closed-network availability on a disconnected network, the mixture decomposition of the performance ratio, a real-argument Vandermonde identity in the paper's own notation, and a discrete allocation inequality proved by an averaging argument. The companion missions of this series formalize Theorems 1–3 of the same paper.
The obvious argument applies Theorem 1 to each network: . This leaves a maximisation over allocations, and no single allocation obviously beats . Proportional splitting fails because does not scale with , and the best allocation depends on all of , and . The paper does not exhibit a good allocation. It averages the objective against probability weights from the Chu–Vandermonde identity, which needs binomial coefficients with real upper arguments. It then passes from two networks to many by an induction that merges networks. The recursion (5) itself rests on a computation with the normalising constants of a product form that has both single-server and infinite-server stations.
Locations form a finite type. is the set of pairs with , and its strong connectivity is a transitive closure. The split is a surjective map from locations onto a finite index type of networks. Every pair with positive accepted demand stays inside one class, and each class is strongly connected under accepted demand, again as a transitive closure. So every location has positive accepted demand. The paper's is relaxed to .
Availability is the BCMP product form of each network on its own, with loads (pick-up) and (transit), and a positive solution of (9). This is a disclosed definition, since the paper invokes the BCMP class without writing it. Availability is defined per location; its equality across a network follows from milestone 1. is Equation (3) with per-location availabilities. Problem (8) is an explicit maximisation over the finite set of allocations. All ratios are real numbers, is assumed so that the ratio is defined, and is computed in .
Defining availability by the recursion (5), or as , would make milestones 1–2 trivial and is ruled out.
A complete development needs:
Ring.add_choose_eq);The closed-network definitions and milestones 5–7 are reusable beyond this mission. Proofs of any milestone are welcome, and so is a proof of Proposition 1.
Centralized matching markets (kidney exchange, ride hailing, freight and labor platforms) repeatedly decide which waiting participants to match now and which to hold for a better opportunity later. Matching early collects value sooner; waiting lets the platform see more arrivals and avoid matches that later turn out to be wasteful. A natural yardstick is the best set of matches that could have been made with hindsight from all arrivals up to a given time, and the question is how far an online policy, which cannot see the future, must fall behind that yardstick.
Kerimov, Ashlagi and Gurvich (SSRN 3824407, September 2022; Management Science 2023, doi:10.1287/mnsc.2021.01215) answer this for multi-way matching networks with patient agents. They identify a single parameter of the fluid relaxation, the general position gap , and show that the regret against the hindsight benchmark can be kept at order at all times, and that no policy does better in order on non-trivial networks. This mission formalizes the upper bound. The paper places itself next to constant-regret results for online packing (Bumpensanti and Wang 2020; Vera and Banerjee 2021), where resolving a linear program at each arrival achieves bounded regret.
There are agent types and matches. Match is a set of at least two types, every type belongs to some match, and the matching matrix has iff . Performing match uses one agent of each type in and earns . Time is discrete; at each time one agent arrives, of type with probability , , independently over time. counts the type- arrivals by time .
A matching policy records , the number of times match has been performed by time . It is admissible when it is non-anticipative and only matches agents present: . The pre-match queue is , the value collected is , and the hindsight benchmark is
The static-planning problem is the linear program
For an optimal let (active matches), the rest (redundant matches), (under-demanded types) and the rest (over-demanded types). The network satisfies general position (GP) if (SPP) has a unique optimal solution and it is non-degenerate, . The general position gap is the smallest positive basic value,
The exhaustive resolving policy with inter-action delay acts only at the epochs . There it performs an optimal solution of the integer program with the redundant matches removed, and then discards the leftover agents of the under-demanded types.
There are constants depending only on such that, under GP, the exhaustive resolving policy with (any tie-breaking) is admissible and
The constants are not fixed, so the goal survives any improvement of them.
Here is the -weighted leftover in after an optimal integer matching of (display (7)).
The upper bound says that, under GP, hindsight-optimal performance up to an additive constant is achievable at every time simultaneously, not just at a known horizon. Long-run average optimality and near-optimality under discounting follow (Remark 2.1). The bound also quantifies the cost of acting often: the delay and the regret both scale with , so networks close to degeneracy force batching. Combined with the paper's lower bound, is the right order on non-trivial networks.
The result has a printed proof (§4, Appendices B and D) but no machine-checked one. Several intermediate statements of the printed proof do not hold as stated and are not posed here. The goal and the stated displays (11) and App. D are posed as the paper states them, so a formal proof requires a correct argument for the uniform-in- bound on the over-demanded queues. Lemma 4.1, the basis and duality facts and Lemma 4.2 are self-contained and checkable on their own.
The obvious approach compares the policy's realized matches with the fluid optimum and controls the deviation with concentration bounds. That gives errors of order , not a constant. The constant comes from showing that the over-demanded queues stay of order uniformly in time and in . Between epochs these queues behave like a multidimensional reflected random walk whose drift toward zero is only of order , while its fluctuations over an epoch are of order . The delay balances the two, but the queue state enters through the integer program (3), whose solution changes discontinuously with the queues, and the quantities that measure the drift are signed combinations of arrival counts, to which the usual one-sided concentration bounds for nonnegative sums do not apply. On top of this every constant must be independent of .
Fin n and matches Fin d (0-based); the topology with its two standing assumptions (, every type in a match) is a structure, and with and are hypotheses.Fin n. Expectations at horizon are finite sums over the first arrivals weighted by , so no expectation is a default value.Contributions welcome: proofs of the LP facts (milestones 2–3) and Lemma 4.1, a Mathlib-ready proof of Lemma 4.2, and any correct argument for the epoch bounds.
Online marketplaces depend on consumer reviews, and a single negative review can move a seller's future sales. Review blackmail exploits this: a consumer buys a product, posts a negative review, and offers to remove it in exchange for a payment. Platforms such as Amazon, eBay, Taobao and TripAdvisor respond with dispute resolution mechanisms that let sellers contest reviews. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) build a game-theoretic model of the seller, the blackmailer and the market's belief about product quality, and ask how the design of such a mechanism changes the blackmailer's leverage. Their first finding concerns a centralized mechanism, where the seller reports the review and the platform judges it: making the platform faster or more accurate does not always lower the ransom the blackmailer can extract. This mission formalizes that result together with the equilibrium analysis it rests on.
A monopolist sells a product of unobservable quality ; the market's prior that quality is high is . A buyer of a high-quality product has gross utility with probability and otherwise, with standard uniform; a low-quality product always gives . One consumer arrives.
The market sees the review , updates its belief to a posterior by Bayes' rule, and the seller then earns a continuation payoff , with nonnegative, convex and strictly increasing on .
Facing a ransom demand the seller can settle (: pay , the review disappears), do nothing (: the review stays), or report () the review to the platform's centralized mechanism at a hassle cost . The platform investigates immediately with probability (timeliness) and identifies a malicious review correctly with probability (accuracy); the review is removed with probability , the mechanism efficiency.
The market cannot observe the seller's interaction with the blackmailer. It holds a belief about the seller's response, and this belief determines the posteriors: under belief a malicious review stays visible with probability , or , and is the Bayes posterior computed from the resulting review likelihoods. When the market believes and the seller plays , his payoff is (), (), or (). A response is an equilibrium if it is a best response to the belief ; among several equilibria, the seller-preferred one prevails. The malicious consumer buys iff some ransom is accepted in the prevailing equilibrium, and the equilibrium ransom is the greatest ransom at which settling prevails.
If and , there are efficiencies at both of which the malicious consumer purchases, with
The equilibrium ransom is not monotonically decreasing in the efficiency .
and the malicious consumer purchases iff .
Corollary 1 is the paper's headline message about centralized dispute resolution: improving the mechanism's timeliness or accuracy can raise the ransom. Below an efficiency threshold the mechanism is never used and the ransom equals the seller's loss from a visible negative review; just above it, the market expects the seller to report blackmail, which softens how it reads a negative review, and the blackmailer can ask for more. This is the motivation for the paper's second design, semi-decentralized dispute resolution, analysed in a companion mission. Proposition 2 is the complete characterization of the blackmailer's equilibrium behaviour under the centralized mechanism and is used again in the paper's pricing analysis (§4.4).
The results are proved in the paper (Appendix C). No machine-checked version exists. This mission produces Lean statements of the model, of the Bayes posteriors, of the equilibrium conditions, of the seller-preferred selection and of the ransom characterization, all derived from the primitive game rather than from the paper's closed forms.
Each step is elementary, but the chain is long and sign-sensitive. The equilibrium conditions require handling a belief-dependent payoff (the posterior depends on what the market believes, not on what the seller does), so a deviation changes the action without changing the posteriors. The ransom characterization needs a three-way comparison of equilibria and the tie-breaking in favour of settling at the boundary, where two equilibria give the same payoff. The corollary needs the jump at the threshold efficiency to be strictly positive and to survive a small increase of the efficiency: the posterior moves with the efficiency, so a continuity argument for composed with the posterior is required, and is only assumed convex and strictly increasing on . The natural first idea, comparing the two closed forms of Proposition 2 at a single point, does not suffice, since at the threshold itself the two regimes coincide in value.
Model with fields and ; inductive types for quality, reviews (, Z for , ) and responses. The posterior post m R is Bayes' rule over the likelihood table with visibility probability of a malicious review; is post (keep (γ*δ) i) R.Standing): ; , convex and strictly increasing on ; ; and . The last is implicit in the paper: it makes the purchase probability that of a standard uniform valuation and keeps the event of positive probability. Every theorem also assumes .IsGreatest of the set of ransoms at which settling prevails; purchase means some such ransom exceeds . "Not monotonically decreasing" means not nonincreasing.ConvexOn, StrictMonoOn, IsGreatest). Proofs of the milestones in order, and reusable lemmas on the monotonicity of the posterior in the visibility probability, are welcome.Online marketplaces rely on consumer reviews, and a negative review lowers what future buyers believe about a product. Review blackmail exploits this: a consumer buys, posts a negative review, and offers to remove it for a ransom. Platforms counter with dispute-resolution mechanisms. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) compare two of them in a Bayesian game between a seller, one consumer and the market. Under the centralized mechanism the seller reports the review and the platform decides whether to remove it. Under the semi-decentralized mechanism the seller removes the review himself, and the platform checks afterwards. If it judges the removal wrongful, it reinstates the review and fines the seller a penalty .
This mission covers the semi-decentralized mechanism. Its main result, Proposition 5, gives the ransom a blackmailer can extract in equilibrium in closed form and says when blackmail pays at all. A platform needs that answer when it chooses the penalty. Mission I of this series treats the centralized mechanism.
A product has quality . The prior that is . A buyer of a high-quality product gets a positive experience with probability ; a low-quality product never gives one. With probability the consumer is malicious. A malicious consumer buys at price , posts a negative review and demands a ransom . Otherwise the consumer is regular. A regular consumer buys with probability (valuation uniform on ) and reviews truthfully: positive () or negative (). No purchase means no review, written ; a removed review is also seen as .
The market observes and forms the posterior by Bayes' rule. The seller then earns , where is nonnegative, convex and strictly increasing on .
Facing a ransom demand, the seller can settle (: pay , review removed), do nothing (), or use the mechanism (). Under the platform judges immediately with probability (timeliness). It recognises a malicious review with probability (accuracy). The review is therefore reinstated with probability , and the penalty is paid with probability . Write for the posterior after review when the market believes the seller's response is . The payoffs of the three responses are then
The market cannot see the interaction, so is an equilibrium at if no response pays more given the belief . The equilibrium ransom is the largest at which settling is an equilibrium and no equilibrium pays the seller more. The malicious consumer buys iff .
A seller could also use the mechanism against genuine negative reviews. Proposition 4 shows that this is deterred exactly when .
Let and .
Proposition 5 has two regimes. If the penalty is high, the mechanism plays no part in blackmail: the seller would never use it, and the ransom equals the one with no mechanism at all. Below the threshold, the ransom is the seller's expected loss from using the mechanism. A lower ransom then means less blackmail, and it pushes the price at which blackmail stops paying downward. The threshold rises with the accuracy and falls with the timeliness . The paper's later results on pricing and on the platform's penalty build on this characterization.
The result is proved in the paper (Appendix C, pp. 41–43). It has no machine-checked proof. Formalizing it pins down the equilibrium concept, including the selection among multiple equilibria. It also corrects a printed slip in the proof: the simplified condition for the mechanism to be an equilibrium drops a factor .
Each individual equilibrium condition is a rearrangement of payoff inequalities. The difficulty lies in selecting among equilibria. Several responses can be equilibria at the same ransom. Settling prevails only if no other equilibrium pays more, and the equilibria themselves depend on . So the set of ransoms at which settling prevails is not given by one inequality. Its greatest element must be found across three scenarios, comparing three thresholds that involve three different posteriors. Those comparisons require the posterior ordering , which comes from Bayes' rule and not from the payoff algebra. Reading the equilibrium condition for alone as the answer gives the wrong ransom in case 1.
Everything lives in the namespace ReviewBlackmail.SemiDec, with one structure Model holding and the payoff fut (the paper's ; Real.pi is never used). The predicate Standing collects the standing assumptions: ; nonnegative, convex and strictly increasing on ; ; ; and the disclosed addition , which makes the purchase probability lie in . Per-statement additions, each disclosed in the item:
Posteriors are defined by Bayes' rule over an explicit likelihood table with two visibility probabilities: for malicious and for genuine negative reviews. Proposition 4 needs beliefs in which genuine reviews are removed. The payoffs of Proposition 5 keep genuine reviews (), the case the paper reduces to via Proposition 4. Ties in the selection rule go to settling.
The posteriors are never defined by their closed forms, and is never defined by (6) or (7). The goal is stated with IsGreatest on the set of ransoms at which settling prevails, not with sSup, so neither the closed forms nor junk values of a supremum can make the goal trivial.
A complete development needs only Mathlib's ConvexOn, StrictMonoOn and IsGreatest and real-field algebra. The algebra of Bayes posteriors with two-point priors may be reusable. Proofs of the milestones and the goal are welcome, in any order.
Young innovative firms often fund research out of internal cash flow rather than external capital. Whether such financial constraints make firms invest less in research and development (R&D) is a long-standing question in corporate finance and the economics of innovation. Myers (1977) showed that the possibility of default leads to under-investment in growth options. Danmo Lin (Management Science, 2022) separates two ways in which spending more on a project can pay off: it can make the payoff larger (scalability) or make the discovery arrive sooner (accelerability). The paper's Corollary 1 says that the classical under-investment result holds exactly when the project is scalable but not accelerable, while acceleration can reverse it. This mission formalizes the under-investment half of that corollary.
A firm faces a one-time R&D opportunity. It chooses an investment intensity , a spending rate per unit of time, and pays it until discovery. Discovery is the first arrival of a Poisson process of rate , and on discovery the firm receives a payoff with mean . As in the paper's equation (2),
and intensities are at least . The project is scalable if (here ) and accelerable if (here ). Future cash is discounted at rate .
An unconstrained (UC) firm can always pay . By the paper's Lemma 1, equation (5), its project value at intensity is the perpetuity
A financially constrained (FC) firm pays out of an asset-in-place (AIP) cash flow , a geometric Brownian motion with drift and volatility that starts at . It must abandon the project once . Lemma 1, equation (6), gives its project value as
The ranges of intensities are those of (7): for the UC firm and for the FC firm, with . The optimal intensities and are the sets of maximizers of and over these ranges.
If and , then . Formally: under the standing assumptions, , , , , and , both optimal sets are nonempty and
The statement pins down when the textbook under-investment effect of financing frictions holds: exactly when extra spending scales the prize but cannot speed it up. The paper contrasts it with the possibility of over-investment on accelerable projects (Corollary 1's second statement, supported by numerical exercises). Taken together, the two statements show that the R&D technology, not only the severity of the constraint, decides the direction of the distortion.
The result is proved in the paper (Appendix A.4); it has no machine-checked proof. A formal proof certifies the comparison for every pair of optima, without the paper's tacit assumption that optima are unique. It also makes explicit the interior-optimum condition under which the inequality is strict. The resulting facts about maximizers of products of a concave power-law profit and a decreasing survival factor are reusable for other real-options models with a survival discount.
The first idea is to compare the two first-order conditions. The UC optimum solves , and at an interior FC optimum the derivative of the survival factor pushes to be positive. Concavity of then orders the two. Turning this into a theorem about sets of maximizers needs more. The FC optimum can sit at a corner, either or the right end , where no first-order condition holds, and the corners must be ruled out or handled separately. The survival factor vanishes at . The UC value vanishes at . When , the comparison is settled by the range rather than by the first-order condition. The strict inequality is false without an interior UC optimum: if , both optimal sets equal .
All objects are in the namespace AccelScal.FCMonopoly, in one definition file. It holds the parameter structure Tech , the predicate Standing, , , , , (5), (6), and the maximizer sets RstarUC, RstarFC over the ranges (7). Powers are Real.rpow, and is Mathlib's deriv.
Committed conventions:
Trivializing formalizations are ruled out. is never defined by its closed form, and neither optimum is a selected value. The goal asserts that both optimal sets are nonempty. The FC range depends on through . The conclusion is the strict "", not "".
The paper's second and third statements of Corollary 1 (over-investment when , and when it is "more likely") are numerical or informal and are not posed. Contributions are welcome on both milestones and on the goal. Also welcome: general lemmas on the maximizers of a positive concave function times a decreasing positive factor, and a future formalization of Lemma 1 (6) from a geometric Brownian first-passage Laplace transform.
Firms that serve several customers from shared capacity must decide which demands to fulfil after demand is observed. A customer-level service commitment constrains the allocation policy even when total capacity appears adequate: serving one customer can consume resources that another customer needs. The question in this mission is how to test a fixed capacity vector against all individual service targets without first specifying a particular rationing rule. Jiang, Wang, and Zhang give a characterization for a broad family of pooled-resource models, including inventory pooling, process flexibility, and assemble-to-order systems (SSRN preprint, §§1.1–2).
The authors' model allows service to mean more than the probability of completely filling an order. It can represent the probability of full service, a fulfilled fraction relative to expected demand, or a fulfilled fraction of realized demand. Their Theorem 1 addresses asymptotic feasibility: every target can be met to within any prescribed positive tolerance. It is distinct from exact feasibility, which the paper treats later under stronger conditions (Jiang, Wang, and Zhang, Theorems 1–2).
There are customers and resource types. A nonnegative capacity vector is fixed before a random, nonnegative demand vector is observed. The joint law of is and has a bounded second moment. After seeing , a decision consists of a vector of fulfilled customer demands and an allocation array recording the amount of each resource assigned to each customer. The paper's set specifies all feasible pairs for that capacity and demand. It is a model input: the three operational examples use different feasible sets (§1.1, equations (1)–(4)).
For customer , a service measure assigns a nonnegative score to fulfilled demand and demand . The customer has a target . A deterministic policy chooses a feasible pair in for each . A randomized policy chooses among deterministic policies. Its expected service to customer is denoted . The capacity is asymptotically feasible when, for every , some randomized policy satisfies for every customer (Definition 1, equation (8)).
For nonnegative customer weights , define maximum weighted service at a realized demand by
The maximum uses only service, with zero allocation cost. The paper also introduces a linear allocation cost , a deterministic Max-Weighted-Service minimization problem, and its expected dual functional; Lemma 1 concerns those general objects (§2, equations (14), (16)–(17)).
Under Assumption 1, the target is the equivalence
The weights range over the whole nonnegative orthant; they are not restricted to a simplex in the theorem. Assumption 1 requires each to be nondecreasing and upper semicontinuous in fulfilled demand at fixed realized demand, and each to be compact (Theorem 1, equation (18)).
Lemma 1 identifies the value of the pointwise Max-Weighted-Service rule: for a fixed . The proof of Theorem 1 then uses a minimax display over to obtain, for every , a randomized policy whose weighted service shortfall is at most throughout (equation (21)). Equation (22) gives the corresponding individual service bounds. These three source claims are the mission's milestones (Lemma 1 and proof of Theorem 1, pp. 12–14).
Theorem 1 supplies a test for a vector of simultaneous service targets using a family of deterministic, weighted allocation problems. It applies to any feasible-set model satisfying the stated assumptions, rather than only to one pooling network. It also delineates the strength of the conclusion: satisfying all weighted tests guarantees arbitrarily close service, while exact attainment requires the additional assumptions in the paper's next result (Theorems 1–2).
The statements in this mission compile as Lean declarations, but their proofs have not yet been machine checked. Completing the mission would provide a reusable formal interface for demand-dependent feasible sets, measurable rationing policies, finite policy randomization, service expectations, and pointwise weighted optimization. Those definitions can also support formal study of the paper's later exact-feasibility and policy-optimality results.
The forward implication compares service under one policy with a maximum over feasible decisions at every demand. The reverse implication is harder: a weighted inequality for each must yield one policy that serves all customers simultaneously to a common tolerance. A separate policy chosen for each weight does not itself meet the vector of targets. The optimization involves a set of demand-dependent policies, and the source's argument relies on properties of its attainable service vectors that need explicit representation in Lean (proof of Theorem 1, pp. 13–14).
Customers and resources are Fin n and Fin m, with zero-based indices; the paper numbers them from one. A solution is a pair , and remains an arbitrary feasible set. Deterministic policies are measurable functions of that select from for every demand realization, at the theorem's fixed capacity. Randomized policies are finite probability mixtures of these selectors. Only finitely many expected services and costs occur in the statements, and finite mixtures represent the corresponding finite-dimensional expectation vectors of the paper's policy measures. The definition of asymptotic feasibility is made directly from these policies and their service values. The maximum in the theorem is made directly from and , so the equivalence cannot follow from defining either side in terms of the other.
The paper defines on nonnegative pairs. Lean uses a total real-valued extension; the theorem requires it to be nonnegative, monotone and upper semicontinuous as specified, and jointly measurable. A common integrable envelope bounds every feasible service value, preventing a nonintegrable Bochner integral from silently taking Lean's default value of zero. A measurable maximizing selector is assumed for every nonnegative ; it ensures that the expectation of and the policy behind the source's tie-breaking are meaningful. The demand law is a probability measure with bounded second moment and nonnegative demand, capacity is nonnegative, and , matching the section's standing setup. Compactness alone permits an empty feasible set in Lean; the selector assumption ensures nonemptiness at each demand.
The definitions include the linear allocation-cost functional because Lemma 1 is stated with the paper's general . An integrable envelope also bounds its absolute value in that milestone. Reusable work includes measurable selection for a demand-dependent compact feasible set, integrability of finite policy mixtures, interchange of the pointwise optimum and expectation under the stated bounds, and the finite-dimensional minimax statement. Proofs or improvements to these interfaces are welcome as long as the source claims retain their stated strength.
Graph alignment asks for the correspondence between the vertex sets of two graphs that are noisy copies of each other. It underlies the de-anonymisation of social networks, where an anonymised graph is matched to a public one (Narayanan, Shmatikov 2009), the comparison of protein–protein interaction networks across species, and matching problems in computer vision. The standard random model for studying when alignment is possible is the correlated Erdős–Rényi model (Pedarsani, Grossglauser 2011).
In that model, exact recovery of the hidden correspondence and almost exact recovery (all but a vanishing fraction of vertices) have sharp thresholds: exact recovery by Cullina, Kiyavash 2016 and 2017; almost exact recovery when by Cullina, Kiyavash, Mittal and Poor (arXiv:1809.03553). Hall and Massoulié (arXiv:2007.00533v5, Operations Research 2023) study partial recovery, the recovery of a constant fraction of the correspondence, in the sparse regime , where almost exact recovery is impossible. This mission formalizes their possibility result, Theorem 2.3. Its companion mission (Partial Recovery in the Graph Alignment Problem I) formalizes the impossibility result, Theorem 2.1.
Fix and parameters with . A parent graph on includes each edge independently with probability . Two copies are made, and each copy keeps every edge independently with probability . The resulting graphs and have adjacency matrices and . For each unordered pair of distinct vertices, has the law of display (3):
independently over the pairs. The covariance of and is (display (2)), which is positive when .
A planted permutation relabels into the observed graph : . An algorithm sees and returns a permutation . Its quality is the overlap
For , a permutation is good (Definition 2) if at least vertices have degree at least in the intersection of with relabelled by :
In Lean, these objects are pLaw, Config, cfgProb, prob, A, B', B, overlap, good and Cond6 in GraphAlignment.Possible.
Let and let , be sequences. Suppose there exist such that, for all large ,
Then some algorithm returns with
The result. Theorem 2.3 shows that partial alignment is information-theoretically achievable in the sparse regime , provided is above an explicit constant depending on . Together with Theorem 2.1, it locates partial recovery between a necessary condition stated through the divergence and a sufficient condition stated through . It complements the almost-exact-recovery results for , which do not apply when stays bounded. The moment generating function computation of Lemma B.2 and the inequality of Lemma B.1 were reused for the sharp exact-recovery threshold by Wu, Xu, Yu (p. 9 of the source).
Formalizing it. The theorem is proved on paper; no part of it is machine-checked. The paper's route to Proposition 4.2 applies a -core theorem for with fixed and an integer, at and , which vary with and need not be integers. The statement of Proposition 4.2 remains true, but a formal proof needs a different argument. Proposition 4.4's union bound contains two repairable gaps: an infimum taken over instead of , and the bound . A formal development would settle the theorem under exactly the conditions (6).
The natural first step is to compute for a fixed wrong permutation and take a union bound over all permutations. The difficulty is that for the terms are not independent: an edge variable enters several terms along the cycles that induces on vertex pairs. A Chernoff bound therefore needs the moment generating function of a sum over each cycle of pairs. That is a transfer-matrix computation, and the per-cycle bounds must then be recombined uniformly in the cycle lengths. The resulting exponent must beat . This is where the sparsity conditions and , and the constant , enter. Proposition 4.2 is a concentration statement for the number of vertices of degree at least in the intersection graph, an Erdős–Rényi graph , when is only a large constant.
Everything is finite. Vertices are Fin n and permutations are Equiv.Perm (Fin n). A configuration assigns Bool × Bool to each non-diagonal element of Sym2 (Fin n), and probabilities are finite sums of the product weights. They are not taken against a free measure, so the model is a genuine probability space whenever . The standing assumptions for every (p. 5 and the running assumption on p. 7) are hypotheses of the asymptotic statements. The paper's remark "we assume " (p. 6) is used by neither result and is not imposed. Logarithms are natural, "" is a limit along , and the thresholds and are real numbers, not floored.
In the goal, an algorithm is a family of maps from the observed pair to a permutation. It is chosen before the planted permutations and may depend on , , , , but never on . This rules out the trivial algorithm "output ". The theorem does not say how is drawn, so the limit is required for every sequence of planted permutations, which covers the uniform case. "Exponential time" is not formalized.
Three statements are posed in a corrected reading, each disclosed in its Formalization Note. In Lemma 4.3, and : the paper allows and , where and (13) are undefined, and Lean's convention would make the bound trivial. Display (10) is stated for an arbitrary permutation . Only the "in particular" clause of Lemma A.2 is stated, because the paper's proof of the general normal-approximation bound does not hold as written. Lemma 4.1 (a -core theorem of Pittel, Spencer and Wormald) is not posed.
A complete development needs: Chernoff bounds for finite sums of dependent Bernoulli variables via the transfer-matrix formula, binomial and Poisson tail estimates, and the cycle decomposition of the action of a permutation on unordered pairs. Lemmas B.1, B.3 and 4.3 are general-purpose and reusable. Proofs of any milestone, and alternative proofs of Proposition 4.2 that avoid -cores, are welcome.
The source is the arXiv preprint v5, whose appendices contain the proofs that the main text defers to an electronic companion.
The quantum approximate optimization algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028, 2014) is a family of shallow quantum circuits, indexed by an integer depth , that prepare states whose computational-basis measurements are biased toward good solutions of a combinatorial optimization problem. It became the standard candidate for optimization on near-term quantum hardware, and its performance on MaxCut is the benchmark against which later analyses and experiments are measured.
The original paper proves one concrete performance guarantee: at depth , on 3-regular graphs, the algorithm achieves an approximation ratio of at least . Short timeline:
A graph has vertex set , and 3-regular means every vertex has exactly three neighbours. Each vertex carries a qubit; a computational basis state is a bit string . For an edge the clause is if and otherwise, and the cut objective is
the number of edges cut by the bipartition defines. As an operator, is diagonal in the computational basis.
Let and let . For angles , the depth-one QAOA state and its expected cut are
The angles may be restricted to , by periodicity.
Two kinds of small subgraphs govern the analysis. A crossed square is a set of four vertices spanning exactly five edges (a 4-cycle with one diagonal). An isolated triangle is a triangle whose three outgoing edges end on three distinct vertices. and denote their numbers in . Finally, for an edge the subgraph type is the shape of the edge together with its adjacent edges; in a 3-regular graph there are three types , according as and have two, one or no common neighbours. Each type defines a function , the expectation of the clause of the central edge in the depth-one QAOA state of the subgraph alone.
For every connected 3-regular graph there are angles , with
that is, . The constant is exactly the paper's , and is included.
The paper's argument passes through the following claims, each a milestone:
The result is the first rigorous worst-case guarantee for the QAOA, and the method behind it (the expected objective is a sum of local terms, each depending only on a bounded neighbourhood of an edge) is the template for every later analysis of fixed-depth QAOA on bounded-degree graphs. It shows that a depth-one circuit, of depth independent of , achieves a constant approximation ratio uniformly over an infinite class of graphs.
The paper's proof is complete apart from one numerical step: the minimization of (35) is reported as a numerical evaluation. No machine-checked version of the result exists. A formal proof requires an exact evaluation of the three subgraph functions at suitable angles, an exact combinatorial count of edge types, and a certified inequality in place of the numerical minimization. The margin is small: the exact minimum is , about above the paper's constant.
The light-cone reduction (milestone 1) is the conceptual step: one must show that conjugating a two-qubit clause by and leaves an operator that involves only the qubits adjacent to the edge, and that the remaining qubits contribute a factor of one. In matrix form on -dimensional space this is a statement about tensor-product structure that the definitions do not make visible. The combinatorial count (milestones 2–4) needs a careful case analysis of how triangles sit in a cubic graph, including the exceptional graph , where the count fails. The final inequality (milestone 6) has a margin of order , so crude bounds on the trigonometric functions do not suffice.
Qubits n = Fin n → Bool from the published QAlgorithms layer, with true the bit . States are vectors in EuclideanSpace ℂ (Qubits n); , as a diagonal operator, and the QAOA unitary are the published definitions uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary. The latter takes mixer angles before phase angles.SimpleGraph (Fin n) with decidable adjacency; "3-regular" is IsRegularOfDegree 3. The cut counts each edge once. is defined as , which equals because is diagonal. The constant is the exact rational .In the classical secretary problem, candidates arrive one at a time in random order; at each arrival the decision maker sees only how the current candidate compares with the earlier ones, and must irrevocably hire or pass. The goal is to hire the best candidate, and the optimal rule (wait for about arrivals, then take the first candidate better than all before) succeeds with probability about .
In many applications the decision maker also receives advice about each candidate: a noisy score, a prediction from a machine-learned classifier, or samples from the same distribution. Dütting, Lattanzi, Paes Leme and Vassilvitskii (arXiv:2011.06726, Mathematics of Operations Research, 2024) propose a single model covering these cases: each secretary carries a signal, ranks and signals have an arbitrary known joint distribution, and the question is which policies are optimal. Their first structural result says that, under two natural conditions on the distribution, the optimal policy can ignore almost all of the history: it needs only the current signal and whether the current secretary is the best so far. Such memoryless policies are simpler, store less, and are relevant where data retention is restricted.
Timeline. Dynkin (1963) gave the rule for the advice-free problem. Gilbert and Mosteller (1966) studied the full-information version, where the advice is the candidate's value drawn from a known distribution. Buchbinder, Jain and Singh (2014) wrote secretary problems as linear programs. Dütting et al. (arXiv 2020) extended this LP to general advice and proved Theorem 8, the result of this mission.
There are secretaries, arriving in the order , and a finite signal space . An outcome consists of ranks (ties allowed) and signals . A signaling structure is a known probability distribution over outcomes such that, almost surely, some secretary has the top rank .
At round the algorithm sees the information : the relative order of the first arrivals and their signals, not the ranks themselves. A policy assigns to every round and every information value a stopping probability in . The policy stops at with probability , and its winning probability is the probability that it stops at some with .
The best-so-far event is . A policy is memoryless if its stopping probability at round depends only on , on whether holds, and on .
Two properties of are assumed. Non-Filtering (NF): for , the conditional law of given is unchanged by additionally conditioning on . History-Irrelevance (HI): conditioned on , the information at round is independent of the event .
For , and let and . The LP of §3 has variables , constraint
and objective (5).
If satisfies NF and HI, then there is a memoryless policy with
Theorem 8 reduces the search for an optimal policy from functions of the entire history, whose number grows exponentially in , to numbers, and with Propositions 9 and 10 it turns the problem into a linear program of polynomial size. The later sections of the paper build on it: threshold policies (§4), secretaries with samples (§5) and binary-classifier advice (§6) are all analysed through this LP. The examples satisfying NF and HI include the classical problem, the full-information problem, samples, and noisy classifier advice.
The paper gives a complete proof. As far as is known, none of it has been machine-checked, and Prove2Me has no formal model of secretary problems with advice. A formal development makes precise the parts the paper's argument leaves informal: the handling of conditioning on null events, of randomized policies, and of the existence of an optimum.
The obvious argument replaces a general policy by its conditional stopping probability given . This fails directly: the probability of reaching round depends on the whole history, so averaging the decision at round changes the distribution of the earlier stopping events, and the winning probability with it. The paper therefore goes through the LP. The variables summarize a policy, NF is what makes constraint (4) depend only on the distribution and not on the policy, and HI is what makes the objective linear in . The reverse direction, Proposition 10, rebuilds a policy from through an induction over rounds in which the survival probability must be tracked exactly.
Fin n, 0-based: Lean secretary is the paper's , and Lean rank is the paper's top rank . The signal space is a finite type, so every probability is a finite sum. Continuous signals (the paper's Example 2, ) and the non-NF Example 11 are out of scope. Ties are allowed, as in §2.Memoryless predicate that allowed dependence on the whole information, or a winning probability without the survival product, would make the goal empty. Neither is used here: a memoryless policy is a function of only, and the winning probability includes .prob, expectOn, cross-multiplied conditioning) and the identity are reusable well beyond this mission. Proving the milestones in the order listed follows the paper's proof. The running time of the LP and the paper's plots are out of scope.Ranking and selection asks which of simulated alternatives has the largest mean, when each simulation run returns one noisy sample and the simulation budget is limited. A large literature allocates the budget using the large-deviations analysis of Glynn and Juneja (2004): for a static allocation in which alternative receives a fixed fraction of the samples, the probability of incorrect selection decays exponentially, and the allocation that maximizes the decay rate is characterized by a system of nonlinear optimality conditions. Those conditions depend on the unknown means, so practical procedures plug in estimates and solve the system repeatedly, which is costly and comes with few guarantees.
Chen and Ryzhov (Proc. 2019 Winter Simulation Conference) propose Balancing Optimal Large Deviations (BOLD), a sequential rule that never solves the optimality conditions: at each step it evaluates the two sides of one condition at plug-in estimates and samples whichever alternative appears to be falling behind. It has no tuning parameters and applies to any sampling distribution whose rate function can be evaluated. The paper states that BOLD learns the optimality conditions with probability 1; the full proofs are in the companion article (Chen and Ryzhov, Management Science, 2023).
There are alternatives with distinct means ; the best is . Alternative produces independent samples from a law with mean , a member of a distributional family indexed by its mean . The families may differ between alternatives.
The rate function of the member with mean is the Fenchel–Legendre transform of its log-moment generating function,
with values in , and . For a normal law with variance , .
An allocation chooses alternative at stage . Write for the number of samples of among stages and for their mean (an arbitrary while ). The plug-in rate is , likewise . For , is the solution of
and (11).
BOLD (Figure 1 of the paper): let be the leader, an alternative with the largest . If the leader is not unique, sample the tied leader with the fewest samples. Otherwise sample the leader if
and if not, sample the minimizing (13). Remaining ties are broken arbitrarily.
Under Assumptions 1–4 of the paper, with probability 1,
These are the plug-in forms of the total balance condition (5) and the individual balance conditions (6), which together characterize the optimal static allocation. The paper states them as Theorems 3 and 4; the goal is their conjunction.
The result. Convergence of BOLD to the optimality conditions shows that the static optimum of Glynn and Juneja can be learned by a cheap sequential rule without knowing the proportion of the budget the best alternative should receive. Top-two methods require that proportion as an input. The paper claims the guarantee for any sampling distributions satisfying four regularity assumptions, not only normal ones. As the paper notes, convergence to the static optimum does not by itself transfer the static exponential rate to the adaptive procedure; the result concerns learning the conditions.
The formalization. The WSC paper gives proof outlines only, and the complete argument lives in a long journal article. No part of it has been machine-checked. A formal proof would check a strong-law argument for an adaptive procedure with two interleaved decision criteria and would yield a reusable formal model of sequential sampling for ranking and selection with general rate functions.
The obvious argument is "sample means converge, hence the plug-in conditions converge". It fails because the sample means converge only if every alternative is sampled infinitely often, and BOLD gives no forced exploration: an alternative is sampled only when (12) or (13) selects it. Consistency must therefore come from the structure of the rule itself. Even with consistency, the limits in Theorems 3–4 are not continuity statements: the plug-in quantities depend on the sample sizes as well as the sample means, and they oscillate around the level 1 as (12) alternately holds and fails, so convergence requires quantitative control of how long the rule can neglect any one alternative. Discrete sampling laws add ties among sample means and a sample mean that can coincide with another alternative's true mean (Assumption 3).
Fin M with 2 < M (indexed from 0). The family is Fam : Fin M → ℝ → Measure ℝ of probability measures, with true law Fam x (μ x). Samples form an observation array W x k (the -th sample of ), mutually independent, with W x k ∼ Fam x (μ x); this gives the same law of the sample path as the paper's sequential sampling.BellWilliams2001.ThresholdPolicy.LargeDeviation, so is a genuine value. is the derivative of its real part. Conditions on are imposed on the effective domain , where is finite nearby.IsBOLD on allocation sequences, so every tie-breaking rule is covered. The initial means are arbitrary. The solution of (10) is a chosen solution between the two sample means; its uniqueness is the paper's claim, not a hypothesis.The development needs strong laws of large numbers along adaptively chosen sample counts, properties of Legendre transforms of log-moment generating functions (convexity, a unique zero at the mean), and law-of-the-iterated-logarithm-type rates for sample means. Lemmas on Legendre transforms of log-MGFs and the observation-array model are reusable for other large-deviations allocation rules. Contributions toward any milestone are welcome. Statements specialized to normal families are not substitutes for the general milestones.
Bayesian persuasion studies a sender who observes a state of the world and commits in advance to a randomized disclosure rule, in order to influence the action of a receiver who updates her belief by Bayes' rule. Since Kamenica and Gentzkow (2011) the model has been applied to platform design, recommendation systems, queue information and rating systems. Almost all of this theory assumes the receiver is an expected-utility maximizer, so that her payoff from each action is linear in her belief.
Many receivers are not. A customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold has a utility that is nonlinear in her belief. Anunrojwong, Iyer and Lingenbrink (2023) call such receivers risk-conscious and show that, for them, the standard revelation-principle reduction to action recommendations fails. Their first main result replaces it with a convex program over the joint distribution of state and action. This mission formalizes that result and the lemmas leading to it.
Let be a finite set of states and the simplex of beliefs, with the Euclidean topology. Sender and receiver share a prior . The receiver chooses an action from a finite nonempty set . Her utility is an arbitrary function ; the sender's utility is .
For each action , the beliefs at which is optimal for the receiver form the set
The paper assumes throughout (Assumption 1) that every is closed.
A signaling scheme consists of a measurable signal space and a probability measure on whose -marginal is . After signal the receiver holds the posterior given by Bayes' rule, and plays an optimal strategy , with , that is . The sender's persuasion problem (3) is to maximize over signal spaces, schemes and optimal receiver strategies; when the receiver is indifferent, the sender picks the strategy she prefers.
A probability measure on is Bayes-plausible if its mean is the prior: .
The sender's problem (3) can be optimized by solving the convex program
It is formalized as an equality of sets: the values achievable in (3) are exactly the objective values of feasible points of (7). This says that every scheme yields a feasible point of (7) with the same value, and every feasible point is realized by a scheme. In particular the supremum of (3) equals the maximum of (7), and an optimal solution of (7) gives an optimal scheme.
Let be the states at which is sender-optimal, assume these sets partition , and set . Then the sender can fully persuade the receiver (almost surely, the receiver takes a sender-optimal action) if and only if is feasible for (7), i.e. for all .
The result. Problem (3) optimizes over arbitrary signal spaces and joint distributions, so it is not finite-dimensional. Program (7) has vector variables in , each in a convex set that depends only on the receiver's utility. Its variable is the joint probability of state and action . The program gives the paper's bound on the number of signals needed (Proposition 1), its characterization of when persuasion helps (Proposition 2), the full-persuasion criterion (Theorem 2) and, after replacing by a polytope, the linear program for binary persuasion (Theorem 3, the companion mission). For expected-utility receivers each is convex, and (7) reduces to the familiar obedience-constrained linear program.
Formalizing it. The results are proved in the paper; none is formalized. A formal development fixes what "can be optimized by solving" means as a set equality and handles general measurable signal spaces with posteriors defined only almost everywhere. It also exposes two places where the printed lemmas need correction (see the scope section).
The usual revelation-principle shortcut would merge all signals that lead to the same action. For a risk-conscious receiver this can change the response: averaging posteriors in can produce a belief outside , since need not be convex. The central geometric difficulty is relating a distribution of posteriors supported on a closed, potentially nonconvex to a finite-dimensional variable in . The converse must preserve both Bayes plausibility and receiver optimality. With general signal spaces, the posterior is determined only almost everywhere, while the stated strategy condition applies at every signal.
Fintypes, nonempty, and carries a measurable space in which singletons are measurable. Beliefs are functions in stdSimplex ℝ Ω, Belief Ω is the simplex as a subtype, is convexHull ℝ, and is the zero function. is a function on , used only on the simplex.Convex.integral_mem, compactness of convex hulls of compact sets), Carathéodory's theorem (convexHull_eq_union), finite discrete measures on , and conditional densities with respect to the signal marginal. The Bayes-plausibility and splitting lemmas are reusable in any persuasion development. Proofs of the milestones, of the goal, and of Theorem 2 are all welcome.Ride-hailing platforms such as Uber and Lyft match riders with self-scheduling drivers who decide for themselves whether to work. Two features make capacity planning on such a platform different from classical fleet management. Demand is spatially imbalanced: more trips start in some locations than end there, so cars accumulate where they are not needed unless they drive back empty. And capacity is endogenous: the number of participating drivers depends on what drivers expect to earn, which in turn depends on how the platform uses them.
Afèche, Liu and Maglaras (MSOM 2023) study how much a platform gains from two operational controls under these conditions: admission control (rejecting some ride requests, depending on destination) and centralized repositioning (directing idle drivers to move empty between locations). The benchmark of their comparison is the regime in which the platform has both controls, called centralized control (regime ). This mission formalizes the paper's characterization of that benchmark: how a fixed number of drivers should be allocated, what each driver then earns, and why the resulting driver equilibrium is the platform's optimum.
There are two locations and four routes , . Route has potential demand rate and travel time . The price is per unit of travel time; the platform keeps a share and drivers keep , with , while paying a driving cost rate , with . Demand is imbalanced: (Assumption 1). Repositioning is profitable: and (Assumption 2).
A pool of potential drivers has opportunity cost rates drawn from a continuous distribution with CDF , strictly increasing on with , and (Assumption 3). If drivers expect a profit rate , then of them participate.
In steady state the platform splits a driver capacity into service capacity on each route, repositioning capacity (empty driving) and queueing capacity (idle drivers). With totals , , and , the set of feasible allocations is
The first equation balances the flows of cars between the locations. The platform earns ; each driver earns
The platform's problem (13) maximizes over with and the participation equation ; its value is .
The paper solves (13) in two steps. Step 1 fixes , computes the maximal revenue over , and among the revenue-maximizing allocations selects one that maximizes , giving the per-driver profit . Step 2 solves . The constants
split capacities into scarce, moderate and ample zones.
The corollary is what makes centralized control a usable benchmark. It says the platform's joint problem, which couples a linear program with a fixed-point equation in , decomposes: the platform can optimize a fixed capacity and then let drivers settle, with no loss. Under the other regimes of the paper this alignment of platform and driver incentives can fail, and the paper's comparisons of regimes (value of admission control, value of repositioning) are measured against the regime- optimum characterized here. Proposition 1 also makes explicit that a centralized platform keeps drivers idle only when all demand is served.
The paper's proofs are in its e-companion, which is not part of the source this mission cites; no machine-checked version of these results exists. The mission produces a checked parametric solution of a small linear program, a checked closed form of the per-driver profit, and a checked equilibrium-and-optimality argument, with every standing assumption made explicit.
Proposition 1 is a parametric linear program in eight variables, but stating its solution is not enough: each zone needs an upper bound on valid on all of , and a second optimization (per-driver profit) over the set of revenue maximizers, which is not a singleton. Driver-optimality (16) is a separate claim about a different objective over the full set ; it holds only because Assumption 2 makes the capacity used for excess cross-location demand still profitable for drivers. Finally, Lemma 1 compares tuples of (13) at different capacities, which requires monotonicity of and in and the participation equation at both capacities. The natural reading of "" as uniqueness of the optimal capacity is false when , since wasteful repositioning can keep revenue at a smaller capacity; the targets assert attainment instead.
All objects live in the namespace RideHailing.Central, in one definition file. Routes are named fields (Λ11 … Λ22, t11 … t22), not indexed. is ProbabilityTheory.cdf μ of a measure μ on . The standing hypothesis Model.Standing bundles , , Assumptions 1–3 as printed, and the paper's implicit conventions, made explicit: , , , , , a probability measure with continuous CDF.
and are defined as suprema over the allocation problem; every target states attainment with IsGreatest or with membership in the selected set, so no conclusion rests on a supremum convention. Capacities in (13) and (16) are strictly positive, because (12d) divides by .
Trivializing formalizations are ruled out: is defined through the two-step selection, never by its closed form (18); "max" is never an unattained supremum; feasibility for (13) includes the participation equation and ; and is characterized by and then quantified over, never chosen.
Regimes and of the paper, which need objects defined only in the e-companion, are out of scope, as are the reformulation of §2.4 and Remark 2. Proofs of any milestone, and lemmas on monotonicity of or attainment of linear programs over , are welcome.
Phase estimation asks: given access to a unitary and an eigenvector with , determine . It is the subroutine behind Shor's factoring algorithm, quantum chemistry energy estimation, and amplitude estimation, and is one of the standard sources of quantum speed-up.
Martyn, Rossi, Tan and Chuang, A Grand Unification of Quantum Algorithms (PRX Quantum 2, 040203, 2021), present search, phase estimation and Hamiltonian simulation as instances of one primitive, the quantum singular value transformation (QSVT) of Gilyén, Su, Low and Wiebe (arXiv:1806.01838, STOC 2019). Most of the paper's numbered results restate QSVT theory from earlier work. Its own proved content is Appendix B: the analysis of phase estimation by QSVT (Section V, Algorithm 3), a bit-by-bit binary search in the spirit of Kitaev's iterative phase estimation, where each bit is read by applying a sign function to a singular value. A closely related QSVT phase-estimation algorithm was found independently by Rall (arXiv:2103.09717).
This mission formalizes that analysis: the exact-arithmetic correctness of the bit search (Theorems 6 and 7), and its robustness when the sign function is only approximated (Theorem 8).
Fix a unitary , an eigenvector , and the phase . Write for the fractional part of .
For and , the matrix acts on with singular value
The procedure keeps a binary fraction , initially , and runs iterations for a positive integer . Iteration halves , evaluates the sign function at through QSVT, measures one ancilla bit , and sets the first binary digit of to :
An additional iteration then sets the units digit , and the output is .
The ideal measurement returns when and when . In practice the sign function is replaced by a polynomial that is reliable only outside the Δ-region ; inside it either bit may be returned.
If
then in every run of the procedure, the singular value can fall in the Δ-region only at the first iteration , and the output satisfies
A companion item states (68): the matrix of Figure 10 is unitary and block-encodes .
Theorem 8 is what makes phase estimation by QSVT implementable: a sign function cannot be realized exactly by a polynomial, and the theorem shows that a polynomial approximation which fails on a band of width about around costs at most one bit of accuracy, and only at one iteration. Combined with the per-iteration failure probability analysis (71)–(72), it yields the paper's claim that queries give an -bit estimate with probability .
On the formal side, the paper proves these results in Appendix B by case analysis on binary digits with carries. No machine-checked version of the analysis exists on the platform, and no QSVT-based phase-estimation result has been formalized elsewhere to the curators' knowledge. The mission separates the deterministic correctness of the bit search from the quantum machinery, so the combinatorial core can be checked independently of QSVT itself.
The obvious argument tracks the digits of one at a time, and it works for an -bit phase. It fails when has more than digits: the sign function rounds rather than truncates, so a bit can be set to when the true digit is , carries propagate, and the invariant must be a rounding statement with a carry bit (Lemma 12's nine-case induction). The final bit can carry into the units place, which is why the additional iteration exists.
For Theorem 8, the natural first idea, that a bit error makes all later bits unreliable, is false; the content is that after an error at the distance stays a fixed amount away from the Δ-region at every later iteration. Turning this into the threshold requires precise bounds on near .
Everything is stated in Lean 4 with Mathlib, over , in the namespace QSVTPhaseEst.BitSearch. The conventions:
Bool; is Int.fract (2^j * φ).A formalization in which the outcome rule mentions , its digits or its rounding, in which is written through the digits of , or in which the output is defined as a rounding of , would make the theorems circular; none of these is used.
Not formalized: QSP and QSVT themselves (Theorems 1–4, 9, 10; Theorem 1 is already an open goal on the platform), the polynomial of (69), the -error probability analysis (71)–(72), and the runtime. Contributions of reusable lemmas on binary roundings (Int.fract of , nearest dyadic rounding with carry) and on near are welcome.
Submodular function minimization (SFM) asks for a set minimizing a function with diminishing marginal returns. It contains minimum cut, matroid intersection and many problems of combinatorial optimization, and the question of how fast it can be solved with a value oracle has a long history: Grötschel, Lovász and Schrijver (1981) gave the first polynomial algorithm via the ellipsoid method; Iwata, Fleischer and Fujishige (2001) and Schrijver (2000) gave the first combinatorial strongly polynomial algorithms; Orlin (2009) brought the bound to .
Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) applied their faster cutting plane method to SFM and obtained an strongly polynomial algorithm. Like several earlier strongly polynomial algorithms, theirs works over a ring family and repeatedly adds new valid arcs that shrink the family without losing a minimizer. The combinatorial core of that step is Lemma 79 (p. 84) and its mirror image Lemma 80 (p. 86), which the authors describe as new to their work. This mission formalizes Lemma 79 and the lemmas its proof uses.
Let and let be submodular (Definition 58): whenever and , where . As in §13.1, .
For write . The base polyhedron is
Every permutation of defines a basic feasible solution (BFS) of by (Theorem 62); precedes when .
A set of arcs on (an acyclic digraph) represents the ring family of sets such that implies for every arc . and are the descendants and the ancestors of , both including . A permutation, or its BFS, is consistent with if for every arc the element precedes (Definition 74). A vector is non-degenerate if it has both a positive and a negative entry. Finally,
An arc is valid if adding it keeps a minimizer of over .
Let be a non-degenerate convex combination of BFS's consistent with . If
then there is such that every minimizer of over that contains also contains .
The mission also contains Lemma 76 (the mirror of Lemma 77), Lemma 78 ( for consistent BFS's) and Lemma 80 (the mirror of Lemma 79, giving an arc with when ).
Lemmas 79 and 80 are what make the paper's SFM algorithms strongly polynomial: each application adds one of at most arcs, and the cutting plane method supplies, through its separating hyperplanes, exactly the convex combinations of consistent BFS's the lemmas take as input. Lemma 80 has no counterpart in earlier work, and the two lemmas are stated for general ring families, which the earlier versions were not. They are also a robust version of Lemma 65: a point of the base polyhedron that is only approximately degenerate still yields structural information about every minimizer.
The lemmas are proved in the paper; none of them is formalized. The mission produces machine-checked statements and proofs of the arc-adding step, in a form independent of the cutting plane machinery and reusable by any formalization of a ring-family SFM algorithm (Iwata–Fleischer–Fujishige, Orlin, or Lee–Sidford–Wong).
The inequality chain of each lemma is short; the work is in the combinatorics of permutations. Moving to the front of a permutation must be shown to produce a permutation again, and the comparison (15.2) depends on knowing exactly which elements precede each before and after the move; the identity holds only because consistency puts all of before , which needs an induction along paths of . The restriction to changes the ground set, so Lemma 77, stated on the full ground set, does not apply verbatim to the restricted problem. The paper's application of Lemma 77 also does not check that the restricted vector is non-degenerate, so that case has to be handled as well.
The ground set is Fin n (0-based); sets are Finset (Fin n), is integer valued and vectors are real. A permutation σ : Equiv.Perm (Fin n) is a position map ( precedes iff σ u < σ v), and the BFS of a permutation is defined by the formula of Theorem 62; Theorem 62 itself (that these are the vertices of ) is not formalized and not needed. Arcs are a relation on Fin n; and use its reflexive-transitive closure, and the digraph is assumed acyclic, as the paper does. Minimizers in Lemmas 76–80 are over the ring family ; in Lemma 65 over all subsets. Constants , and are real numbers.
Running-time and oracle-count clauses ("using oracle calls and time") are out of scope, as is the paper's main Theorem 31 and the bound on the number of BFS's in the combination (the existence claim holds for any finite combination). Validity of the new arc is stated in the strong form proved on p. 85: every minimizer containing contains . The page's base polyhedron constraint "" is read as . The restricted base polyhedron in the restriction claim uses the normalized .
The hypotheses are satisfiable: with , , , , the combination satisfies them for . A modular never does, so the goal is not vacuous only because is genuinely submodular; a formalization in which the BFS's are not tied to , or in which non-degeneracy is non-strict, would change the statement and is ruled out.
Useful infrastructure: greedy vectors of a submodular function lie in its base polyhedron; reordering lemmas for permutations of Fin n; restriction of a set function to the complement of a set. Contributions of proofs of any milestone, and of Lemmas 76, 78 and 80, are welcome.
A permissioned blockchain is a shared ledger to which only approved participants may write. In supply chains it is proposed as a way to make product information (origin, quality, which supplier fulfilled an order) verifiable to buyers. Iyengar, Saleh, Sethuraman and Wang (SSRN 3602376; Management Science 2023, doi:10.1287/mnsc.2022.4532) ask who gains from such adoption and who pays for it.
Their first main result (Proposition 4.8, the subject of the companion mission I) identifies an adoption failure: when products differ strongly in how well they match consumers' tastes, full adoption raises total welfare, yet no manufacturer adopts, because price competition leaves manufacturers no profit with which to recover the adoption cost while the information gain accrues to consumers. Their second main result, Proposition 4.9, the goal of this mission, shows that a simple self-financing mechanism removes the failure: charge consumers a fee for access to the blockchain's information and pass the proceeds to the manufacturers.
There are manufacturers, . Manufacturer has a horizontal type and a vertical type ; each of the four type classes has exactly members. Joining the blockchain costs manufacturer an amount ; records the decision. A unit mass of consumers values a matching product at and a mismatched one at , with , plus a vendor quality ; the high-quality vendor has marginal cost . Each consumer also has an outside option , drawn from a continuous distribution supported on . The parameter of interest is the horizontal differentiation ; is held fixed and .
Under full adoption, a consumer who has access to the blockchain's information finds a best product utility ; without access, only . A system of transfers charges each consumer who wants access a fee and pays manufacturer an amount . A consumer pays () when
and denotes the mass of paying consumers. The system is self-financing if
Manufacturer earns (15), where the gross profit is zero because of price competition. The system overcomes adoption failures if full adoption ( for all ) is an equilibrium of this game.
The proof of Proposition 4.9 uses the fee and the gain from access
The goal asserts the existence of a working scheme, as printed; it does not fix the scheme.
(a) For and every , is continuous and weakly decreasing on .
(b) For all sufficiently large there is with
so that at the fee exactly the consumers with pay.
Proposition 4.9 is the constructive half of the paper's message: an adoption failure driven by the split between who bears the cost and who reaps the benefit can be repaired without outside funding, by a fee on the side that benefits. The paper's scheme (, ) exactly reimburses adoption costs and is financed by a threshold set of consumers; Lemma B.1(b) is the fixed-point statement that makes this calibration consistent.
The result is proved in the paper (App. A.2, pp. 36–38, and App. B, pp. 38–41). It has no machine-checked proof. This mission produces one: a formal model of the access-fee mechanism in the reduced form the paper's proofs use, the threshold lemma, and the main proposition. The goal can be attacked through Lemma B.1(b) as in the paper, or by any other scheme meeting the definition.
The calibration is circular: the fee depends on the mass of paying consumers, and the mass of paying consumers depends on the fee. Lemma B.1(b) resolves this with a one-dimensional fixed point , and the delicate points are positivity of at the relevant arguments (so that the fee is finite), the three-piece shape of , and choosing large enough that the sign change happens inside the strictly decreasing piece. For the goal, the point to check is that the self-financing identity uses the actual mass of payers at the chosen fee: a fee too high drives the payers' mass, and with it the revenue, towards zero.
Fin 2 × Bool × Fin m; adoption profiles are Bool-valued. is ProbabilityTheory.cdf μ for a measure μ on ℝ. is an argument of every object, with .Model.Standing): , , , , ; a probability measure without atoms, , and for (support ). No cost function , no Assumption 1 and no finite mean are needed or assumed. Lemma B.1(a) additionally assumes , the model's .ProbabilityTheory.cdf; no new library is needed. Lemmas on CDFs of atomless, fully supported laws on are reusable beyond this mission. Proofs of the milestones and of the goal are welcome; the goal may be proved by any route.Y. Bai (arXiv:2609.11276, September 2026) proves that the irrationality measure of π is at most 7.101862832357, improving the Zeilberger–Zudilin bound 7.103205334137 (2020). The proof keeps the Zeilberger–Zudilin integral but gives its numerator two independent exponents, specialised at A₁ = A₂ = 1857/2785; the resulting integer linear forms in 1 and π, combined with Hata's lemma, give μ(π) ≤ 7.101862832357. This entry is the campaign template with the value 7.101862832357. Source: https://arxiv.org/abs/2609.11276
The original exact goal EndStatement.ThreeSum.SolvedInTime 1.960614 is Proved on Prove2Me. All seven original milestones are complete. The complete machine extension has 481 accepted theorem proofs and reuses 110 proved theorem nodes; its accepted dependencies connect to the original main reduction. The independent fixed-model lower bound remains separate from the algorithm proof. Scientific priority and global optimality are not asserted by these formal verification results.
3SUM asks whether three entries at distinct positions in an integer input sum to zero. Its familiar quadratic algorithm makes it a benchmark for studying how much arithmetic structure can reduce the cost of an exhaustive search. The relevant comparison is the exponent of input size in a precisely specified machine model. An improvement to that exponent is an asymptotic statement; it need not provide better measured running times at accessible input sizes.
Alman and Vassilevska Williams, 2026 developed a deterministic truly subquadratic framework for polynomially bounded integer 3SUM. The c0ldzy17 source snapshot, dated 11 October 2026, develops a subsequent deterministic construction with a formally stated 1.962 target. The author-supplied certificate package 3sum_certificate_1p960614_v3, dated 14 October 2026, studies a further parameter and switch refinement. It contains mathematical arguments and exact rational checks, and explicitly leaves the complete modified machine-program theorem unproved. This mission studies that remaining extension together with its supporting certificates.
An input of size is an integer-valued function on the positions . For each fixed natural number , every value has absolute value at most . A YES instance has pairwise distinct positions satisfying . Equal values at different positions are allowed. The problem asks for a decision, so a successful algorithm need not return the positions. Inputs of size less than three are NO instances.
The word RAM is the existing campaign foundation specification. A program is a finite list of instructions for constants, arithmetic, direct and indirect memory access, branching, acceptance and rejection. Words have a fixed width and a signed integer interpretation. For each fixed , one program, one word-width constant and one time function must work for every input size and every sufficiently large word width. The mission retains that specification without introducing an alternative computation model.
The supporting binary entropy is measured in bits:
For an integer expansion , write
These are analytic quantities used to describe local encoding and reporting costs. The source's twelve charges also depend on a representation-scale parameter , a band shift , a box saving , an initial threshold , a terminal fraction , and a uniform entropy coefficient .
The campaign goal is the exact proposition
For , its time requirement is
Correctness and termination still cover all input sizes. The integer-size exponent includes , and the same program must be correct for every word width above its specified threshold.
The primary certificate uses and the rational quartic
Supporting targets establish its validity on , its derivative and tangent bounds, and the uniform inequality . The fixed parameters are , , , , and . The parameter theorem bounds every one of the twelve costs strictly below . Integer scheduling and general local-cover identities are separate milestones. A further independent milestone proves for the explicitly defined relaxed fixed-expansion cost model. That model bound concerns its admissible parameter tuples; it is not a lower bound for 3SUM itself.
The supplied certificate demonstrates that a quartic switch already suffices for the proposed 1.960614 cost target. It also separates a uniform analytic inequality from a numerical experiment: the statement quantifies over the full closed interval. Its finite scheduling statement uses integer comparisons and accounts for the rounding error at every admissible level, rather than requiring executable logarithms.
Formalization adds checked statements about these continuous and finite objects and a reusable dependency structure. The full campaign goal requires an additional result: the actual modified program must obey the certified costs, and its operational correctness must reach the foundation specification. The upstream parameter certificate likewise distinguishes its exponent ledger from its separate implementation obligations. An exact rational checker passing is evidence for the numerical certificates; it does not establish the full new machine theorem.
Changing expansion from 256 to 232 changes the local universe and the vertex, output and degree counts together. The representation scale, band denominator and polynomial switch also change. Consequently, the original fixed-parameter runtime result cannot simply be invoked after replacing a few numerical constants. The new local construction, global encoding, sparse queries, reporting and arithmetic operations must share consistent parameters and a complete cost account.
The small gap between the principal cost cap and the target must absorb the proved subpolynomial overheads, including exceptional-size handling and the conversion to word instructions. The machine bridge has now been proved in this mission. Its accepted dependency tree connects the modified program and its runtime analysis to the unchanged campaign specification. Its statement has no assumed solver callback or unproved runtime contract. The fixed-model lower-bound milestone is an independent analytic root, and is not used to justify a faster algorithm.
The campaign pins Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Entropy and its derived quantities are real-valued; the final exponent is rational; finite subset counts and cleared switch comparisons use natural numbers. Theorems explicitly restrict logarithmic arguments and denominators to their intended domains. Natural-number subtraction in the switch is used only below the final level, with positive even microblock size.
The local-cover milestone covers every natural and positive half-block size. The cost-model milestone quantifies over all tuples satisfying its written assumptions and includes a whole-interval entropy constraint. Neither finite testing nor a floating-point optimizer substitutes for these universal statements. The initial package includes no Lean proof of the new machine goal, and the mission does not represent it as an established record.
The underlying algorithms and formal infrastructure retain their attribution to Alman and Vassilevska Williams; Björklund, Husfeldt, Kaski and Koivisto; Swapnil Jain; c0ldzy17; Anthropic; Jihoon Hyun; and Lean/Mathlib, as documented by the upstream source. The certificate development and this formalization use AI assistance. Scientific priority and global optimality are outside the mission's claims.
3sum_certificate_1p960614_v3/3sum_certificate_v3/PROOF.md, Sections 0–8; certificates/c232_quartic.json; verify_certificate.py. This is a supplied research artifact, not a claimed public publication.Source code and complete Lean formalization: GitHub repository. Fixed source revision: 8c25c0325de5.
Retail prices are rarely constant over long horizons: promotions, high–low cycles and staggered discounts across similar items are the norm. One explanation in the pricing literature is the reference effect: consumers compare a posted price with a reference price formed from past prices, and react to gains and losses relative to it. Single-product models with reference effects (Popescu and Wu 2007; Hu, Chen and Hu 2016) predict that, for consumers who react symmetrically to gains and losses, the optimal price usually settles to a constant. Guo, Jiang and Shen (SSRN 4189049, published in Manufacturing & Service Operations Management, 2025) study the same question for several substitutable products sold under multinomial-logit (MNL) demand. Their §4.3 shows that pricing substitutes jointly, rather than at one common price, makes cyclic optimal pricing more likely. This mission formalizes that comparison, Theorem 7, together with the results the paper ties it to.
A seller offers products over periods . In period product has price and reference price , both in with . Reference prices follow exponential smoothing with memory .
The deterministic utility of product is
with and . The market share is and the period revenue is . Product is loss-neutral when . The seller maximises with discount ; is the optimal value. The myopic policy maximises over . Throughout, the paper assumes , where solves its equation (9); this makes the ceiling inactive for the myopic problem.
A policy has a steady state if it maps reference to price . An optimal steady state (Definition 4) is a steady state of an optimal policy, and a policy is cyclic when it has no steady state.
§4.3 takes perfect substitutes: , , for all , loss-neutral. The single-product-based policy solves the problem (25) restricted to one common price for all products, from a uniform reference . The common myopic steady state comes from Corollary 2, where solves . The constants are
For identical loss-neutral products with :
and
hold, then has a steady state and the optimal policy has none.
Theorem 7 separates two models that coincide in their steady states (Remark 3) but differ in whether a steady state exists. Joint pricing can sustain asynchronous cycles, in which some substitutes are discounted while others are not, and these keep total purchase probability high. A single common price can only cycle synchronously. Part 1 says the multi-product optimum never settles when the single-price one does not. Part 2 gives explicit parameter regions, strong reference effects (large ), short memory (small ) and patient sellers (large ), where the single-price model predicts a constant price but the true optimum is cyclic. Practically, a retailer who prices similar items at one price can misjudge whether long-run promotions are optimal at all.
The paper's proofs are in its online supplement (Appendix C.6), which is not part of the source file used for this mission. To our knowledge none of these results has a machine-checked proof. A formalization would check the inequality algebra behind (26)–(28) and pin down exactly what "the optimal policy is cyclic" means when optimal policies need not be unique.
The statements compare two infinite-horizon problems, each with a continuous state, through the existence of fixed points of their optimal policies. Neither problem has a closed-form value function. A steady state is optimal only if no deviation, however long, improves on the constant path, so ruling it out requires a profitable deviation, and establishing it for requires a global optimality argument for (25). Stationarity conditions at a steady state only produce candidates (Corollaries 2 and 4); they do not decide whether a candidate is optimal, so the obvious argument stops exactly where the theorem starts. The revenue is not concave in prices, the reference dynamics couple all periods, and the comparison must hold uniformly over every optimal policy, not one computed policy.
Products are Fin n (index for the paper's product ), and parameters are functions Fin n → ℝ; the identical-products results use constant functions of scalars . The market share (3) is defined directly, without the Gumbel derivation. is the supremum of the discounted revenue over all price sequences in , and the single-price value is the supremum over uniform sequences from a uniform reference. Steady states are in sequence form: is an optimal steady state when the constant path from reference attains , and similarly for . "Cyclic" is the universal statement that no point is a steady state. A myopic policy is any maximising selection, and every statement about it quantifies over all selections.
Standing hypotheses in every theorem: , , , , , and stated as "some root of (9) is at most ". Added hypotheses: (the setting of §4.3); in Theorem 7.2, so that is defined (it excludes only , where (26b) fails anyway); for the limit claims of Corollary 2 (at the reference never moves). Quantities the paper calls "the unique solution" are bound as variables solving their equation, never chosen. Remark 4 evaluates (28) at the candidate of Corollary 4, because the conclusion is that no optimal steady state exists.
A trivial formalization is ruled out: "cyclic" may not be read as a statement about one chosen policy or one initial reference price, and the single-price problem may not be replaced by the problem, since it keeps all products and the shared MNL denominator.
A complete development needs: summability and boundedness of discounted revenue, the Bellman characterisation of steady states, analysis of the myopic MNL problem (Theorems 1–2 of the paper), and the second-order analysis behind (28). The MNL revenue lemmas and the sequence-form steady-state calculus are reusable beyond this mission. Proofs of any milestone, and of the parts of Theorem 7 separately, are welcome.