Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

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.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131125302137Formalized record≥ 2.15Open frontier

11 provers on it19 of 20 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ 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.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ 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 $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

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.

≤ 2Formalized record

19 provers on it9 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -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 $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 12Formalized record≤ 2Open frontier

8 provers on it14 of 15 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 23Formalized record≤ 5Open frontier

41 provers on it15 of 17 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

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.

All missions

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Revenue-Sharing Allocation Strategies for Two-Sided Media Platforms: Pro-Rata vs. User-Centric: The Ratios π2j/π1j for Which Each Rule Sustains All Artists Form Two Explicit IntervalsResearch Paper

Motivation

Music and podcast streaming services such as Spotify, Apple Music and Deezer charge every subscriber the same monthly fee and pass a share of the collected revenue to the artists. How that share is split is contested. The industry default, pro-rata, pools all fees and pays each artist her share of total streams. The alternative, user-centric, splits each subscriber's fee according to that subscriber's own listening. The two rules pay identical amounts when all users stream the same volume, and differ whenever heavy users and light users listen to different artists; which artists gain and which lose under each rule is the subject of an active industry debate.

Alaei, Makhdoumi, Malekian and Pekeč (SSRN 3645521; published in Management Science 68(12), 2022, doi:10.1287/mnsc.2022.4307) model the question as a two-sided market in which every artist has an outside option: she can leave the platform and sell her content directly. A rule is only viable if it pays each artist at least what she would earn alone. The paper's first main result, Theorem 1, says exactly when each rule can keep every artist on the platform. This mission formalizes that theorem and the chain of results its proof rests on, citing the authors' submitted manuscript (SSRN 3645521) for all page and result numbers.

Setting

There is a finite set $\mathcal M$ of artists and two user types $i\in\{1,2\}$ . Type $i$ users consume content at usage rate $\lambda_i$ and form a population of mass $q_i$ ; a type $i$ user wants artist $j$ with probability $\pi_{ij}$ per use. Throughout,

\lambda_2>\lambda_1>0,\qquad q_1,q_2\in(0,1),\ q_1+q_2=1,\qquad \pi_{ij}\ge0,\ \sum_{j}\pi_{ij}=1 .

Type 2 users are the heavy users.

Going solo. If artist $j$ sells directly at price $r$ , a type $i$ user buys when her value $\lambda_i\pi_{ij}$ is at least $r$ , so the demand $d(j,r)$ is $0$ , $q_1$ , $q_2$ or $1$ according to which of $\lambda_1\pi_{1j}\ge r$ and $\lambda_2\pi_{2j}\ge r$ hold. The solo revenue is

R_j=\max_{r} r\,d(j,r).

The platform. With all artists on the platform and both types subscribing, the fee is $\mathrm{Fee}=\min_i\lambda_i\sum_j\pi_{ij}$ and the revenue is $\mathrm{Rev}=\mathrm{Fee}\,(q_1+q_2)$ . A payout rate $\beta\in[0,1]$ is the fraction of revenue paid to artists. The pro-rata payment (Definition 1) and the user-centric payment (Definition 2) to artist $j$ are

p^{\mathrm{pr}}_j(\beta)=\beta\,\mathrm{Rev}\,\frac{\sum_i q_i\lambda_i\pi_{ij}}{\sum_i q_i\lambda_i\sum_k\pi_{ik}},\qquad p^{\mathrm{uc}}_j(\beta)=\beta\sum_i q_i\,\mathrm{Fee}\,\frac{\lambda_i\pi_{ij}}{\sum_k\lambda_i\pi_{ik}} .

The platform is sustainable with a rule if some $\beta\in[0,1]$ makes every artist's payment at least $R_j$ .

Assumption 1 is $\lambda_1\ge\lambda_2q_2$ : it rules out the case where the platform would rather serve heavy users alone, in which the two rules coincide. Artists are sorted by the ratio $\pi_{2j}/\pi_{1j}$ into four regions

W=[0,\tfrac{q_1\lambda_1}{\lambda_2}),\quad Z=[\tfrac{q_1\lambda_1}{\lambda_2},\tfrac{\lambda_1}{\lambda_2}),\quad Y=[\tfrac{\lambda_1}{\lambda_2},\tfrac{\lambda_1}{\lambda_2q_2}),\quad X=[\tfrac{\lambda_1}{\lambda_2q_2},\infty).

