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?
Least-squares estimation from adaptively collected data is the statistical heart of linear bandits: the actions depend on past noise, so classical fixed-design theory does not apply. Chapter 20 of Lattimore–Szepesvári resolves this with the method of mixtures: the process is a supermartingale, and integrating over a Gaussian mixture yields the self-normalized bound — the goal theorem — , valid uniformly over all times. The resulting confidence ellipsoids for the regularized least-squares estimator (Abbasi-Yadkori et al.) calibrate every algorithm of Mission X. The mission also formalizes the Kiefer–Wolfowitz theorem of Chapter 21: G-optimal and D-optimal experimental designs coincide, with optimal value exactly — the classical equivalence theorem of optimal design theory.
Every even integer greater than is the sum of two primes. Christian Goldbach posed it in a 1742 letter to Euler, and it has resisted proof for nearly three centuries while being verified computationally up to — making it one of the oldest and most famous open problems in all of mathematics. Its ternary sibling, the weak Goldbach conjecture, was settled by Helfgott in 2013, but the strong form stated here remains wide open: the circle method controls three-prime sums yet loses control at two. This headline mission hosts the conjecture as a machine-checked target for partial results, reductions between its variants, and any future attack.
A reinforcement-learning agent that learns a Markov decision process (MDP) from data ends up with point estimates of the Q-values: the long-run discounted reward of taking an action in a state and acting optimally afterwards. Point estimates say nothing about their own reliability. Choosing between two actions whose estimated values differ by a small margin, deciding how much more data to collect, or allocating exploration effort all need the sampling distribution of the estimate. Finite-sample bounds (Kearns and Singh 1998) give rates with loose constants. Asymptotic normality gives exact limiting constants.
Zhu, Dong and Lam establish a central limit theorem for the plug-in Q-value estimate of a finite MDP whose data are collected by an exploration policy, with an explicit covariance matrix. For a fixed policy, the analogous result for the value function was obtained by Mannor, Simester, Sun and Tsitsiklis (2007). The new step is the optimal Q-values, which depend on the data through a maximum over actions. The paper uses the covariance to design a pure-exploration policy (Q-OCBA) that allocates samples to maximize the probability of selecting the optimal policy.
Let and be finite nonempty sets of states and actions. A pair has a random reward with law on , mean and variance , and moves to state with probability . The discount factor is . The Bellman operator is
and the Q-values are its fixed point , with .
Data are collected by an exploration policy . Starting from some state, the agent repeatedly takes , observes , and moves to . The state-action pairs then form a Markov chain with transition matrix . From observations, the plug-in estimates are the sample mean reward and the empirical transition frequencies at each pair, with fixed initial values at unvisited pairs. The estimate is the fixed point of .
The standing assumptions are:
Under Assumptions 1–3, almost surely, and
Here , and , , are diagonal with entries , and . The matrix is the multinomial covariance of . The covariance is part of the statement: the paper's subsequent results (Corollary 1, Q-OCBA) use it.
The result. Theorem 1 gives asymptotically exact simultaneous confidence regions for all Q-values from one trajectory of exploration data. The closed form of shows how each source of noise contributes: reward noise through , transition noise through , the amount of data at each pair through , and propagation through the dynamics of the optimal policy through . This decomposition is what makes usable as an objective for allocating exploration effort, which the paper's Q-OCBA policy does. Corollary 1 (CLT for the optimal value ) is derived from it.
Formalizing it. The result is proved in the paper, but the proof cites its probabilistic core: a joint central limit theorem for empirical transition frequencies of an irreducible finite Markov chain (Trevezas and Limnios 2009, Proposition 3), together with the multivariate delta method. A machine-checked proof would also certify that the covariance formula, with its transposes and weights, is correct as printed. No Q-value CLT or Markov-chain CLT for empirical transition matrices is currently formalized on the platform. The existing Markov-chain CLTs there are scalar and assume uniform ergodicity.
The deterministic half (milestones 4, 5, 7) is linear algebra plus an implicit-function argument. The obstacle is that depends on through a maximum, which is not differentiable at ties. Assumption 2 removes ties at , and differentiability holds only on a neighbourhood where the argmax stays the same.
The probabilistic half is harder. A natural first idea is to treat the visits to each pair as i.i.d. samples and apply the classical multivariate CLT. This fails because the number of visits is random and depends on the whole trajectory, and the samples at different pairs are dependent through the chain. The CLT (23) needs a martingale or regeneration argument for the Markov chain on state-action pairs. The chain is only assumed irreducible, so it may be periodic, and uniformly ergodic CLTs do not apply directly.
S × A with Fintype, DecidableEq and Nonempty; the paper's flattening is notation only. , and the initial state law are PMFs, and rewards are probability measures on with MemLp id 2 (Assumption 1).MarkovChainCLT.chainMeasure. Every initial state law is allowed. Time is 0-based.bellmanFix). It is the unique fixed point whenever the Bellman operator is a contraction, which covers every stochastic and a neighbourhood of .multivariateGaussian on EuclideanSpace, and convergence in distribution is TendstoInDistribution.Trivializations ruled out.
Matrix.inv returns on singular matrices, but is invertible under the pins, so is not a junk zero.multivariateGaussian returns a point mass for a non-positive-semidefinite matrix, but and are positive semidefinite.Infrastructure. A complete development needs:
TendstoInDistribution form;Contributions of any of these as standalone lemmas are welcome.
Not posed. Corollaries 1–2 and Theorems 2–6 of the paper (optimal-value and fixed-policy CLTs, non-unique optimal policies, constrained MDPs, Q-OCBA consistency, approximate value iteration, kernel representations) are not part of this mission.
Many selection problems in machine learning and operations research ask for a set of items that maximizes a utility with diminishing returns, subject to a combinatorial feasibility constraint: summarizing a collection of images or documents, placing sensors, recommending a diverse set of products, or choosing a set of edges that forms a matching. Diminishing returns is submodularity; the feasibility constraints in these examples (matroids, intersections of matroids, matchings, knapsack-type systems) are instances of -extendible systems, a class introduced by Mestre (ESA 2006). Many useful objectives, such as graph cuts and diversity-regularized utilities, are non-monotone: adding an item can lower the value.
The greedy algorithm has a long history for this problem class. Fisher, Nemhauser and Wolsey (1978, doi:10.1007/BFb0121195) showed that greedy gives a -approximation for monotone submodular objectives over -systems, a class that contains -extendible systems. For non-monotone objectives, the known greedy-based algorithms ran the greedy algorithm repeatedly. Gupta, Roth, Schoenebeck and Talwar (WINE 2010) obtained roughly , Mirzasoleiman et al. (2016) roughly , and Feldman, Harshaw and Karbasi (COLT 2017) , each with or oracle queries. Harshaw, Kazemi, Feldman and Karbasi (arXiv:2104.02772; Mathematics of Operations Research, 2022) showed that a single random subsampling of the ground set, followed by one run of the plain greedy algorithm, gives a -approximation for non-negative submodular objectives with expected oracle calls. This mission formalizes that guarantee.
Let be a finite ground set of size , with a fixed linear order that is used only to break ties. A set function is a map . The marginal gain of at is .
The problem is for non-negative submodular ; OPT denotes a maximizer.
SampleGreedy with sampling probability keeps each element independently with probability , giving a sample . It then starts from and repeatedly adds the element of largest marginal gain among those with and , ties broken by the fixed order, until no such element is left. Its expected value is
For the analysis the paper introduces Algorithm 2, which runs greedy over the whole ground set, flips a -coin for each chosen element, and maintains a set (initially OPT), removal sets , snapshots and indicators (" was considered") and .
For non-negative submodular , a -extendible system with , and every : SampleGreedy's output is always independent, and $$f(T) \le \frac{(p+1)^2}{p},\mathbb E_{1/(p+1)}[f(S)], \qquad f(T) \le (p+1),\mathbb E_{1/(p+1)}[f(S)] \ \text{if is monotone},
f(T) \le p,\mathbb E_{1/p}[f(S)] \ \text{if is linear}.$$
In attack order: Lemma 3 (p. 8, already Proved on the platform: a random set whose elements each appear with probability at most keeps a fraction of in expectation); Lemma 4 (p. 10, SampleGreedy and Algorithm 2 have the same output law); Lemma 5 (p. 11, invariants of Algorithm 2); Lemma 6 (p. 12, ); Lemma 7 (p. 13, inequality (5)); Lemma 8 (p. 14); the display of §4.1.1 (p. 14); Lemma 9 (p. 15, linear objectives); Lemma 10 (p. 16, inequality (7)).
The result shows that one random subsample plus one greedy pass beats the repeated-greedy algorithms for non-monotone objectives over -extendible systems, both in ratio and in query count, and matches the classical for monotone objectives. Since no polynomial-query algorithm achieves a ratio better than for this problem (Feldman, Harshaw and Karbasi 2017, Theorem 4), the ratio is nearly tight. The proof technique, which couples the subsampled algorithm with an auxiliary algorithm that flips coins only for the elements it considers, is reused in the paper's streaming algorithm and in later subsampling-based algorithms.
The result is proved on paper; no machine-checked version is known. A formalization would give a checked analysis of a randomized greedy algorithm over an abstract independence system, including the coupling of two random processes, which is the step that informal proofs usually treat most briefly. It would also give reusable definitions of -extendible systems and of greedy runs with explicit tie-breaking. The mission also records a defect of the printed text: Lemma 9 as printed is false for linear functions with , so it is stated here with .
The obvious argument would analyze SampleGreedy directly, but there the sample and the greedy path are entangled: which element is chosen next depends on the whole sample. The analysis instead goes through Algorithm 2, and the hard step is Lemma 4, an exact equality of output laws. Its proof needs both algorithms to break ties identically and the coins to be fixed in advance. After that, the expectation bounds of Lemmas 7, 8 and 10 condition on the history up to the iteration in which a given element is considered, and the coin of that element is independent of that history. In the finite-sum encoding this conditioning becomes a combinatorial regrouping of the coin outcomes, which has to be carried out explicitly. Lemma 6 requires a disjointness argument for the sets across the whole run.
The ground set is a Fintype α with a LinearOrder α, which is the paper's tie-breaking order (p. 10). Set functions are Finset α → ℝ, and is a predicate Finset α → Prop. The parameter is a natural number with . Submodularity is the published lattice form NonmonotoneSubmod.Shared.Submodular (), equivalent on finite ground sets to the paper's (1). The while loops run for exactly iterations, which is enough because each effective iteration adds or considers a new element. Expectations are exact finite sums over the samples or coin outcomes. Algorithm 2's coins are a fixed bit set, and its line 6 is one fixed minimum-cardinality choice. "-approximation" for a randomized algorithm is read, as in the paper's proof, as , stated against every independent . Linear means (1) with equality and allows , except in Lemma 9, which adds . The oracle-count clause of Theorem 1 is not formalized.
Trivializing encodings are excluded. The expected value is a sum over the greedy runs on each sample, with the sample as the greedy pool (not the whole ground set followed by a filter). The weights sum to 1. The comparison set is always assumed independent. The ratio is real division. A sanity file checks that the output on a sample differs from the output on the whole ground set.
A complete development needs the greedy run's invariants, the coupling of Lemma 4, and the regrouping of finite sums over coin outcomes by the history before a given element is considered. The last of these is reusable for any analysis of an algorithm that flips independent coins. Proofs of any milestone, and alternative proofs of Lemma 4, are welcome.
Two parties who do not share a reference frame can align one by sending quantum systems through an unknown rotation. Mathematically, a device applies an unknown matrix to each of qubits, and the task is to estimate from one measurement on the output. How fast the smallest achievable error falls with is a basic question of quantum metrology and quantum statistics: classical repetition gives order , and entangled inputs can do better.
Masahito Hayashi's paper (arXiv:quant-ph/0407053v3) shows that, with the right input, estimating an SU(2) action reduces exactly to the phase-estimation problem solved by Bužek, Derka and Massar. The reduction yields an error of order with the explicit constant .
Timeline.
Let be the group of complex unitary matrices of determinant one, and let be its invariant (Haar) probability measure. The cost of reporting when the truth is is
For each , let be the -dimensional irreducible representation of on a space . If has eigenvalues , its character is
where is the Chebyshev polynomial of the second kind.
For uses of with a reference system on which does not act, the paper works on
Its ingredients are:
The method value of an input is .
The goal theorem has four parts.
Equality holds for the phase-aligned , . 3. For , , and the minimum is attained. 4.
The result. The error of a covariant SU(2) measurement on this space equals, coefficient by coefficient, the error of a covariant phase measurement. Eq. (13) says that the SU(2) character integral has the same tridiagonal kernel as the phase-estimation identity (7). Optimizing the input therefore becomes the largest-eigenvalue problem for a path graph, and that problem has a closed-form solution. With uses, the protocol reaches error . This beats the rate of independent uses, and the paper gives the explicit constant. Chiribella, D'Ariano and Sacchi later showed that is optimal over all measurements; the present paper does not prove that.
Formalizing it. No part of this computation is machine-checked yet:
The paper's own displays contain slips: the conjugation in (8), (9) and (14), the value on p. 9, the coefficients of the expansion on p. 10, and a quoted Bužek vector that is not the minimizer. A checked development fixes these.
The obvious route through (13) is to "expand the product of characters and keep the constant and , terms", as p. 10 does. That route needs the Weyl integration formula. Mathlib has the Haar measure but no Weyl integration formula for , no compactness instance on Matrix.specialUnitaryGroup, and no classification of its irreducible representations.
The reduction from the operator integral in (14) to the scalar integral (13) needs two further facts: Schur orthogonality on each pair of blocks, and the invariance of to move from to .
The optimum over inputs is a Perron–Frobenius problem for a path graph. It is easy to state with , but in exact form it needs the attained eigenvector , not the vector the paper quotes.
Representations.
Matrix.specialUnitaryGroup (Fin 2) ℂ.IsTopologicalGroup, CompactSpace, MeasurableSpace with BorelSpace).dg.BasedIrreps (based, continuous, unitary, irreducible), indexed for .CanonicalIndex, canonicalAction and canonicalInput (with identity block unitaries).Measurement and error.
DensityPOVMs: a reference measure and a PSD operator density integrating to .bellCost.Ruled-out trivializations.
IsLeast, not sInf or ⨅.Infrastructure. The reusable parts beyond this mission are:
Gap48.P23.polynomialIrrep);Proofs of any milestone, and of these supporting facts, are welcome.
Related work on the platform. The Chiribella–D'Ariano–Sacchi items of the Next46.P36 series pose related but different statements:
optimalPOVM and minimumEigenvalueInput concern a general compact group, a Haar-averaged risk, and optimality over all measurements.cartesianFrameOptimum concerns SU(2) without a reference system, with a different cost.This mission reuses their definition layer and their Schur orthogonality theorem. It states Hayashi's own reference-assisted protocol, with its exact pointwise error and the limit .
Not formalized. The following parts of the paper are out of scope:
Organizations, athletes and students build capability gradually: a team can raise or lower its skill level only a little from one period to the next, while the demands placed on it can change abruptly. A trainer (a coach, a manager, a curriculum designer) who controls the sequence of demands, subject to a budget on their average intensity, wants to know which sequence leaves the trainee with the highest capability in the long run. Periodized training in sports, with alternating rest and high-intensity phases, is the familiar practical answer.
Eliaz and Spiegler (Management Science, 2023) model this as a trainer committing to a stochastic challenge process and an agent that adjusts sluggishly, by at most one unit per period. Their Proposition 1 shows that against a myopic sluggish agent, a budget of about on the average challenge can sustain a long-run capability of about , nearly twice what a flexibly adjusting agent would keep, and that a slightly perturbed rest/high-intensity cycle achieves it. This mission formalizes Proposition 1.
A training program is a pair : a stochastic matrix on a finite set of states , irreducible, and an output function giving the challenge in each state. By irreducibility has a unique invariant distribution . The program is feasible for an integer and a slack if it satisfies the intensity constraint (1):
The agent holds a non-negative integer capability . At each period it observes the challenge and chooses , paying with . A myopic agent minimizes period by period, which gives rule (2):
The pair is then a Markov chain, the extended process: from it moves to with probability , where is rule (2). The lowest long-run capability is the lowest value takes beyond a sufficiently large . On a finite chain a path is eventually absorbed in a recurrent class and visits all its states infinitely often, so is the minimum of over that class.
(i) If , then for every feasible program on every finite state set, every recurrent class of the extended process contains a state with
(ii) There is such that for every the two-state program
is feasible, its extended process has exactly the recurrent states and , and every invariant distribution puts mass on and on ; both tend to as .
In attack order: uniqueness of the invariant distribution of an irreducible finite chain (§2, p. 7; already proved on the platform); the myopic best response (2); the extended process is a Markov chain whose invariant laws have state marginal ; every recurrent class carries an invariant law; Step 1, the balance identity (4), ; Step 2, ; Step 3, every invariant law charges a capability ; the two-state program's average intensity ; and the recurrent states and invariant masses of its extended process.
The result separates two quantities a trainer might confuse: the average intensity of the demands, which the budget constrains, and the capability they sustain, which depends only on the sign of under sluggish adjustment. Because the cardinal budget and the ordinal adjustment rule differ, alternating rest () with high intensity () holds capability near for an average cost near . Part (i) shows that no program, however many states it uses, does better, so the two-state periodized program is optimal for a myopic agent. The paper's second main result (Proposition 2, a forward-looking agent) is not part of this mission.
Formalizing it adds a machine-checked account of an argument whose printed version has two gaps (see Formalization scope): the bound in part (i) needs , and the printed Step 3 reaches only . The proposition is proved on paper; it has not been formalized. The finite-chain lemmas built along the way (an invariant law on every recurrent class, the marginal of an invariant law of a product-type chain, level-crossing balance for a skip-free coordinate) are reusable outside this paper.
The paper argues with long-run frequencies along a sample path. A formal proof has to replace that by invariant distributions of a finite chain on , whose recurrent classes need not be unique and whose invariant laws need not be unique either. The step from the average bound to the minimum is the delicate one: knowing that is at most about and that is not constant only shows that the minimum is at most . The bound needs a finer use of the constraint, and it fails for , so any argument that treats as negligible without quantifying it cannot be completed.
Lean represents the trainer's chain with the published mm_basic vocabulary (IsStochastic, IsStationary with row vectors , Irreducible); uniqueness of is the proved MarkovMixing.exists_unique_stationary. Challenges and capabilities are natural numbers; and use truncated subtraction (harmless since ). Feasibility asks for some invariant distribution satisfying (1), which is by uniqueness. The extended process lives on Fin (M + 1) × S for a truncation level ; the goal quantifies over every such , which covers every initial capability . "Lowest long-run capability " is stated as: every recurrent state reaches a state with . In the two-state program index 0 is and 1 is . The limit "probability " is stated through the exact masses and , together with existence of an invariant law.
Part (i) is posed with because it is false for . With , , , , : the invariant law is , the average challenge is , and the only recurrent states of the extended process are and , so the lowest long-run capability is . The paper states but says it "can be arbitrarily close to zero" and treats it as negligible. Part (ii) holds for every . The printed Step 3 argument only yields ; a solver must supply the step to , and the milestone is posed in that corrected form.
The statements rule out the trivializing readings: part (i) ranges over every finite state set, every truncation level and every recurrent state (not a fixed , not some class, not the minimum over transient states, which a low would make trivial); part (ii) asserts feasibility, all in an interval up to , that the two named states are the only recurrent ones, and the masses together with existence of an invariant law, so no clause holds vacuously; and the extended kernel is stochastic because .
Contributions welcome: proofs of the finite-chain milestones (they need only mm_basic and Mathlib's matrix library), the balance identity (4), and the corrected Step 3.
mm_basic). https://doi.org/10.1090/mbk/107A retailer selling one product over periods must choose a price each period without knowing how demand responds to price. Charging different prices reveals the demand curve but costs revenue, and in practice every price change has its own cost: relabelling, customer goodwill, contractual limits on repricing. Dynamic pricing with learning asks for policies whose cumulative revenue loss against the best fixed price, the regret, grows slowly in , and recent work also asks that the policy change its price rarely.
The paper's literature review (pp. 3–5) frames the gap. For parametric demand, Broder (2011) gives an MLE-based policy with regret and price changes, and Cheung, Simchi-Levi and Wang (2017) study limited price changes when demand is one of finitely many known curves. Non-parametric policies such as Besbes and Zeevi (2015) and the continuum-armed bandit algorithm of Agarwal et al. (2011) do not control price changes and incur at least of them. Perakis and Singhvi (SSRN 3336949; published in Operations Research, doi:10.1287/opre.2020.0445) show that, under a two-point bandit feedback assumption borrowed from online convex optimisation (Agarwal and Dekel 2010, Nesterov 2011), a non-parametric policy can keep regret while changing its price only times.
Prices lie in . In period the retailer charges and observes demand
where is an unknown smooth non-increasing demand curve and is noise. The revenue is , maximised on at a unique interior price . The two performance measures are
Assumption 1 asks for with ; Assumption 2 asks that among the observations at two charged prices there is one pair with identical noise, and that the policy can identify it. bounds for .
The SLPE policy (Algorithm 1) runs in rounds with half-widths , . Round charges , and for periods each, starting from . It fits a two-piece linear demand estimate whose level is the average demand and whose slopes are finite differences of the two identical-noise pairs, maximises the estimated revenue on to obtain , and recentres: .
Under Assumption 1, the gradient condition with , and
there are constants independent of such that for every , every noise realisation and every choice of the policy's tie-breaking and pair selection,
and, on every realisation where Assumption 2 and the concentration event hold in each used round,
The result gives a non-parametric pricing policy whose number of price changes is doubly logarithmic, the same order as the number of batches needed in batched multi-armed bandits, while its regret is within of the lower bound of Keskin and Zeevi (2014). Its key estimate, Lemma 4, is a perturbation bound for the maximiser of a piecewise linear surrogate of a smooth revenue function; it applies wherever an optimum is located from noisy function values with matched-noise finite differences.
The theorem is proved on paper and, to the extent that can be determined, has no machine-checked proof. Formalizing it adds a continuum-armed pricing policy with an explicit price-change bound, and a checked version of an argument whose printed proof has gaps: a high-probability step that is false as printed, an inequality used two-sidedly that is assumed one-sidedly, and a logarithm base that does not match. Lemma 4 is posed as printed. It is supported numerically but its printed proof is incomplete, so a formal proof, or a counterexample, is itself new information.
The obvious argument for Lemma 4 compares the first-order condition of the surrogate with that of the true revenue. It fails as written: the surrogate's maximiser may sit at an endpoint of or at the kink , where no first-order condition holds, and the comparison needs a two-sided bound on while Assumption 1 is one-sided and weighted by . The regret bound then needs the induction that keeps inside every round's range, a careful treatment of the last round, which the horizon truncates, and the conversion of the doubly exponential decay of into a round count.
Periods are 0-based and rounds 1-based. The demand is d : ℝ → ℝ, and is a parameter satisfying hypotheses, not a defined argmax. The noise is a single realisation ε : ℕ → ℝ, and the regret and the price-change count are numbers on it, with no expectation. The policy receives only , an argmax selector (any rule returning a maximiser of a continuous function on an interval), a pair selector (four periods per round), and the observations at the prices it charges. is rounded up. The concentration event's probability is the separate Hoeffding milestone.
The following hypotheses and repairs are added and disclosed in each item:
Four formalizations would make the goal trivial, and the statements rule each out: a policy that reads or , constants allowed to depend on or on the realisation, an argmax or pair oracle not tied to the observations, and an Assumption 2 that no realisation can satisfy (zero noise with in-block pairs satisfies it, and a sanity check exhibits a full instance).
Theorem 2 (the relaxed Assumption 2A and Algorithm 2) is not part of the mission. A complete development needs Taylor's theorem with remainder, sub-Gaussian tail bounds (available as Mathlib's HasSubgaussianMGF and the platform theorem BanditAlgorithm.subgaussian_sample_mean_tail_bound), and bookkeeping for the round schedule. The schedule lemmas and the finite-difference bound are reusable beyond this paper. Proofs of any milestone are welcome, as is a counterexample to Lemma 4's constant.
Quantum error correction protects quantum information from noise by storing it in a code and undoing the damage with a recovery operation. The textbook theory, the Knill–Laflamme conditions, characterizes codes that can be corrected perfectly. Real noise rarely admits perfect correction, and codes that are only approximately correctable can perform better than perfect ones: they can use fewer physical resources for a given target fidelity. Approximate quantum error correction (AQEC) asks for algebraic conditions that tell, from the noise and the code alone, how well a code can be corrected.
Mandayam and Ng (arXiv:1202.5139, Phys. Rev. A 2012) extend an earlier AQEC framework for subspace codes (Ng and Mandayam, arXiv:0909.0931, 2010) to subsystem codes, where information is stored in one tensor factor of a subspace and the factor is a gauge whose state does not matter. Subsystem codes include noiseless subsystems and the Bacon–Shor family, and they are the natural setting for operator quantum error correction (Kribs, Laflamme and Poulin, arXiv:quant-ph/0412076, 2005).
The system space is , with , finite dimensional; is the projector onto and the identities of the factors. The code is the set of all product states , with density operators.
The noise is a completely positive, trace-preserving (CPTP) map with Kraus operators :
Write for the support of . A recovery is a CP map that is trace preserving on .
The fidelity of states is . The fidelity loss of the code state under and compares the information in before and after:
The code is -correctable on under when some recovery has for every .
The transpose channel is the recovery with Kraus operators
the inverse square root being taken on the support of .
Suppose that, for all ,
with operators on and operators on . Then the transpose channel is a recovery, and for every
so is -correctable on whenever (operator norm). The statement holds for every choice of the operators ; each choice determines and gives a bound.
Under (12), is -correctable on for every , where
is the fidelity loss of the transpose channel. Theorem 2 is sharper than Corollary 3; the corollary trades sharpness for a quantity that is easy to compute.
The milestones follow the paper's own steps: the pure-state form (5) of the fidelity; the reduction of the worst case over to pure product states; trace preservation of on ; the trace-preservation identity of in terms of ; the fidelity formula (14) on pure product states; Theorem 2; and the bound of the expression (13) by the operator norm.
When all vanish, (12) is the paper's perfect-correction condition (Theorem 1), and the transpose channel is a perfect recovery. Corollary 3 quantifies the robustness of that statement: a perturbation of size costs at most that much fidelity loss, with an explicit recovery. This turns the search for approximate subsystem codes into a check of a matrix inequality, and it supplies the sufficient half of a characterization whose necessary half (near-optimality of the transpose channel) the paper establishes only in restricted scenarios.
Status: the results are proved in the paper, not formalized. Prove2Me's catalog has no statement of Theorem 2, Corollary 3, or of perfect-correction conditions for subsystem codes. This mission states the subsystem-code model in Lean, with mixed code states and a possibly singular , and poses each step of the paper's proof as a target. The reduction to pure states needs the joint concavity of the fidelity, which Mathlib does not have; a proof of it is reusable across quantum information theory.
Two steps resist a direct computation. First, the code contains mixed product states, while the fidelity formula (14) is available only for pure ones; the passage from one to the other is the joint concavity of , a consequence of Uhlmann's theorem, not a linear-algebra identity. Second, need not be invertible: is a pseudo-inverse, the transpose channel is trace preserving only on , and the trace-preservation identity of needs that each maps into . Arguments that treat as an inverse are wrong in general.
a × b with first, matching ⊗ₖ and the published partial trace; is a separate finite type o. The noise's Kraus operators are rectangular matrices Matrix o (a × b) ℂ, so , , are identity matrices and is 1 ⊗ₖ B i j.a → ℂ, unit when star ψ ⬝ᵥ ψ = 1; is vecMulVec ψ (star ψ).WildeQIT.fidelity , rootFidelity ), the partial trace WildeQIT.partialTraceRight, the channel action PeresTerno.krausUpdate, density matrices PeresTerno.IsDensityMatrix, and the support inverse square root and support projector QReversal.NearOpt.invSqrt, supportProj.o to a × b with . Full support of is not assumed.Matrix.Norms.L2Operator; neither the entrywise sup norm nor the Frobenius norm.The statements carry no smallness hypothesis on , quantify over all code states including mixed ones rather than over pure states only, and admit only recoveries that are trace preserving on ; each of these restrictions would make the goal weaker or trivial.
Needed infrastructure: the continuous functional calculus identities for and for range inclusions of , Kronecker-product algebra, and joint concavity (or Uhlmann's theorem) for the fidelity. Proofs of any milestone, and general fidelity lemmas usable beyond this mission, are welcome.
Mixed-integer convex programming (MICP) optimizes over sets described by convex constraints together with the requirement that some variables be integers. Modern solvers handle such problems routinely, so a modeler who wants to optimize over a nonconvex set asks a basic question first: can be written as the projection of the integer points of some closed convex set? This is the question of representability. For linear constraints with rational data it was settled by Jeroslow and Lowe in 1984: the rational MILP-representable sets are exactly the sets with rational polytopes and a finite , so each is bounded or periodic (Theorem 1.1 of arXiv:1706.05135v3). For general convex constraints no comparable description exists, and the class is much richer: it contains unbounded sets that are neither periodic nor finite unions of convex sets.
Timeline:
Fix and write points of as . A closed convex set induces an MICP formulation of when
is MICP-R if such an exists, and binary MICP-R if moreover every point of with integer has . The index set is , the projection of all of , and the -projected sets are .
The recession cone of a set is . A set is rationally unbounded if, for every and every rational affine map into , the image is either bounded or has a nonzero integer recession direction. is rational MICP-R if it has a formulation whose index set is rationally unbounded; in the polyhedral and ellipsoidal special cases, exact characterizations were obtained only under such rationality assumptions.
A set is periodic if some satisfies for every and . The diameter of is , and the MICP diameter of a formulation is .
If is closed and rational MICP-R, and there is a real with for every convex , then there are compact convex sets and closed periodic sets with
The milestones follow the paper's proof (§6) in attack order:
Theorem 5.1 is the paper's structural result for rational MICP-R sets. It shows that the set , , is not rational MICP-R although it is MICP-R, characterizes the compact rational MICP-R sets (for them binary variables suffice), and separates rational MICP from rational MILP on subsets of (Propositions 5.4, 5.5). It also gives modelers a necessary condition to check before attempting a formulation.
The results are proved on paper; none of them, and none of the representability notions, has a machine-checked formalization that we know of. The mission produces the definitional layer (formulations, index sets, rational unboundedness, MICP diameter, rational affine hulls) and the full chain of §6, which reuses general facts from convex analysis and the geometry of numbers: unimodular alignment of lattice subspaces, a flatness theorem, and separation of convex and concave functions.
The obvious induction removes integer variables one at a time by relaxing an unbounded integer direction. It breaks in two places. First, relaxing a direction can merge the sets along into a set of unbounded diameter; the proof must show that this happens only when the formulation is nearly periodic, which needs the width functions of Lemma 6.11 and the uniqueness of the asymptotic direction in Lemma 6.13. Second, slicing an index set by can destroy rational unboundedness, so the slices must be built by rational shrinking maps (Lemma 6.7) and the integrality of must be maintained by a flatness argument (Lemma 6.5). Because the index set is a projection of a closed set, it need not be closed, and its plain recession cone differs from that of its closure; the argument has to work with non-closed convex sets throughout.
Points live in EuclideanSpace ℝ (Fin n), auxiliaries in Fin p → ℝ, integer variables in Fin d → ℝ with the lattice as the image of Fin d → ℤ. Closedness and convexity of are part of "induces". Diameters are extended Euclidean diameters (Metric.ediam, value on unbounded sets), and is valued in . Rational affine maps are -matrices with -offsets; rational unboundedness quantifies over every target dimension . The recession cone is that of the set itself (the published Grunbaum2003.characteristicCone). Affine dimensions are integers with ; relative interiors are intrinsicInterior; extended-real support functions use EReal. Coordinates are -based.
Three statements carry a disclosed change: Lemma 6.4 adds (as printed it fails for ), Lemma 6.7 adds (as printed it fails in dimension ), and Lemma 6.12 reads the -projected sets of the new formulation at integer indices.
Trivializing encodings are ruled out: the diameter is not Metric.diam (which is on unbounded sets), rational unboundedness is not tested on alone, periodicity requires , the index set is the projection of all of , and are finite.
Contributions are welcome at every level: the binary characterization and the union lemma are self-contained; Lemmas 6.3–6.5 and 6.8 are reusable geometry-of-numbers and convex-analysis facts; proofs of Lemmas 6.1, 6.2 and Proposition 6.1 assemble them.
Given an unknown quantum state distributed over two systems, we determine how much quantum communication is needed to transfer the full state to one system. This communication measures the "partial information" one system needs conditioned on it's prior information. It turns out to be given by an extremely simple formula, the conditional entropy. In the classical case, partial information must always be positive, but we find that in the quantum world this physical quantity can be negative. If the partial information is positive, its sender needs to communicate this number of quantum bits to the receiver; if it is negative, the sender and receiver instead gain the corresponding potential for future quantum communication. We introduce a primitive "quantum state merging" which optimally transfers partial information. We show how it enables a systematic understanding of quantum network theory, and discuss several important applications including distributed compression, multiple access channels and multipartite assisted entanglement distillation (localizable entanglement). Negative channel capacities also receive a natural interpretation.
This mission is the statement-level formalization of Quantum information can be negative (arXiv:quant-ph/0505062v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal state merging has signed cost S(A|B) (Unnumbered main result: optimal quantum state merging and negative information, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
4 results of the paper are not stated yet, because the library lacks an interface they need:
Consider many instances of an arbitrary quadripartite pure state of four quantum systems ABCD. Alice holds the AC part of each state, Bob holds B, while D represents all other parties correlated with ABC. Alice is required to redistribute the C systems to Bob while asymptotically preserving the overall purity. We prove that this is possible using Q qubits of communication and E ebits of shared entanglement between Alice and Bob, provided that Q geq I(C;D|B)/2 and Q+E geq H(C|B), proving the optimality of the Luo-Devetak outer bound. The optimal qubit rate provides the first known operational interpretation of quantum conditional mutual information. We also show how our protocol leads to a fully operational proof of strong subadditivity and uncover a general organizing principle, in analogy to thermodynamics, that underlies the optimal rates.
This mission is the statement-level formalization of Optimal quantum source coding with quantum information at the encoder and decoder (arXiv:0706.2907v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (Method of types): all simultaneous typical-projection bounds (Theorem 5 (Method of types): all simultaneous typical-projection bounds, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
11 results of the paper are not stated yet, because the library lacks an interface they need:
We discuss the capacity of quantum channels for information transmission and storage. Quantum channels have dual uses: they can be used to transmit known quantum states which code for classical information, and they can be used in a purely quantum manner, for transmitting or storing quantum entanglement. We propose here a definition of the von Neumann capacity of quantum channels, which is a quantum mechanical extension of the Shannon capacity and reverts to it in the classical limit. As such, the von Neumann capacity assumes the role of a classical or quantum capacity depending on the usage of the channel. In analogy to the classical construction, this capacity is defined as the maximum von Neumann mutual entropy processed by the channel, a measure which reduces to the capacity for classical information transmission through quantum channels (the "Kholevo capacity") when known quantum states are sent. The quantum mutual entropy fulfills all basic requirements for a measure of information, and observes quantum data-processing inequalities. We also derive a quantum Fano inequality relating the quantum loss of the channel to the fidelity of the quantum code. The quantities introduced are calculated explicitly for the quantum "depolarizing" channel. The von Neumann capacity is interpreted within the context of superdense coding, and an "extended" Hamming bound is derived that is consistent with that capacity.
This mission is the statement-level formalization of On the von Neumann capacity of noisy quantum channels (arXiv:quant-ph/9609024v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is von Neumann capacity of the Pauli depolarizing channel (V.A, (5.18): von Neumann capacity of the Pauli depolarizing channel, PDF p. 11). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper, we present a new entanglement monotone for bipartite quantum states. Its definition is inspired by the so-called intrinsic information of classical cryptography and is given by the halved minimum quantum conditional mutual information over all tripartite state extensions. We derive certain properties of the new measure which we call "squashed entanglement": it is a lower bound on entanglement of formation and an upper bound on distillable entanglement. Furthermore, it is convex, additive on tensor products, and superadditive in general. Continuity in the state is the only property of our entanglement measure which we cannot provide a proof for. We present some evidence, however, that our quantity has this property, the strongest indication being a conjectured Fannes type inequality for the conditional von Neumann entropy. This inequality is proved in the classical case.
This mission is the statement-level formalization of "Squashed Entanglement" - An Additive Entanglement Measure (arXiv:quant-ph/0308088v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Superadditivity and tensor-product additivity (§II, Proposition 4 (p.1 seed), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
In previous papers, we expressed the Entanglement of Formation in terms of Conditional Mutual Information (CMI). In this brief paper, we express the Entanglement of Distillation in terms of CMI.
This mission is the statement-level formalization of Entanglement of Distillation and Conditional Mutual Information (arXiv:quant-ph/0202144v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Common-cause classical laws have zero CMI (§2, Eq.(5), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
These results of the paper are already proved in Mathlib, so they are not open goals here: InformationTheory.klDiv_comp_right_le.
We investigate entanglement measures in the infinite-dimensional regime. First, we discuss the peculiarities that may occur if the Hilbert space of a bi-partite system is infinite-dimensional, most notably the fact that the set of states with infinite entropy of entanglement is trace-norm dense in state space, implying that in any neighborhood of every product state there lies an arbitrarily strongly entangled state. The starting point for a clarification of this counterintuitive property is the observation that if one imposes the natural and physically reasonable constraint that the mean energy is bounded from above, then the entropy of entanglement becomes a trace-norm continuous functional. The considerations will then be extended to the asymptotic limit, and we will prove some asymptotic continuity properties. We proceed by investigating the entanglement of formation and the relative entropy of entanglement in the infinite-dimensional setting. Finally, we show that the set of entangled states is still trace-norm dense in state space, even under the constraint of a finite mean energy.
This mission is the statement-level formalization of On the quantification of entanglement in infinite-dimensional quantum systems (arXiv:quant-ph/0112064v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 10: no separable ball under a strict mean-energy bound (Proposition 10: no separable ball under a strict mean-energy bound (seed paper result), PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
Interior-point methods minimize a linear function over a convex set by following the minimizers of , where is a self-concordant barrier for . The number of Newton steps the path-following method needs to reach accuracy is , where is the barrier's self-concordance parameter. A smaller is a better iteration bound, and the question of the smallest achievable for an arbitrary convex domain is a basic question of the theory.
A convex domain is a convex set with non-empty interior; it is proper if it contains no line with . need not be closed or bounded. For the polar set of with respect to is
a convex body, and the universal barrier is .
A function on is a barrier if as . A convex, three times continuously differentiable is self-concordant if, for all and ,
and -self-concordant if moreover (2).
The proof works with one-dimensional laws. For a convex body and , the marginal density is the density of for uniform on . For a density on , is its mean, its variance and its third central moment; . A density is -concave if is concave on its support (for : is constant on its support, up to endpoints).
The parameter is exact, so the goal carries no constant to improve.
The theorem settles the self-concordance parameter of the universal barrier for every proper convex domain: it is , and by the lower bound of Nesterov and Nemirovski no barrier does better in general. It implies the -self-concordance results for cones as special cases, and it gives a canonical barrier attaining the optimal iteration bound on any domain. Proposition 1, a pair of sharp moment inequalities for -concave distributions, is of independent interest; it extends the third-moment bound for log-concave laws used by Bubeck and Eldan.
The result is proved on paper; none of it is formalized. A complete development would give machine-checked statements of the universal barrier, its derivative formulas, Brunn's principle for hyperplane sections, and the moment inequalities, all of which are reusable for other barrier constructions (the entropic barrier missions on the platform use the same definitions of barrier and self-concordance). The two polynomial inequalities (milestones 4 and 7) are self-contained and the appendix proof of Lemma 4 is long elementary calculus, a natural target for automation.
The derivative formulas reduce -self-concordance to moment inequalities for the marginal of the polar body. The obvious argument uses only log-concavity of marginals (Prékopa–Leindler) and the log-concave third-moment bound; it yields and loses a constant. Exactness requires the stronger -concavity and moment bounds that are sharp for every , attained by on . Proposition 1 is an extremal problem over an infinite-dimensional class of densities, and the sharp constants surface only as polynomial inequalities in a parameter whose degree grows with (milestones 4 and 7); Lemma 4 must hold uniformly in the integer , and small behave differently. The localization lemma the paper cites for the reduction is not in Mathlib. On the analytic side, Lemma 1 requires differentiating three times under the integral for a possibly unbounded .
The space is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume. The goal's conclusion is the published predicate EntropicBarrier.Universal.IsNuSelfConcordantBarrier K φ n: barrier limits at every frontier point within ; convexity, and inequality (1) on through the published line-restriction form ConvexOptimization.IsSelfConcordantOn; and (2) in one-sided form, equivalent to the two-sided one. Lemma 1 uses Fréchet derivatives iteratedFDeriv. The universal barrier is a total function; its values off are junk and never read. All of 's standing assumptions (convex, non-empty interior, no line) are bundled in IsProperConvexDomain, together with .
Three conventions correct slips of the page and are disclosed in each item:
Densities are non-negative functions with integral , and moments are Bochner integrals; a -concave density has bounded support, so they are genuine. Not formalized: Brunn's principle for general , the localization lemma (Theorem 3) and its corollaries, the limiting reductions of §4.1.1–§4.1.5 and §4.2.1, and the internals of Appendix A. Contributions of any of these as supporting lemmas, of Brunn–Minkowski-type tools for sections, and of differentiation-under-the-integral results for polar volumes are welcome.
A retailer that sells substitutable products must decide, for each arriving customer, which subset of products to display. Customer preferences are unknown at the start and have to be learned from purchases, while every suboptimal display costs revenue. This is dynamic assortment planning, a standard problem of revenue management in e-commerce and online advertising, and its learning version is a bandit problem whose arms are the subsets of products.
Under the multinomial logit (MNL) choice model the problem has been studied through the regret of a policy over customers (Chen, Wang and Zhou, §2 and Table 1):
In the capacitated model the regret must grow with . Chen, Wang and Zhou (arXiv:1805.04785v2, Mathematics of Operations Research 2021) show that without a capacity constraint it need not: a trisection policy achieves regret with a universal constant, and is a lower bound. This mission formalizes the upper bound.
There are items with known revenues and unknown utilities ; the no-purchase option has utility . In each period the retailer offers an assortment , and the customer buys with probability or buys nothing with probability , independently of the past. The expected revenue of is
and the regret of a policy is , where maximizes over all subsets.
The policy rests on two objects. The level set collects the items whose revenue is at least . The revenue potential is a piecewise-constant function of one real variable. Its maximum is , its right limit is , and denotes the fixed point .
The adaptive-confidence trisection policy keeps an interval , starting from . In epoch it forms the points and , at distance , and runs inner iterations. Each inner iteration does two things:
At the end of the epoch the policy sets if , and otherwise. The policy knows and but never .
There is a universal constant such that for every , every horizon , all and all , the adaptive-confidence trisection policy satisfies
No gap condition and no bound on is assumed. The constant is left unspecified, as in the paper.
Theorem 3, together with the lower bound of Theorem 4, settles the minimax regret of uncapacitated MNL assortment learning at , independent of the number of products. The policy uses no estimate of the individual utilities, and its cost per period is one level-set offer, so it applies to catalogues where is large compared with . The structural lemmas on the revenue potential (Lemmas 1–4) are standard tools for MNL assortment problems and are reusable by other missions on static and dynamic assortment optimization. Lemma 8 is a MOSS-style concentration inequality whose confidence level grows with the sample size; it is the device that removes the factor of the paper's baseline bound (Theorem 2).
The result is proved in the paper and is not presented as open; no machine-checked proof of any part of it is known. The platform has the MNL model, the UCB policy of Agrawal et al. (whose bound depends on ) and Hoeffding's inequality, but no level-set or trisection analysis. A formal proof would also check the paper's argument, whose printed slips are recorded in the scope section.
The regret concerns a stateful algorithm whose epochs end at random times: an inner iteration takes two periods while exploration is active and one afterwards, and the policy's internal state must be recomputed from the purchase history alone. The obvious argument fixes a confidence level , bounds each epoch's regret on the event that all confidence intervals hold, and sums a geometric series. That argument loses a factor, and it is the paper's own Theorem 2. Removing the factor needs confidence levels that weaken as data accumulate. A failure is then no longer rare enough to be ignored, so the analysis has to track its cost. This is done by a recursion on conditional expected regrets across three cases (interval to the right of, containing, or to the left of ), in which a wrong decision in one epoch passes to another case with controlled probability. Within an epoch, the purchases made while exploring a level set must be shown to behave like i.i.d. samples with mean , although the number of explorations is itself random.
MNLBandit.UCB.Setting with every subset admissible: histories are sequences of choices in Option (Fin N) (none = no purchase), policies are deterministic functions of the past choices, and expectations are finite sums over histories. Items and periods are 0-based in Lean; epochs and inner iterations are as on the page.Function.rightLim.An object is hidden in one of boxes. Each search of box costs time , and if the object is there it is found with probability , independently of all earlier searches. When the searcher knows the probabilities with which the object was placed, the problem has a classical index solution. Norris (1962), Bram (1963), Blackwell (reported by Matula, 1964), Black (1965) and Ross (1983) showed that it is optimal to search, at every step, a box maximizing the current Gittins index , where is the number of failed searches of box so far. Ross also showed the converse: only such sequences are optimal.
The adversarial version replaces the known prior by a hider who chooses the box to maximize the expected time to detection, while the searcher minimizes it. Because overlook is possible, a pure search strategy must be an infinite sequence of boxes. This zero-sum search game goes back to Bram (1963) for unit search times, and it belongs to the search games against an evader in a stationary search space surveyed in Book 1 of Alpern and Gal (2003).
Timeline.
There are boxes with search times and detection probabilities .
Pure strategies. A pure strategy of the hider is a box. A pure strategy of the searcher is a search sequence . If the hider is in box , the expected time to detection is
where is the number of searches of box among the first .
Mixed strategies. A hiding strategy is a probability vector in the simplex . A search strategy is a probability mass function on , and . Against a sequence , a hiding strategy earns the hider .
Value and optimal strategies. The value is
A hiding strategy is optimal if it attains . A search strategy is optimal if for every box .
Gittins search sequences. , the set of Gittins search sequences against , consists of the sequences that always search a box of maximal Gittins index.
Tie-breaking by one ordering. A permutation lists the boxes in order of preference. is the Gittins search sequence against that, whenever several boxes have maximal index, searches the one lists first. Then
has at most elements, whereas can be uncountable.
For every optimal hiding strategy there is a search strategy with
The goal fixes no constants. It asserts that an optimal search strategy exists, and that one can be found among mixtures of at most elements of .
The result. In the searcher's pure strategy space is uncountable, so the existence of an optimal search strategy is not automatic. The standard theory of semi-finite games gives only -optimal strategies. Theorem 6 settles existence for general search times. Theorem 10 reduces the search for an optimal strategy to the finite set .
The paper's computational section builds on this reduction. For interior , optimality of in is equivalent to optimality in the finite matrix game, which a linear program solves (Proposition 11). This is also the basis of the paper's bounding algorithm. Theorem 10 extends Gittins' two-box, unit-time Proposition 8.5 to any number of boxes and arbitrary search times.
Formalizing it. The results are proved on paper. To our knowledge none is machine-checked. The Blackwell–Ross index theorem is the only ingredient already proved on the platform. This mission formalizes:
The obvious route to existence is the -game argument of Blackwell and Girshick: if the set of payoff vectors is closed, the infimum over its convex hull is attained, and Carathéodory gives a mixture of at most points. For general search times no such closedness argument is available for itself: its payoff vectors are unbounded, and a sequence that neglects a box has an infinite coordinate. The paper therefore restricts to Gittins sequences against hiding strategies bounded away from the boundary, and adds pseudo-strategies that dominate everything near the boundary. Closedness of the resulting set rests on the continuity of . This map is discontinuous at tie points in general and is continuous only along the cones (Lemma 17).
For Theorem 10, the natural idea is that every Gittins sequence is a mixture of the . That is false pathwise. Lemma 9 replaces it with a statement about extreme points of .
Representation.
Fin n and searches are 0-indexed (ξ : ℕ → Fin n).stdSimplex ℝ (Fin n), boundary included.PMF (ℕ → Fin n).ℝ≥0∞).AllocationIndices search-problem definitions, with cost . Blackwell's theorem is the published AllocationIndices.search_index_optimal.Tie-breaking.
[NeZero n], which is implied by the simplex being nonempty.Real vectors. , and are real vectors, obtained via toReal. They are used only for interior , where every coordinate is finite.
Trivializing readings, all excluded. None of the following is used:
Infrastructure and contributions. A complete development needs:
convexHull_eq_union) and Krein–Milman (Mathlib closure_convexHull_extremePoints);The -game theorem and the semi-finite minimax theorem are reusable well beyond search games. Proofs of any milestone, and of these general tools as separate lemmas, are welcome.
A retailer who sets a price for a product with limited inventory usually learns about demand from past sales. When the shelf runs empty, sales record the inventory level rather than the demand. Demand above the stock is lost and never observed. This demand censoring is pervasive in retail and inventory data, and it biases naive estimators of demand curves (Besbes and Muharremoglu, Management Science 2013; Ban, Operations Research 2020). Bu, Simchi-Levi and Wang (SSRN 3619625; Management Science, doi:10.1287/mnsc.2022.4382) ask a basic question about offline (historical) data. The retailer has censored sales at a few past prices and must choose a single new price. When can it, with enough data, guarantee near-optimal revenue no matter what the unobserved part of the demand distribution looks like? The paper answers this exactly, and gives an algorithm that achieves the guarantee whenever it is achievable.
The retailer has units of inventory and chooses a price in a known interval . Demand is linear: , where the base demand is random with c.d.f. , and the price sensitivity lies in a known interval . Demand is nonnegative almost surely at every feasible price. Sales are , and under a c.d.f. of the expected revenue is .
Offline data. different historical prices were used with inventories . At pair there are independent censored sales . The data size is . A value of is observable only below the observable boundary . Write , which is assumed positive. Assumption 1 asks that, below , is either discrete with finitely many atoms or has a density, with a slope or density lower bound .
Ambiguity set. No amount of censored data reveals on . The set of distributions consistent with the data is . The optimistic and pessimistic revenues are and . Their largest maximizers on are the optimistic price and the pessimistic price . With the largest maximizer of , the worst-case revenue loss of a price is .
Identifiability. A data-driven algorithm maps the censored data and the public inputs (, the two intervals, the pairs ) to a feasible price . The problem is identifiable (Definition 1) if some algorithm satisfies for every .
The problem is identifiable if and only if
The Lean goal states this in three parts, for every instance satisfying the standing assumptions:
Theorem 1 separates censored-data pricing problems into two classes. In identifiable ones, more data eventually yields near-optimal prices. In the others, a positive loss persists however large the sample, and the right benchmark is the minimax loss . The criterion is checkable in terms of two robust optimization problems, the maximax and the maximin. The constructive half comes with an algorithm that uses only observable data and has sample complexity , matching data-driven newsvendor results without censoring (Levi, Perakis and Uichanco, Operations Research 2015).
The results are proved in the paper. None of them, and none of the model, is formalized. The mission formalizes the model, the ambiguity set, the algorithm and the full chain of the proof. It includes two concentration inequalities not yet available in Lean in the needed form: DKW with Massart's constant for distributions with atoms, and a uniform bound over monotone function classes.
The algorithm sees only the censored data. A proof that silently uses or to pick the price does not establish the theorem. The obvious estimator of , least squares on observed sales, is biased by censoring. D2ACD instead regresses empirical quantiles at the level , below which the data are uncensored. Its analysis needs a lower bound on the slope of the c.d.f. (Assumption 1), and a uniform-in-price comparison of piecewise empirical revenues whose breakpoint is itself random. On the other side, the lower bound requires the exact extremal distributions in . The optimistic one sends the unobserved mass beyond every relevant demand level. The pessimistic one puts it at the boundary .
Representation. c.d.f.s are probability measures on . means agreement with on every half-line , , so an atom at is allowed. , , the worst-case loss and are defined as suprema and infima. Their attainment is part of the milestones, so no statement is true through a junk value. "" is the supremum of the set of maximizers. The data are base-demand samples under the product law, mapped to censored sales. An algorithm is a function of the sample sizes and the censored sales for fixed public inputs. Failure probabilities are outer measures. The limit is over all sample-size vectors with .
Standing assumptions and disclosed choices. The data equation is ; the page drops once. The continuous branch of Assumption 1 bounds the density on , with a lower bound of the support. The printed contradicts nonnegative demand together with . The historical prices are pairwise different, as the text says. The finite-sample statements (Lemmas 1, 2, Theorem 2) are made on the data assumption for all , as on p. 10; the goal is not. In D2ACD, is the clamp of the least-squares slope to , which is the arg min of line 9. Ties go to the largest price and the least index. The output is when some sample is empty.
Trivializing readings ruled out. Definition 1 fixes the instance before asking for an algorithm, so a constant algorithm returning witnesses the bare equivalence. For that reason the goal names D2ACD, a definition taking only the public inputs and the censored sales, and states the quantitative lower bound for the other direction. Two sanity instances, one discrete and one uniform, satisfy every standing assumption, so the hypotheses are not vacuous.
Contributions welcome. Proofs of any milestone. The concentration lemmas A.2 and A.3 are reusable well beyond this mission. Propositions 1–3, 6 and 7 are deterministic convex-analysis arguments about the two robust revenue curves and are a natural starting point.
Models of Bayesian social learning describe agents in a network who each receive a private signal about an unknown state of the world, observe the actions of their neighbours over time, and act optimally given everything they have seen. They are used in economics, operations research and the study of collective decision making to ask whether groups aggregate dispersed information, and they presuppose that every agent can carry out the Bayesian update. Hązła, Jadbabaie, Mossel and Rahimian (arXiv:1705.04770, Operations Research 2021) show that this presupposition fails in general: already at the second round of interaction, computing a Bayesian agent's action is NP-hard (their Theorem 1). The proof is a reduction from approximate VERTEX-COVER. This mission formalizes the mathematical core of that reduction: in the network built from a graph, the belief of one designated agent at time two is pushed to opposite extremes by graphs with small vertex covers and by graphs whose vertex covers are all large.
A finite set of agents is given, and every agent has a neighbourhood of agents whose actions she observes, with . The state is , drawn from the uniform prior . Agent receives a private signal with law ; conditionally on the signals are independent, so a signal profile has probability .
At every time agent knows her own signal and the actions of all at times . Her information set is the set of profiles that agree with in and in all those actions. Her belief is the posterior (4)
and in the binary action model (utility ) her action is the more likely state, with ties broken towards . Actions at time depend on information sets at time , which depend on actions at earlier times, so all of these are defined together by recursion on . The log-belief ratio is .
The reduction network for a simple graph with vertices and edges has agents: a vertex agent for each vertex, observing only herself, with and ; an edge agent for each edge , observing , and herself, with an uninformative signal; an agent observing only herself; and the agent , with an uninformative signal, observing and all edge agents. With , and , agent 's signal is chosen so that
Agent 's observed history is: every edge agent announces , and announces .
There are and such that for every , every graph on vertices, every admissible signal structure of , and every signal profile producing the observed history:
The constant is not fixed: the paper writes .
Theorem 6 is the step that turns a statement about vertex covers into a statement about beliefs. Together with the NP-hardness of distinguishing graphs with a vertex cover of size from graphs with no vertex cover smaller than (Theorem 5, from Khot, Minzer and Safra's proof of the 2-to-2 games theorem), it shows that no polynomial-time algorithm computes the time-two action of a Bayesian agent unless P = NP, and that even approximating the belief is hard, since the two cases differ by exponentially small versus exponentially close to one. This sets a limit on rational-agent models of social learning as descriptions of behaviour and motivates bounded-rationality alternatives.
The result is proved in the paper; to the best of current knowledge it has not been formalized. The mission produces a machine-checked model of Bayesian group decision making on a network, with information sets defined by recursion on time, reusable for other results about Bayesian learning on graphs, and a finite Chernoff bound in Kullback–Leibler form. The NP-hardness itself is not part of the mission: it needs a model of computation and inherits its hardness from a cited theorem.
The model's information sets are defined by a recursion in which every agent simulates what every neighbour could have seen. The first obstacle is to compute the time-two information set of agent in closed form: one must check that the actions of agent and at earlier times, and of the edge agents at time zero, carry no additional information, and that the edge agents' time-one actions reveal exactly whether the vertex signals form a vertex cover. Then the posterior becomes a ratio of two weighted counts of vertex covers. A naive bound comparing the two sums term by term does not separate the YES and NO cases, because the sums are dominated by different covers; in the YES case the large covers must be discarded using a tail bound whose exponent beats the likelihood of a single small cover, which is where the constants enter.
States, signals and actions are Bool (false = 0). A network is BinNet (neighbourhoods with , and ); post, mapAct, infoSet, act, logBelief are (4), the MAP action with ties to , , and . Information sets contain the conjunct from the history of (1). The reduction network is vcNet G k₀ k₁ for G : SimpleGraph (Fin n), on the agent type Agent n G (vertex agents, edge agents indexed by G.edgeSet, iAg, kap), with quantified over all pairs in with . Vertex covers are Mathlib's SimpleGraph.IsVertexCover. Decimals are exact rationals; , , are compared as real numbers. Probabilities of events on the vertex signals are written as finite sums of over subsets . is the published bernoulliRelativeEntropy. is the number of graph vertices, not of agents.
The goal is about the model's own posterior on the model's own information set, for every profile on which the model's actions produce the history; it is not stated about a hand-written ratio of sums, which would skip the model. The constants and are quantified before the graph and before 's parameters, so they cannot depend on the instance. The complexity clauses of Theorem 6 (a polynomial-time reduction, the bounds (9)) and Theorem 1's NP-hardness are not formalized.
Contributions welcome: closed-form computations of early information sets in the model, the finite Chernoff bound (Theorem 7; the published Proved MassartDKW.Binom.comment_3 is the strict-tail Cramér–Chernoff bound for binomial n p), and the numerical inequalities of (16) and (17).
The symmetric traveling salesman polytope is the convex hull of the incidence vectors of all Hamiltonian cycles of the complete graph . Minimizing a linear cost over it is the traveling salesman problem, and polyhedral methods for the TSP (cutting planes, branch and cut, LP relaxations and their integrality gaps) depend on linear inequalities that are valid for and, ideally, define its facets. Known facet classes include the comb, clique-tree, path and crown inequalities; Naddef's survey (Naddef 2007) collects them.
Circulant TSP instances are those whose edge costs depend only on the edge's length around a circle of equally spaced cities. Gutekunst and Williamson (SIAM J. Discrete Math. 2019) showed that the subtour LP has integrality gap exactly on circulant instances; the witnessing family of LP solutions is cut off by several known facets, but not robustly under small modifications. They conjectured an inequality, now called the circlet inequality, that would cut off the whole family. The paper of this mission (arXiv:2012.12363v1) proves that conjecture and shows the inequality is facet defining when . Its coefficients are themselves circulant, a property shared among classical facets only by the crown inequalities of Naddef and Rinaldi (Math. Oper. Res. 1992).
Timeline. 2019: Gutekunst and Williamson characterize the subtour LP gap on circulant instances and conjecture Inequality (2). 2020: Gutekunst and Williamson prove validity (Theorem 3.1) and the facet property (Theorem 5.1) for , and compute the inequality's strength.
Fix cities , edges of , and . The length of the edge is
an integer in . For a vector and , is the total weight on edges of length . A Hamiltonian cycle visits every city once and returns; its incidence vector marks its edges, and
For the circlet coefficients are for odd and for even (for : ), and the circlet inequality is
An inequality is valid for if every point of satisfies it, and facet defining if moreover the face has .
In the Lean development, cities are Fin n, a Hamiltonian cycle is an ordering π : Equiv.Perm (Fin n), its incidence vector is MetricTSP.tourVec π, STSP n is the convex hull of these vectors, lenCount n i x is , coeff n i is and circletForm n x is .
For every positive with :
Every Hamiltonian cycle on cities, , satisfies (2). The proof is by minimal counterexample and runs through the milestones Claim 3.2 (the base case ), Lemma 3.3 (a violating cycle has ), Lemma 3.4 (a minimal violating cycle contains none of three local edge patterns), and the window count with .
Lemma 3.4 is proved by contracting four vertices of a cycle containing one of the patterns and showing the cost drops by at least : Claims 4.1 and 4.2 (symmetries), Proposition 4.3 (surviving edges never get more expensive), Propositions 4.4 and 4.5 (the five contracted edges), and the resulting contraction step.
The dimension (cited on p. 19 from Naddef and Rinaldi, Theorem 3.7), and a family of tight Hamiltonian cycles with linearly independent incidence vectors.
The circlet inequality is a facet of whose coefficients depend only on edge length, so it is invariant under rotation of the city labels. It resolves the circulant TSP conjecture of Gutekunst and Williamson and removes from the subtour LP every member of the canonical family of solutions that witnesses the integrality gap on circulant instances, a class of TSP instances for which relatively little is known. Since any relabelling of the cities gives another valid inequality, it supplies on the order of facets of . The validity proof also gives a self-contained example of a minimal-counterexample argument by vertex contraction, a technique common in polyhedral combinatorics.
The result is proved in the paper; it has not been formalized. This mission produces machine-checked statements of the validity theorem, the facet theorem, and every intermediate result their proofs use, together with a reusable formal model of , edge lengths on a cycle, and facets of polytopes built from tour incidence vectors. The dimension of is a classical cited result that, to the best of current knowledge, has no formal proof either; it is included as a target in its own right.
Validity is not a local statement. A Hamiltonian cycle may use edges of any length, and the coefficients alternate between and with parity, so no edge-by-edge or degree-by-degree bound works: the inequality is tight on cycles that mix lengths , and one other length. The paper's argument needs the global structure of the cycle twice, once to rule out the patterns of Figure 4 in a minimal counterexample (where a parity argument on a four-group quotient graph handles the hardest equality case of Proposition 4.5) and once to count windows. The contraction step requires checking that the contracted object is again a Hamiltonian cycle and tracking costs on two different vertex sets with different moduli and .
For the facet half, exhibiting the tight tours is explicit, but proving the linear independence of incidence vectors for all and proving the dimension of are substantial linear-algebra arguments. The paper's own justification of independence for the first family is inaccurate (a length- edge is shared by two rotations), so a correct argument has to be supplied.
Fin n with 0-based labels; lengths and costs depend only on label differences, so the shift from changes nothing. The contraction results (Propositions 4.3–4.5, the contraction step) use the paper's 1-based labels in ℕ, with integer lengths and costs, and refer to a cycle's edges through the label of each vertex ().Fin n → Fin n → ℝ (ordered pairs); the incidence vector is symmetric with zero diagonal, and affine dimension is the same as in . counts each unordered edge once.Disjunctive.Polarity.IsFacet (extreme, nonempty, dimension one less), and the goal conjoins validity, since a face of codimension one is also cut out by the reversed inequality.A quantum computer executes a fixed, finite instruction set of gates, while quantum algorithms are written with arbitrary gates. Every algorithm must therefore be compiled: each gate is replaced by a sequence of available instructions whose product approximates . If an accuracy required sequences of length , compiling an -gate algorithm to overall accuracy would cost instructions, which would erase quadratic speed-ups such as Grover's search. The Solovay-Kitaev theorem says the cost is only polylogarithmic in , for every instruction set, and the Solovay-Kitaev algorithm finds the sequences efficiently. It is the standard justification for treating the choice of a universal gate set as immaterial in quantum complexity theory.
Timeline. Solovay announced the theorem for in 1995 on an email list, without a subsequent paper. Kitaev outlined a proof for in 1997 (Kitaev 1997), with an algorithm. Nielsen and Chuang's textbook (2000, Appendix 3) gave a detailed proof, and Kitaev, Shen and Vyalyi (2002) gave two algorithmic variants, one with sequence length . Dawson and Nielsen (2005, arXiv:quant-ph/0505030) gave the self-contained pedagogical account of the theorem and algorithm, for qubits and qudits, which this mission formalizes; their algorithm yields length .
Fix a dimension . is the group of complex unitary matrices of determinant , and is the adjoint. The distance between gates is the operator norm of their difference,
A sequence of gates also denotes the unitary , and is its length; is an -approximation to when .
An instruction set for (Definition 1) is a finite set such that
The Solovay-Kitaev algorithm is a recursion of depth . At depth it returns a stored basic approximation of bounded length . At depth it computes , decomposes approximately as a balanced group commutator with close to the identity, and returns the concatenation of five sequences computed at depth . The accuracies satisfy and the lengths .
For every instruction set for there is such that for every and every some sequence of gates from satisfies
Theorem 1 of the paper asserts length for some ; the goal fixes , the exponent the paper's algorithm attains (Eq. (8), and §5.1 for qudits). is left unspecified, as in the paper.
In attack order: the inverse-sequence fact (p. 3); (p. 3); the base case, bounded-length -approximations (p. 5); Lemma 1, the error of an approximated group commutator (Eq. (14)); Lemma 2, a traceless Hermitian is a commutator with ; Lemma 3, ; the logarithm of a gate near the identity (p. 12); the balanced approximate commutator in , Eq. (33); the recursion invariant of the algorithm (Eqs. (1)–(2), (15), (21)–(22)); the closed form of (Eq. (4)); and the depth/length trade-off (Eqs. (7)–(8)).
The result. Theorem 1 makes universality quantitative. Any two universal instruction sets simulate each other with polylogarithmic overhead, so the class of efficiently computable quantum functions does not depend on the gate set, and fault-tolerant architectures may restrict themselves to a small set of protected gates. The algorithm turns the existence statement into a compiler with polylogarithmic running time.
Formalizing it. The theorem is proved, and the paper's argument is complete apart from constants it declares "tedious … easy to supply". The paper is not machine-checked, and the platform has no version: an open goal from Childs's lecture notes (QAlgorithms.Childs.solovayKitaev) concerns circuits of one- and two-qubit gates up to global phase with an unspecified exponent, and proved items cover commutator estimates only. This mission produces the qudit statement with the explicit exponent , the commutator estimates of Lemmas 1–3 in arbitrary dimension, and an explicit model of the recursion. The paper's constants are only approximate (, ); rigorous values are a welcome by-product.
The obvious argument, approximating with ever longer sequences from a dense subgroup, gives no rate at all: density says nothing about how long sequences must be. The rate comes from an error-cancellation effect: if are at distance from the identity and are approximated to accuracy , their group commutator is approximated to accuracy , better than the inputs (Lemma 1). Making this work needs (i) a decomposition of every gate close to the identity as an approximate balanced commutator in , which requires a matrix logarithm, the commutator representation of traceless Hermitian matrices (Lemma 2), and a third-order Baker-Campbell-Hausdorff estimate (Lemma 3); and (ii) a uniform base case, which needs compactness of to turn pointwise universality into a single length bound . The paper's derivation of Eq. (33) also contains a sign slip: with the commutator approximates instead of , which a formal proof must repair.
Gates are elements of Matrix.specialUnitaryGroup (Fin d) ℂ; Lemma 1 is about matrices in the unitary group. The distance is the operator norm QAlgorithms.specNorm from the published definition QAlgorithms_Defs_Basic, never Mathlib's entrywise matrix norm. Sequences are lists, their unitary is the list product , and the inverse sequence is the reversed list of inverses. Instruction sets are Finsets closed under inverses; universality is the paper's own gloss of Definition 1, part 3 ("for every and a product of gates from is an -approximation"). The exponential is NormedSpace.exp on complex matrices. The algorithm is a Lean function of two routines: a lookup basic and a decomposition gc, indexed by the recursion level because GC-Approx-Decompose's guarantee is relative to the current accuracy.
Conventions and additions, all disclosed in the items: becomes so that bounds are meaningful for every (same -class); the paper's approximate constants (, , , ) are existential and chosen before and ; the logarithm milestone adds (needed by Lemma 2) and (the proviso of p. 3); the identity is not stated, since as printed it fails for .
Trivializing formalizations are ruled out: must be closed under and must consist of gates from ; the constant is quantified before and , so it cannot depend on them; in the recursion invariant the base routine has a fixed length bound and the decomposition routine is constrained by the accuracy bounds, not assumed to be exact.
Running time (Eqs. (3), (6), (9), ) is out of scope: there is no machine model. Needed infrastructure: compactness of (Mathlib has no instance at this revision), a principal logarithm near the identity, operator-norm estimates for products and exponentials, and spectral facts about Hermitian matrices. The commutator and exponential estimates are reusable beyond this mission. Proofs of any milestone, and sharper constants, are welcome.
Mixed-integer programs often contain general integer variables . A standard modelling device replaces such a variable by binary variables linked to through a polytope, a binarization. Examples are the unary encoding, the "full" encoding with one indicator per value, and the logarithmic encoding . Binarizations let cutting-plane and branching techniques built for 0/1 variables, such as lift-and-project and sequential convexification, act on general integer programs. Computational experience with such encodings is mixed. A logarithmic encoding uses the fewest variables, but it is not obvious that it should help or hurt the strength of the relaxation. Dash, Günlük and Hildebrand (Mathematical Programming 170, 2018) studied split cuts in binary extended formulations. Aprile, Conforti and Di Summa (arXiv:2106.00354, Mathematics of Operations Research, 2024) introduced a rank that measures how many convexification steps on the binary variables are needed to remove fractional values of , and compared binarizations by it.
The underlying operation is Balas's sequential convexification (Balas, Discrete Applied Mathematics 89, 1998; doi:10.1016/S0166-218X(98)00136-X): for a polytope , replacing by for in turn yields the convex hull of the mixed 0/1 points.
A point is written . A polytope is the convex hull of finitely many points; is its vertex set and two vertices are adjacent when the segment joining them is a face of . The skeleton is the resulting graph.
For a polytope with some coordinates restricted to , write . The lift-and-project rank is the least such that some indices satisfy .
A polytope is a binarization of in the range , , if the -values of its points with are exactly . For a number let . Given integers and points , the rank of is
with the lift-and-project rank taken with respect to . It counts the -convexifications needed to cut off every point of whose -value lies strictly between and for some .
is a -hypercube binarization if its vertices project onto in the -space and onto in the -space, so that the vertices of correspond one-to-one to those of the -cube, each with its own integer -value. The logarithmic binarization is
For every -hypercube binarization and all ,
The milestones follow the paper's development:
where counts coordinate directions in which no edge of crosses any level .
The theorem gives a precise sense in which the logarithmic encoding is the best among all encodings of an integer variable whose binarization has the combinatorics of a cube. It is not only the most compact one: it also requires the fewest sequential convexification steps on the binary variables to remove any prescribed family of fractional -intervals. Combined with Corollaries 4.19 and 4.22, it yields the explicit formula . In particular, for every even . By Theorem 4.23 this extends to every hypercube binarization a result of Owen and Mehrotra (Operations Research 50, 2002) on the logarithmic encoding: convexifying all but one of the -variables of does not ensure integrality of .
The result is proved in the paper. No machine-checked version exists. The mission formalizes the vertex-and-edge view of sequential convexification that the paper's proofs rest on: Balas's theorem for V-polytopes, lift-and-project rank as a hitting set, and the hypercube graph of a binarization with its cut structure. Mathlib has convex hulls, extreme points and extreme subsets, but no face lattice of polytopes, no skeleton graph and no hypercube graph. Platform results on Balas's theorem exist only for H-polyhedra with explicit bound rows.
The comparison is between an arbitrary hypercube binarization and a specific one. Direct computation of for an arbitrary is not possible, because the polytope depends on the whole edge structure of , and the skeleton of a hypercube binarization need not be the cube graph: it can contain extra edges. The step that has to be bridged is from the lift-and-project rank of a polytope to a statement about cuts in the hypercube graph . That requires the vertex description of sequential convexification, the location of vertices of fractional slices on edges of , and the reduction from the skeleton to the subgraph . A natural first idea, comparing the polytopes and through an affine map, fails: a general hypercube binarization is not affine, and by Lemma 4.16 of the paper is, up to symmetry, the only affine one.
The Lean development fixes the following conventions.
p : Fin (d+1) → ℝ, with = p 0 and = p i.succ. Coordinates of are indexed from , so the weight of is 2 ^ (i : ℕ).Set.extremePoints, and edges are the published Hirsch.Adj.Disjunctive.HigherDim.SplitConvexify and IteratedSplit.lpr Q H is defined for any set H of 0/1 coordinates, with repetitions allowed in the sequence of convexified variables, as an sInf that Theorem 2.1 shows is attained.rk B xbar takes the fractional points as an argument. Every statement about it quantifies over all admissible choices, and in the goal the choices for and are independent.A formalization in which the rank of is a junk value (an empty set under sInf, or convexification over the wrong coordinates) would make the goal trivial. The definitions were checked against this: a sorry-free verification file proves and that is a -hypercube binarization.
A complete development needs:
The polytope and edge results, including the vertex form of Balas's theorem, are reusable well beyond this paper. Contributions proving any milestone, or general lemmas on vertices of hyperplane sections and on projections of polytopes, are welcome.
Selecting a valuable subset subject to several simultaneous restrictions is a common combinatorial optimization problem. A facility may contribute less after nearby facilities have already been selected; a collection of observations may provide overlapping information. Such diminishing returns are captured by submodular objectives. Matroid constraints describe families of admissible selections that are closed under deletion and satisfy an exchange rule. Requiring a selection to satisfy several matroids permits overlapping restrictions on the same elements.
Lee, Sviridenko and Vondrák study this model with access to objective values and independence tests through oracles. Their main monotone guarantee is a polynomial approximation factor of for any fixed number of matroids and fixed . The source compares this with the earlier greedy guarantee. This mission formalizes the published monotone result and its supporting exchange statements, with the constants and algorithmic quantifiers intact (Introduction and Theorem 3.1).
The ground set is a finite set of elements. A submodular function assigns a real number to every subset and satisfies
All objective values in the faithful source statements are nonnegative. For the headline theorem the function is also nondecreasing: implies . The empty set need not have value zero.
A matroid on is a family of independent sets containing the empty set, closed under taking subsets, and satisfying augmentation: a smaller independent set can gain an element from a larger independent set while remaining independent. There are such matroids, all on the same ground set. A set is common independent, or feasible, when it is independent in every one of them. The quantity is the maximum of over feasible subsets. This maximum exists even when is empty, since there are finitely many subsets and the empty set is feasible.
An algorithm receives a value oracle for and one independence oracle for each matroid. A value query specifies a subset and returns its value; an independence query specifies a matroid and a subset and returns a yes-or-no answer. Real arithmetic and comparisons use the unit-cost oracle convention. No table of all objective values is supplied (Introduction, p. 795).
The goal is the first sentence of Theorem 3.1. For each fixed and , there must exist one finite oracle program and polynomial constants, depending only on those fixed parameters, such that on every instance it halts and returns a feasible set with
The time bound includes initialization, oracle queries, subset processing, unsuccessful searches, and output. It is not merely a bound on the number of improving moves (Theorem 3.1, p. 803).
The eleven supporting milestones follow the source's numbered statements. They cover perfect matching for equal-size independent sets; irreducible cycle covers; the independence consequence of a unique perfect matching; feasibility of irreducible cycles; feasible path and cycle covers; exact-cover addition; generalized Rota exchange; bounded-multiplicity exchange for independent sets; exact-cover removal; and exact and approximate local-search inequalities. The order follows the dependencies identified in §§1–3. The exact local-search bound is
with a factor on the left in the approximate version. Here is an integer, is any feasible set, and the objective may be nonmonotone (Lemmas 3.1–3.2).
The approximation theorem gives a quantitative guarantee for general matroid intersections with a submodular objective. Restricting the constraints to partition matroids, or proving that a good set exists without a polynomial computation, would lose part of the result. The supporting exchange statements also describe how independent sets can be related when individual exchanges cannot simply be combined across constraints (§§2–3).
The mathematics is a published result; this mission asks for machine-checked proofs of its formal statements. The submodularity predicate is reused from an existing published definition. Lemma 2.1 is anchored to an existing Open bijective exchange theorem through a contraction and graph interpretation, rather than posed again. Open means that its proof remains a target. The remaining statements and the operational oracle model are local drafts, and compiling their statements does not prove them.
A chain of individually feasible swaps need not give a feasible simultaneous exchange. The source's distinction between an arbitrary directed cycle and an irreducible one therefore matters. Feasibility of a path or cycle also includes every eligible subpath, not just the whole vertex-set swap. Losing either distinction changes the supporting exchange results (Definitions 2.1–2.2).
Polynomial computation is a separate obligation from local-optimum quality. Literal Figure 1 admits infeasible singleton initialization when loops are present and nontermination at zero value under its non-strict update test. These issues are recorded as findings about the displayed routine, while the existential headline retains all inputs. Two further findings identify missing witness properties and an invalid intermediate path-count estimate in the printed analysis; they do not establish falsity of the numbered local-search inequalities. Proofs must resolve those obligations without importing them as assumptions (pp. 802–803).
Lean represents by Fin n, subsets by finite sets, objective values by real numbers, and matroids by Mathlib matroids with ground set equal to the whole finite type. Indexed families preserve repeated sets and repeated paths or cycles. Paths may consist of one vertex, cycles may have two vertices, and the cover multiplicity is , including . There is no looplessness, normalization, positive-optimum, or equal-cardinality restriction on the headline inputs.
The algorithmic goal uses a finite register-machine language whose only input-dependent operations are the two types of oracle queries. An explicit halt and a bound on the full execution cost are conclusions. Definitions contain neither an approximation guarantee nor an assumed polynomial stopping bound. The terminal predicate for Figure 1 uses strict inequality because the printed update uses greater-than-or-equal. Empty and zero-value inputs belong to the headline theorem even though the literal terminal predicate need not describe them.
The stronger linear-objective sentence of Theorem 3.1, the nonmonotone algorithm of Theorem 4.1, and the tightness examples in §5 are outside this mission. No optional variants are posed. Contributions needed here include the source theorem proofs, the exchange adapter, and the operational algorithm witness and its accounting.
A system of users sharing resources may have no stable configuration: whenever the users settle on their choices, somebody may prefer to change. Weighted congestion games describe this question when different users place different demands on the resources they choose. Routing and scheduling provide examples, but the mathematical question here does not impose a particular network or scheduling structure. It asks which resource cost functions guarantee stability regardless of the finite population, its demands, and its feasible choices. Harks and Klimm give a classification of such functions in their 2012 paper, Theorem 5.1.
There are two distinct requirements. A stable configuration may exist even when some sequences of individually profitable moves cycle forever. Guaranteeing that every sequence terminates is generally stronger. The result identifies the continuous function classes for which these two universal guarantees coincide. The word “universal” matters: the assertion concerns all games generated by a class of costs, rather than the behavior of one specified game.
A weighted congestion game has a nonempty finite set of players and a nonempty finite set of facilities . Each player has a positive real demand and a nonempty finite collection of available strategies. A strategy is a subset of facilities; it may itself be empty. A profile chooses one strategy for every player. Facility has a real-valued cost function defined on the nonnegative half-line. Its load and a player's private cost are
Costs can have either sign, and the game model imposes no monotonicity. A pure Nash equilibrium is a profile satisfying for every feasible unilateral change . A strict improvement lowers the deviating player's cost. The finite improvement property, or FIP, excludes improvement cycles, equivalently infinite improvement paths in this finite profile space. These conventions follow §2 and Definition 2.1.
For any set of cost functions, write for all such games with at every facility. The class is consistent if every game in has a pure equilibrium, and FIP-consistent if every such game has the FIP. The class can be infinite or empty. In the results below, continuity always includes the endpoint zero. “Monotonic” means nondecreasing or nonincreasing, with the direction allowed to differ between functions.
The goal is Theorem 5.1, p.427. For a set of continuous functions, the following are equivalent:
The exponential rate is shared by the entire class. No coefficient or rate is subject to a sign or nonzero restriction. The disjunction is inclusive, as printed in the theorem: classes of constant functions satisfy both alternatives.
Six source milestones support this target. Lemma 3.1 characterizes monotonicity by local right-hand comparisons with . Lemma 3.2 supplies positive loads with either or the reversed inequalities. Lemma 3.4 asserts monotonicity of the integer hull with offsets
under unrestricted consistency. Proposition 5.1 uses consistency for exactly three players to obtain monotonicity of both restricted hulls
Lemma 4.1 equates monotonicity of every integer combination of two continuous monotonic nonconstant functions with affine dependence between them. Lemma 5.1 equates monotonicity of the translated-function hull with each function being affine or exponential; its rate may depend on the function. The source locations are pp.422–427, §§3–5.
The classification separates structural guarantees from favorable individual instances. A class that fails the displayed alternatives cannot guarantee a pure equilibrium for every admissible game. Conversely, either alternative guarantees termination of strict improvement paths as well as equilibrium existence. This gives a precise answer to the unrestricted consistency question posed by Harks and Klimm, without imposing nonnegative or increasing costs.
The mathematical results are published results, not new conjectures. The remaining task is their machine-checked proof. This draft supplies compiled definitions and theorem statements; the seven theorem bodies remain proof targets. Its reusable components include the finite weighted game model, universal class predicates, and three different integer hulls. Published pure-equilibrium and improvement-path definitions are reused through their existing interfaces.
Monotonicity of individual resource costs does not settle the unrestricted problem. The selected statements impose conditions on combinations of functions, and those conditions distinguish the allowed class-wide structure. In particular, separate exponential representations for every member do not establish the common-rate alternative. Another logical obstacle is that an improvement cycle alone need not rule out an equilibrium elsewhere in a game's profile space. The source's nonexistence arguments must exclude every feasible equilibrium, not just exhibit cycling behavior. These distinctions are visible in §§3–5.
The findings accompanying this mission record local issues in printed proofs separately from their theorem statements. Such issues do not authorize stronger hypotheses or weaker conclusions in the faithful targets.
Players and facilities are indexed by finite initial segments with strictly positive sizes. Strategies are finite subsets, and feasible strategies are subtypes of the specified nonempty families. This represents every finite game up to relabeling. Demands are strictly positive nonnegative reals, loads are finite sums, and private costs are ordinary reals. Payoff-maximizing published definitions receive the negative of the private cost. Finite profile spaces justify the equivalence of the published infinite-path FIP convention and the paper's cycle convention.
Consistency is defined by quantification over all admissible games; neither potentials nor the classification are included in admissibility. The hulls are constructed from integer coefficients and the stated translates, without selecting only their monotonic members. Continuity is imposed on the whole nonnegative domain. These choices exclude vacuous proxy models and restricted strategy classes. The empty class and constant functions remain included. No asymptotic estimates or extracted constants occur.
The twelve new definition items precede the seven theorem items, and the six numbered source milestones retain their provenance. No optional variant is posed. The independent two-player characterization and the network and singleton results are outside the mission. In particular, the correction notice on p.436 concerning finite rather than polynomial termination does not introduce an algorithmic target here. Contributions should complete the faithful statements and their needed supporting theory while preserving these conventions.