Formalization targets

Goal: Theorem 1 (p. 17)

Under Assumption 1 (and $\pi_{1j}>0$ for all $j$ ), the platform is sustainable with pro-rata if and only if, for all $j$ ,

\frac{\pi_{2j}}{\pi_{1j}}\in\Bigl[\tfrac{q_1(\lambda_2-\lambda_1)}{\lambda_2},\tfrac{q_1\lambda_1^2}{\lambda_2^2q_2+\lambda_1\lambda_2(q_1-q_2)}\Bigr]\cup\Bigl[1,\tfrac{q_1\lambda_1^2}{\lambda_2q_2^2(\lambda_2-\lambda_1)}\Bigr],

and sustainable with user-centric if and only if, for all $j$ ,

\frac{\pi_{2j}}{\pi_{1j}}\in\Bigl[0,\tfrac{q_1\lambda_1}{\lambda_2-q_2\lambda_1}\Bigr]\cup\Bigl[1,\tfrac{q_1\lambda_1}{q_2(\lambda_2-\lambda_1)}\Bigr].

Milestones

Lemma 1 (p. 14): $R_j$ equals $q_1\lambda_1\pi_{1j}$ , $\lambda_2\pi_{2j}$ , $\lambda_1\pi_{1j}$ , $q_2\lambda_2\pi_{2j}$ on $W,Z,Y,X$ , attained at the stated fee with the stated subscribers.
Eq. (10) (p. 16): every artist is paid at least $R_j$ under pro-rata with payout $\beta$ iff $\beta\ge\beta^{\mathrm{pr}}=\frac{q_1\lambda_1+q_2\lambda_2}{\lambda_1}\max_j\frac{R_j}{q_1\lambda_1\pi_{1j}+q_2\lambda_2\pi_{2j}}$ .
Lemma 6 (p. 45): pro-rata sustainability is equivalent to four region-wise bounds on $\pi_{2j}/\pi_{1j}$ .
Eq. (11) (p. 16): the same for user-centric with $\beta^{\mathrm{uc}}=\frac1{\lambda_1}\max_j\frac{R_j}{q_1\pi_{1j}+q_2\pi_{2j}}$ .
Lemma 7 (p. 45): user-centric sustainability is equivalent to three region-wise bounds.

Significance

Theorem 1 separates the two rules by the kind of artist they can retain. Both rules lose artists whose audience is concentrated among heavy users, since such an artist captures those users' full fee by going solo; pro-rata tolerates a larger ratio $\pi_{2j}/\pi_{1j}$ before losing her. User-centric, in turn, can retain artists listened to mainly by light users, which pro-rata pays too little. The later results of the paper (which rule artists and the platform prefer, Propositions 2–3, and the optimal artist sets of §3.4) all start from this characterization.

The result is proved in the paper. No part of it, nor the underlying model of subscription fees, outside options and payout rates, has a machine-checked proof. The platform already has an axiomatic treatment of pro-rata and user-centric indices on stream-count tables; this mission adds the economic model with prices, outside options and payout rates, and its sustainability theorem. A complete development gives a checked version of the paper's case analysis, including its boundary cases.

Difficulty

Each step is elementary, and the difficulty lies in the bookkeeping. The solo revenue is a supremum of a step function times the price, and identifying its value requires comparing three candidates on four regions with half-open boundaries. The payments must be simplified from their general form (with sums and a minimum fee) to the closed forms of (10)–(11), which uses the standing assumptions and Assumption 1. Finally, combining four region-wise conditions into two intervals does not go region by region: when $\lambda_2>2\lambda_1$ the first pro-rata interval is empty and no artist in $W$ or $Z$ can be sustained, and the upper intervals agree with the region boundary $\lambda_1/(\lambda_2q_2)$ only because of Assumption 1. A transcription that treats the printed intervals as non-empty, or drops Assumption 1, gives a false statement.

Formalization scope

Everything sits in the namespace ProRataUC.Sustain, in one definitions file and six theorem files. The setting is a structure Setting M over a type M of artists with [Fintype M], with real fields lam1 lam2 q1 q2 and listening probabilities pi1 pi2 : M → ℝ; the standing assumptions are one predicate Setting.Standing, and Assumption 1 is a separate predicate. Conventions:

The solo revenue is the real supremum of $r\,d(j,r)$ over all real $r$ , with $d$ the printed four-case demand; the family is bounded above, so the supremum is genuine.
The fee and revenue are those with all artists on the platform and both types subscribing, with the sums $\sum_j\pi_{ij}$ as printed, not hard-coded to $\lambda_1$ .
Sustainability is the existence of a payout rate $\beta\in[0,1]$ under which every artist's payment is at least $R_j$ , not the inequality $\beta^{\mathrm{pr}}\le1$ and not the interval condition; equations (10)–(11) are the bridge.
$\beta^{\mathrm{pr}}$ and $\beta^{\mathrm{uc}}$ use a maximum over a nonempty finite set, so (10)–(11) assume at least one artist.
The intervals are closed in Theorem 1 and half-open in Lemma 1 and the regions, as printed.

Added hypotheses, each disclosed in the statement: $\pi_{1j}>0$ (the paper's ratio presupposes it; Lean's division by zero would put an artist heard only by heavy users in the region $[0,\cdot)$ and make part (b) false); Assumption 1 in equations (10)–(11) and Lemmas 6–7, whose proofs use it although the lemmas say "for a given $\lambda$ and $q$ ".

Formalizations that would trivialize the goal are ruled out: sustainability is not defined as the printed intervals or as $\beta^{\mathrm{pr}}\le1$ , $R_j$ is not defined by Lemma 1's case formula, $\pi_{1j}>0$ is explicit, and Assumption 1 is kept.

Contributions welcome: proofs of the milestones in order, reusable lemmas on suprema of step functions times price (the two-type monopoly pricing problem) and on Finset.sup' of ratios, and the interval bookkeeping of Theorem 1.

Selected references

S. Alaei, A. Makhdoumi, A. Malekian, S. Pekeč, Revenue-sharing allocation strategies for two-sided media platforms: Pro-rata vs. user-centric, submitted manuscript, SSRN 3645521 (2020); published in Management Science 68(12):8699–8721, 2022. https://ssrn.com/abstract=3645521 , https://doi.org/10.1287/mnsc.2022.4307
G. Bergantiños, J. D. Moreno-Ternero, Revenue sharing at music streaming platforms, Management Science, 2025 (axiomatic comparison of pro-rata and user-centric); arXiv:2310.11861. https://arxiv.org/abs/2310.11861

7 thms2 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

On Dimension Bounds for Auxiliary Quantum SystemsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

The private classical capacity and quantum capacity of a quantum channelResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Zero-error communication under discrete-time Markovian dynamicsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Non-Ownership Business Models for Solar Energy: When a Solar Power Company Optimally Offers Power Purchase Agreements, Leasing and SalesResearch Paper

Why the business-model choice matters

Customers, prices and profit

Formalization targets

What the result enables

Main difficulty

Formalization scope

Selected references

One-Shot Manipulation of Dynamical Quantum ResourcesResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Theoretical framework for quantum networksResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Lower bound on entanglement in subspaces defined by Young diagramsResearch Paper

Motivation

What is formalized

Selected references

Labor Welfare in On-Demand Service Platforms: With Delay-Sensitive Customers, Average Labor Welfare First Increases and Then Decreases in the Labor Pool SizeResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 11)

Milestones (in attack order)

Significance

Difficulty

Formalization scope

Selected references

Controlling Epidemic Spread: Reducing Economic Losses with Targeted Closures: The Effective Reproduction Rate Is Below One if and only if a Linear Matrix Inequality in the Activity Levels HoldsResearch Paper

Why targeted closures matter

The spatial epidemic model

Formalization targets

What the result provides

Where the difficulty lies

Formalization scope

Selected references

Revenue-Sharing Allocation Strategies for Two-Sided Media Platforms: Pro-Rata vs. User-Centric: The Ratios π2j/π1j for Which Each Rule Sustains All Artists Form Two Explicit IntervalsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 17)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Energy-constrained private and quantum capacities of quantum channelsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

OpenAI Ten Proofs 06: Quantum parallel repetitionResearch Paper

The mother of all protocols: Restructuring quantum information's family treeResearch Paper

Motivation

What is formalized