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?
EvalScript decides what a script does; VerifyScript decides which scripts run, on what stack, under which signature version, and what counts as success. It is where pay-to-script-hash (BIP16), segregated witness (BIP141) and the hand-off to Taproot live: the output script is evaluated first, then — if it is a witness program — the witness is interpreted, or — if it is P2SH — the redeem script is extracted from the scriptSig and run, possibly revealing a wrapped witness program. Each of these steps carries anti-malleability rules (an empty scriptSig for native witness, exactly one push for wrapped witness, push-only scriptSigs for P2SH, a clean witness stack) and the future-compatibility rule that unknown witness versions succeed. (VerifyScript, BIP16, BIP141)
This mission transcribes VerifyScript, VerifyWitnessProgram for version 0 and the unknown versions, ExecuteWitnessScript, and the script predicates, on top of the published interpreter and signature layer, and proves that the four spending templates that carry the chain's history behave as advertised — P2SH, native P2WPKH, native P2WSH, P2SH-wrapped P2WPKH — and that the malleability and compatibility rules hold as universal statements.
A byte-level evaluation parses a script with GetOp, rejects scripts over 10,000 bytes, and runs the Script mission's interpreter with the signature mission's concrete oracle for the given signature version (BASE or WITNESS_V0) and script code. Stacks are top-first; a CScriptWitness lists its elements first to last, the last being the top, so witness stacks are reversed before execution.
VerifyScript runs the scriptSig, keeps a copy of the resulting stack, runs the output script, and requires a true top. With WITNESS, an output that is a witness program (OP_n and one push of 2–40 bytes) must have an empty scriptSig and is handed to VerifyWitnessProgram. With P2SH, an output OP_HASH160 <h> OP_EQUAL requires a push-only scriptSig; the copied stack is restored, its top is the serialized redeem script, which is run on the remainder and must leave a true top; with WITNESS, a redeem script that is a witness program must be the scriptSig's only push and is handed to VerifyWitnessProgram as P2SH-wrapped. Finally, with WITNESS, a non-empty witness that no program consumed fails.
VerifyWitnessProgram for version 0 distinguishes a 32-byte program (P2WSH: the last witness element is the script, its SHA-256 must be the program) from a 20-byte one (P2WPKH: exactly two elements, the implied DUP HASH160 <program> EQUALVERIFY CHECKSIG); ExecuteWitnessScript requires every element within 520 bytes and exactly one true element at the end. Version 1 with a 32-byte program outside P2SH is Taproot, delegated to a handler parameter when the TAPROOT flag is on; pay-to-anchor and every other version/size combination succeed.
for every 20-byte , every signature and key within the push limit, every transaction, amount and flag set with WITNESS. This is BitcoinVerify.p2wpkh_correct: the most common output type on the network today is correct against the full dispatch, the interpreter and the concrete BIP143 checker. The first conjunct is a genuine finding of the transcription: OP_0 <h> is evaluated as a script before the witness is consulted, so an all-zero program is unspendable.
isPayToScriptHash_iff, isWitnessProgram_iff): the byte tests are exactly the templates.parseScript_pushes, isPushOnly_pushes): canonical pushes parse back and are push-only.native_witness_malleated, witness_unexpected): non-empty scriptSig on a witness program fails; an unconsumed witness fails.unknown_witness_version): unknown versions succeed exactly when the program is a true script value.p2wsh_correct): the witness script, hashed to the program, runs on the remaining elements and must leave one true element.p2sh_correct): hash match and redeem evaluation on the pushed arguments.p2sh_p2wpkh_correct): the wrapped program through the P2SH path.The template theorems are two-directional: they say what spends succeed and that nothing else does, for every oracle verdict. Combined with the signature mission they reduce the correctness of the four templates to Hash160 equalities and ECDSA verification of the appropriate sighash. The rule theorems make BIP141's malleability protections and its upgrade hooks universal facts about the transcription rather than test cases.
What is left to the Taproot mission: the version-1 branch (TaprootHandler) and Tapscript. What is policy and off: SIGPUSHONLY, CLEANSTACK, MINIMALIF, DISCOURAGE_*. Known modeling limit inherited from the Script mission: OP_CODESEPARATOR positions are not tracked, so the oracle's script code is the whole executed script (exact for scripts without the opcode).
Status: all statements are open with intentional placeholder proofs. The dispatch has been checked by evaluation against independently signed P2WPKH, P2SH-P2WPKH and legacy P2SH spends and their negative variants.
The base evaluation of a witness output is easy to forget: OP_0 <h> must itself evaluate to a true top before the witness is looked at, which produces the castToBool h conjunct and the all-zero exception. The P2SH path reasons about two stacks — the one after the scriptSig (restored and popped) and the one after the output script (only its top matters) — and about the parse of the scriptSig twice (as pushes, and as IsPushOnly). The unknown-version theorem needs the evaluation of OP_n for every in 1–16 through the interpreter's small-integer branch, with its count and disabled-opcode exemptions. Witness order (last element on top) must be threaded through reverse, dropLast and getLast? consistently.
Flags are the seven consensus flags of GetBlockScriptFlags. The amount is an integer (negative where unknown, as the source passes for legacy inputs). The Taproot branch is a parameter. No Mathlib is required; the development imports only Std.
A trivializing formalization would define verifyScript by cases on the templates; here it is the source's control flow and the templates are theorems.
VerifyScript, VerifyWitnessProgram, ExecuteWitnessScript, src/script/interpreter.cpp, and CScript predicates, src/script/script.cpp, at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. SourceThe Hlawka inequality compares the norms of three vectors with those of their pairwise sums and total sum. The question is the smallest comparison constant that works in every finite dimension.
This mission records the proved extension of the sharp diagonal Hlawka constant to every real . It uses the unchanged coordinate norm and cyclic constant from the foundation mission, for arbitrary complex vectors, including unequal and zero norms.
The cutoff-12 goal theorem is already proved on Prove2Me. Sixteen accepted interval proofs cover and join the proved cutoff-16 result. The conclusion includes both the inequality and optimality of its constant, uniformly over all finite complex coordinate dimensions.
This is an entry in the sharp diagonal Hlawka campaign, whose conjectured endpoint is . The cutoff-2 mission remains open; 12 is a proved sufficient cutoff, with no claim that it is optimal. The broader Schatten-norm question for general matrices is described by Audenaert and Kittaneh, §8.2.
A finite-range piece of Dusart's explicit upper bound for the prime counting function: for . Dusart proved the bound for every [P. Dusart, Estimates of some functions over primes without R.H., arXiv:1002.0442, Theorem 6.9]. This mission asks only for the finite range, which is a computation over about 148,000 primes and needs no analytic input.
Why it matters: the bound is an input to explicit Goldbach-type results, where it is used to control prime counts in a bounded window. A Lean proof lets those results drop one cited assumption.
Proposed by the Lean Lab, an AI-assisted formalization project on Goldbach-related literature. The statement was written by Claude; the proposer confirmed it against the paper before launch.
A Bitcoin transaction is authorized by signatures, and whether a signature counts is decided by a chain of exact rules: the byte layout the signature must have (strict DER since BIP66), which parts of the transaction the signature commits to (the signature hash, in its legacy and BIP143 forms, with the historical SIGHASH_SINGLE bug), how the public key is parsed, how a possibly non-canonical signature is parsed "laxly", and finally ECDSA verification on secp256k1 — or Schnorr verification for Taproot. Each of these has been the site of a consensus-relevant subtlety: BIP66 was a soft fork to remove OpenSSL's parsing from consensus; the SIGHASH_SINGLE bug lets a signature commit to nothing; high-S normalization is why libsecp256k1 accepts what historical blocks contain. (interpreter.cpp, pubkey.cpp, BIP66, BIP143, BIP340)
This mission transcribes that layer end to end — the encoding checks, FindAndDelete, both signature hashes, CPubKey::Verify with the lax DER parser and normalization, the secp256k1 verification equations for ECDSA and Schnorr, the checker's lock-time methods, and the byte-level script parser — and proves what the rest of validation needs: the strict-DER test is exactly the canonical layout, the signature hashes depend on what they should and nothing else, the checker's outcomes are characterized, and the Script mission's abstract P2PKH theorem instantiates to the concrete cryptography.
secp256k1 is the curve over the prime field of order , with group order and generator . Points are affine pairs or infinity; addition and scalar multiplication are the textbook formulas with Fermat inverses. A public key is parsed as secp256k1_eckey_pubkey_parse: compressed (02/03, square root by with parity selection), uncompressed (04) or hybrid (06/07), with coordinates below and on the curve. A signature reaches verification through ecdsa_signature_parse_der_lax, which tolerates long-form lengths and leading zeros, ignores trailing bytes, and substitutes the zero signature on overflow; its S value is normalized to the low half; the message is the 32-byte hash reduced modulo ; and secp256k1_ecdsa_sig_verify accepts iff , and . Schnorr verification is BIP340 with tagged hashes and lift_x.
The signature hash of input under hash type is, for legacy scripts, SHA-256d of the CTransactionSignatureSerializer output — version, the inputs (only the signed one under ANYONECANPAY; other inputs' scripts blanked, their sequences zeroed under SINGLE/NONE), the outputs (none under NONE, truncated to with blanked others under SINGLE), lock time — followed by as four bytes, except that SINGLE with no output at yields the constant ; for witness v0 it is the BIP143 construction with hashPrevouts, hashSequence, hashOutputs, the script code and the amount.
The encoding checks are IsValidSignatureEncoding (the fourteen BIP66 tests), low-S, the key-shape tests and the hash-type test, assembled by CheckSignatureEncoding/CheckPubKeyEncoding under the flags (DERSIG is the only one mainnet consensus enables). The checker (EvalChecksigPreTapscript) deletes the signature push from the script code (legacy only), applies the encoding checks as script errors, and returns CheckECDSASignature's verdict: a valid key, a non-empty signature whose last byte is the hash type, and CPubKey::Verify on the signature hash. The lock-time checks are CheckLockTime and CheckSequence. The oracle packages all of this, with Core's hashes, into the abstract Oracle of the legacy Script interpreter.
This is BitcoinSig.derEncode_complete together with its converse derEncode_valid: the byte-indexed test of the source is exactly the canonical layout, in both directions. It is the content of BIP66 as a statement about byte strings rather than a procedure.
SIGHASH_SINGLE bug (sigHash_single_bug): the hash is when there is no output at the input's index.sigHashLegacy_skeleton, sigHashWitnessV0_skeleton): both hashes ignore scriptSigs and witnesses; (sigHashLegacy_anyoneCanPay): with the flag, only the signed input matters.pubkeyValid_iff, normalizeS_low, overflow_rejected).checkSig_empty, checkSig_dersig, checkSig_base_iff): an empty signature is a clean false; with DERSIG a malformed one is a script error; the legacy verdict is ECDSA on the legacy sighash of the signature-deleted script code.parseScript_p2pkh): the P2PKH bytes parse to the interpreter's P2PKH instructions.p2pkh_concrete): the Script mission's p2pkh_correct, instantiated with Core's hashes and checker.With this mission the signature-related rules of the pinned source are kernel-checked semantics rather than prose: what shape a signature must have, what it signs, and what accepting it means in terms of the curve equations. The characterization of strict DER removes a class of malleability by construction. The sighash theorems are the facts that transaction malleability arguments and the segregated-witness design rest on. The concrete P2PKH theorem closes the loop the Script mission opened: the template is correct with the real cryptography, modulo nothing but the mathematics of the curve.
What is deliberately not claimed: that the curve operations are constant-time, that the group law holds (the verifier is a function; its correctness as a signature scheme is a cryptographic, not a consensus, property), or anything about OP_CODESEPARATOR positions, which the legacy interpreter of the Script mission does not track (the oracle's script code is the executed script, exact for separator-free scripts). Signature caching, the precomputed-transaction-data caches and the sighash midstate cache are optimizations with the same result and are not modeled.
Status: all statements are open with intentional placeholder proofs. The definitions have been checked by evaluation against the BIP340 test vectors, the BIP143 worked example, independently generated ECDSA signatures, and a reference implementation of the legacy serializer.
The strict-DER characterization is byte-index chasing: the source reads sig[4], sig[5 + lenR], sig[lenR + 7], and the proof must relate these to the slices and and show the three leading-zero rules are exactly minimality of the big-endian integers. The converse direction needs the cuts at , , and the end to reassemble the string. The sighash theorems look definitional but require relating getD on the input list to the projected skeleton under ANYONECANPAY (one input), SINGLE (outputs truncated) and the blanking rules. The checker characterization has to split the signature into body and hash-type byte in both directions.
Field and scalar arithmetic are on Nat modulo and , with inverses by Fermat and explicit fuel for exponentiation and scalar multiplication. Byte strings are List (BitVec 8); the transaction type is the serialization mission's. Policy flags (LOW_S, STRICTENC, WITNESS_PUBKEYTYPE, NULLFAIL, CONST_SCRIPTCODE) are carried where they shape the control flow but are off in block validation. Tapscript signature checking (BIP341/342 sighash, OP_CHECKSIGADD) belongs to the Taproot mission.
A trivializing formalization would define the strict-DER test by the layout, or the sighash by what it should depend on; here both are the source's procedures and the layout and dependence are theorems. No Mathlib is required; the development imports only Std.
script/interpreter.cpp, pubkey.cpp, script/script.cpp, and libsecp256k1 eckey_impl.h, ecdsa_impl.h, modules/schnorrsig/main_impl.h at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. SourceEvery commitment in Bitcoin — a transaction id, a merkle root, a block hash, the proof-of-work target test — is a hash of a byte string, and the byte string is produced by a serializer that every node must implement identically. A node that encoded a CompactSize one byte longer, or read a witness flag differently, would compute different ids for the same transaction and fork from the network. Bitcoin Core's serialization lives in serialize.h (integers, CompactSize, vectors), primitives/transaction.h (the basic and BIP144 extended transaction formats), primitives/block.h (the 80-byte header), and its hashes in crypto/ and hash.h. (serialize.h, transaction.h, sha256.cpp)
This mission transcribes that layer — writers and readers for integers, CompactSize, vectors, transactions, headers and blocks; SHA-256, RIPEMD-160 and SHA-1 as full algorithms; Hash, Hash160, txid, wtxid, the header hash; transaction and block weights; and the mainnet genesis block — and proves the properties the rest of consensus consumes: encodings are canonical and round-trip, the witness-stripped id ignores witnesses, hashes have their sizes, and the transcribed genesis block hashes to the genesis hash of chainparams.cpp.
A writer turns a value into a byte list; a reader consumes a prefix of a byte list and returns the value and the remainder, or none where the source throws. Fixed-width integers are little-endian; signed ones are two's complement. A CompactSize is one byte below , or a marker byte , , followed by , , little-endian bytes; the reader rejects an encoding that could have been shorter ("non-canonical") and, in its default range-checked mode, any value above . A vector is its CompactSize length then its elements; a byte string is its length then its bytes; a uint256 is 32 raw bytes.
A transaction serializes as version vin vout nLockTime, or, when witnesses are allowed and some input carries one, in the extended format: version 0x00 0x01 vin vout witnesses nLockTime, where the 0x00 is an empty dummy vin and 0x01 the flag byte. The reader follows the source's control flow exactly: it reads vin; if that is empty and witnesses are allowed it treats it as the dummy, reads the flag byte and, if non-zero, the real vin and vout; a set witness bit then reads one witness stack per input and rejects a record whose stacks are all empty; any other flag bit rejects. A header is int32 nVersion, previous hash, merkle root, nTime, nBits, nNonce; a block is a header and a transaction vector.
Well-formedness names the field ranges under which the writers are faithful: 32-bit fields below , hashes of 32 bytes, amounts in , lengths at most , and — for blocks — every transaction has an input or a witness.
Hashes are the algorithms of crypto/: Merkle–Damgård padding, 64-byte chunks, the SHA-256 schedule and 64 rounds, the two RIPEMD-160 lines, the SHA-1 rounds; Hash is SHA-256 twice and Hash160 is RIPEMD-160 of SHA-256. The txid hashes the witness-stripped serialization; the wtxid the full one; the block hash the 80-byte header. Weight is three times the stripped size plus the full size.
for every well-formed block , witness mode and remainder . This is BitcoinSer.block_roundtrip: deserialization is a left inverse of serialization, in the witness-aware and the legacy reader alike. It is the statement that gives every hash commitment a referent: the bytes a node hashes are exactly the bytes from which every other node recovers the same block.
leBytes_length, readLE_leBytes): width and round-trip.compactSize_roundtrip, compactSize_canonical, compactSize_range): the writer's output is accepted; only the shortest encoding is ever accepted; read values are bounded.serHeader_length, header_roundtrip): 80 bytes, round-trip with the signed version.tx_roundtrip): round-trip in both formats, with the genuine side condition that the witness-aware reader needs a non-empty vin or a witness.serTx_strip, txid_strip): the stripped serialization and the txid ignore witness data.weight_no_witness): without witnesses, weight is four times the size.sha256_length, hash160_length).genesis_merkle, genesis_hash): the transcribed genesis coinbase and header hash, by kernel evaluation of the transcribed SHA-256, to the merkle root and block hash recorded in chainparams.cpp.serBlock_injective): distinct well-formed blocks have distinct serializations.The round-trip and canonicality theorems make the byte layer of consensus exact: a transaction or block has one encoding, the encoding determines the object, and the identifier hashes are functions of the object alone. The genesis theorems are an end-to-end check against the real chain: the transcriptions of CreateGenesisBlock, the serializers and SHA-256 together reproduce the hard-coded genesis hash, which no transcription error in any of them could survive. The witness-independence theorem is the structural fact behind segregated witness. For the whole-consensus development this mission supplies the concrete hash and serialization semantics that the Merkle, header, proof-of-work and script components took as parameters.
Not modeled: network message framing, CompactSize reading in the chunked allocation loop (semantically the same read), serialization of CBlockIndex/undo data, and the stream exception types (all failures are none).
Status: all statements are open with intentional placeholder proofs. The hash functions have been checked against the standard test vectors and the genesis values by evaluation; the genesis theorems are stated so that the kernel re-checks them.
Round-trip looks like unfolding until the transaction reader: because UnserializeTransaction reuses the vin read as the witness dummy, an empty vin is ambiguous, and the honest theorem carries the side condition "an input or a witness". The canonicality theorem is where the three "non-canonical" rejections earn their keep: without them a value would have several encodings and the statement would be false. The signed fields need the two's-complement conversion in both directions. For the genesis theorems the difficulty is not mathematical but computational: the kernel must evaluate nine SHA-256 compressions, which the definitions are written to allow (structural recursion only, no well-founded fixpoints in the evaluated path).
Bytes are BitVec 8, values are Nat/Int, words are UInt32. Readers return Option (α × Bytes). The writers truncate out-of-range values modulo the width, which the well-formedness predicates exclude; the readers are total. No Mathlib is required; the development imports only Std.
A trivializing formalization would define the readers as inverses of the writers; here each reader follows the source's byte-level control flow, and the round-trips are theorems.
serialize.h, primitives/transaction.h, primitives/block.h, hash.h, crypto/sha256.cpp, crypto/ripemd160.cpp, kernel/chainparams.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. SourceWhen a faster multiplication algorithm becomes available, its consequences depend on which problems reduce to multiplication and how the reduction changes input size. A displayed runtime bound alone does not identify this connection. The surrounding computation can also consume the improvement if its cost is omitted or underestimated.
Fourier transforms and bounded integer convolution illustrate two different connections. A complex Fourier transform can be expressed through ordinary complex polynomial multiplication using chirps, following Bluestein's construction. Bounded integer coefficients can instead be packed into binary integers, as in Kronecker substitution. This mission makes the first reduction an explicitly counted arithmetic program and proves the operand-size bound needed by the second. It does not identify binary integer computation with exact complex arithmetic.
A costed oracle returns an answer and a natural-number charge. The general program interface supports returns, explicitly charged work, and adaptive oracle queries. Its substitution theorem preserves answers and sums the query charges with local overhead.
The concrete Fourier interface additionally has explicit instructions for complex multiplication and inversion, each charged one unit. A product instruction takes arrays of lengths and and returns their ordinary polynomial product as an array of length , including trailing zero padding. The oracle's charge measures that product call. Array construction, access, index arithmetic, and control operations are uncharged in this arithmetic-operation model. The complex parameter is supplied as input, so root construction is outside the interface.
The binary magnitude length is zero for and is otherwise. It excludes a sign bit. The integer oracle multiplies signed integers with charge bounded by . Packing and decoding still have explicit charges ; their implementation in a bit-machine model is outside the proved scope.
The reusable general theorem states that a correct oracle with nondecreasing bound , at most calls of size at most , and overhead at most gives correct execution with cost
Composition preserves the complete answer-and-cost pair. An asymptotic corollary transfers eventual upper bounds on the resulting formula.
The main goal is the concrete Fourier transfer theorem. For every , nonzero , and input , a fixed program returns
with one full polynomial-product call and exactly additional multiplication or inversion instructions. Consequently, if the oracle cost is at most , then
When is the desired primitive th root of unity, this is the unnormalised discrete Fourier transform. The identity itself holds for every nonzero . The main theorem does not assume that is monotone or regular.
The Fourier milestones verify middle-coefficient extraction from a full product, generation of chirp entries in exactly instructions, the chirp identity, the exact total cost, and its runtime consequences. For , the conditions and give the pointwise bound . If these conditions hold uniformly with one , a family of these transforms has accounted cost .
The integer milestones prove that packing signed coefficients of magnitude at most in base produces an integer of magnitude length at most , for . For input bound , the automatic choice satisfies every spacing condition when . The resulting convolution program is correct and costs at most
This applies the existing proved signed Kronecker correctness theorem with a newly justified oracle input size.
The Fourier application no longer relies on arbitrary preparation and decoding labels. Its specific program includes every complex multiplication and inversion used to generate the chirps and scale the arrays, and the interpreter proves their count. A better complex polynomial-product bound can be substituted directly into the main inequality.
The packing application now evaluates an integer multiplication bound at a proved number of magnitude bits. Its logarithmic spacing overhead remains visible. This prevents substituting a length- coefficient array directly into a runtime bound for -bit integers.
These are formalizations of known reduction principles, with concrete program choices and constants supplied by the companion development. They are not new Fourier or multiplication exponent records. Local Lean proofs accompany every theorem in the strengthened draft. Local verification and accepted platform proof submissions remain distinct statuses.
Correct adaptive substitution must preserve subsequent queries, not merely the final numerical bound. Fourier preparation must actually generate chirps by a linear number of instructions; writing a large power in a returned expression would not justify a cheap implementation. Full-product coefficients must match the middle-product identity at every permitted index, and negative exponents must use a nonzero parameter.
Signed packing requires both correctness of balanced-digit decoding and a magnitude bound on the packed operands. A correct encoding alone cannot justify the claimed multiplication cost. Replacing by also needs a scaling condition; arbitrary runtime functions do not supply one automatically.
The core definitions use terminating inductive programs, natural-number charges, and an explicit eventual big-O predicate. The arithmetic instruction type permits arbitrary mathematical continuations and return values, so it is not a verified compiler from arbitrary functions to circuits. For the concrete Fourier program, preparation and decoding use only its explicit scalar instructions and structural array operations. Its cost result is an arithmetic-operation count, with the oracle cost interpreted in the same unit.
The Fourier theorems include ; this particular program still performs seven scalar instructions and a product call, returning an empty array. The packing size lemma includes empty lists and cancellation, while convolution requires . Coefficient bounds include their endpoints and allow negative entries.
The integer result does not prove linear-time bit encoders or decoders. Neither application establishes finite-precision error bounds, root-construction costs, memory costs, or an unrestricted implication from binary integer multiplication to exact complex DFT complexity. Subsequent work can add a verified bit representation and encoding implementation, or a register-based arithmetic compiler. Such additions must justify their costs independently rather than selecting favorable work labels.
Pricing a product line under the multinomial logit (MNL) model is a classical problem in revenue management. Its best-known answer is that, at optimality, every offered product carries the same markup, and offering more products never hurts (Hopp and Xu, 2005; Li and Huh, 2011). Both conclusions rest on the assumption that a consumer weighs every available alternative.
Empirical marketing work instead describes a two-stage process: consumers first screen alternatives into a consideration set and then choose within it. R. Wang's paper (The Threshold Effects on Consumer Choice and Pricing Decisions, Manufacturing & Service Operations Management, 2021; SSRN 3765711) models the screening with a threshold: an alternative is considered only if its nominal utility is within a tolerance of the best available alternative. This threshold MNL (TMNL) model can violate the independence of irrelevant alternatives and regularity, and the paper shows that it changes the optimal assortment and pricing policy. This mission formalizes that pricing result.
A firm sells products with unit costs . An outside option is always available. At prices , product has nominal utility , where is its intrinsic utility and the price coefficient; the outside option has nominal utility . The markup is , and is the utility net of cost, so . Products are labelled so that .
For an offer set let . The threshold consideration set is
The consumer then chooses with probability , and alternatives outside have probability . The outside option enters the denominator only if it is itself in ; a product priced attractively enough () prices it out. The firm's expected profit is
and the joint assortment and pricing problem (3) maximizes over all offer sets and prices .
A utility-net-cost ordered assortment is . A price vector on follows the quasi-same-markup/same-utility policy if, for some , products charge one common markup and products share one common nominal utility; product is free.
With , there is with
and, whenever (3) has a maximizer, a quasi-same-markup/same-utility price vector on attains .
Theorem 4 reduces a search over offer sets and prices to nested assortments and a policy described by a few scalars, which is what makes the problem solvable in practice; the paper's Appendix A turns this into an algorithm. It also shows where the TMNL answer departs from plain MNL: the low-margin tail of the assortment sits on the boundary of the consideration set at a common nominal utility rather than at the common markup, and offering fewer products, even a single one, can be optimal.
The result is proved in the paper, not formalized anywhere. A machine-checked version would settle the case analysis on whether the outside option is considered, which the paper treats in two separate proofs, and would make the model's objects (the consideration set and the TMNL choice probabilities) available for the paper's comparative statics in and its price-competition results.
The profit is a discontinuous function of the prices: a product, or the outside option, enters or leaves the consideration set as prices cross the thresholds . The standard MNL argument, which writes the optimal profit as the fixed point of a smooth first-order condition, applies only inside a region where is fixed. Across regions the supremum need not be attained. Already for one product, the profit is the markup as long as the outside option is priced out () and drops at , so no price is optimal and the paper's answer is "". A complete argument therefore cannot stay inside one region: it has to compare offer sets and regions with one another and deal with values that are reached only in the limit at a region's boundary.
Products are Fin N; the paper's product is the index , and is the set of indices below . The outside option is the separate parameter u0. Prices are arbitrary real vectors (they may be negative). The scale of the Gumbel noise is fixed to , as the paper does for (3), and the logit formula is the model: its derivation from random utilities is not formalized. Membership in is written as " for every ", equivalent to the maximum form. The standing assumptions of §3 are hypotheses of every theorem: , , the labelling by , and where is named.
Every optimal value is a least upper bound with an explicit value , never a sSup, because (3) need not have a maximizer; Theorems 1 and 4 add that when (3) does have one, it is attained on the ordered assortment (by quasi-same-markup/same-utility prices, in Theorem 4). Theorem 2's "" is stated at the closure point , with the profit given by the continuous formula for the outside-excluded consideration set. Theorem 3 assumes an attained optimum, as the paper does. A formalization in which the outside option always contributes to the denominator, or in which Definition 2's two groups are empty for every , would make the goal a statement about a different model or a restatement of Theorem 1, and is ruled out here. For every price vector satisfies Definition 2, as in the paper, so the goal's pricing clause has content from on.
All definitions are in one module, ThresholdMNL.Pricing.Model, which depends only on Mathlib. Proofs of the milestones are welcome in any order; the exchange step is self-contained algebra, and the consideration-set definitions are reusable for further TMNL results.
Mixed-integer quadratic programming (MIQP) asks to minimize a quadratic function over the points of a polyhedron whose first coordinates are integers. It contains integer linear programming, quadratic programming and combinatorial problems such as max-cut.
To place a decision problem in the class NP one needs, for every yes-instance, a certificate whose length is polynomial in the length of the input. For a mixed-integer system the natural certificate is a feasible point, and the whole difficulty is to show that some feasible point can be written down with polynomially many bits. A. Del Pia, S. S. Dey and M. Molinaro (arXiv:1407.4798; Mathematical Programming, 2017) proved that this is so for one quadratic inequality, which places the decision versions of integer and mixed-integer quadratic programming in NP; since they are NP-hard, both are NP-complete.
Timeline:
All data are rational. Fix integers , and , a matrix (not necessarily symmetric), vectors , , a number and a matrix . The feasible set of equation (2) is
where means that the first coordinates of are integers.
The complexity (bit-size) of a rational number in lowest terms is ; that of a vector or matrix is the number of its entries plus the sum of the sizes of its entries, and that of a finite set of objects is the sum of their sizes. Write for the complexity of .
A quantity is -small when its complexity is at most for one polynomial that serves every input . For a set of vectors, is the set of non-negative real combinations and the set of non-negative integer combinations of finitely many vectors of . A pointed polyhedral cone is simple when its number of extreme rays equals its dimension, i.e. it is generated by linearly independent vectors.
There is a polynomial such that for all and all rational as above,
The degree and coefficients of are left unspecified, which is what the paper proves and what NP membership needs.
Theorem 1 gives a polynomial-length certificate for every yes-instance of decision MIQP, hence Corollary 2: the decision versions of integer and mixed-integer quadratic programming are NP-complete. It unifies the two classical membership results above and, by the examples on pp. 2–3, marks the exact boundary: one quadratic inequality is always fine, two are not. Downstream, polynomial-size optimal or feasible solutions are the starting point for any analysis of exact algorithms for MIQP, for fixed-dimension questions (Del Pia and Weismantel solved in 2014; fixed dimension in general is open), and for bit-complexity arguments in branch-and-bound.
The result is proved and published. None of it, including Vavasis's theorem and the integer-linear case, has a machine-checked proof. Formalizing it produces a bit-size calculus for rational data, a mixed-integer Minkowski–Weyl decomposition with size bounds (Proposition 4), and the cone-refinement machinery of Section 3. The v1 proof read here has two gaps (Case 2, p. 7, passes from real to integer cones; p. 9 applies Theorem 3 to a non-polyhedral set), which the journal version revises; a formal proof settles the argument.
The obvious argument fails at unboundedness. If the feasible set were bounded, one would pick an optimal or extreme point and bound its size by linear algebra. Here the integer directions can be unbounded, the quadratic constraint is non-convex, and the feasible set need not contain any vertex-like point: a feasible point may exist only far out along a ray. One must control how far one has to travel along integer combinations of rays and show that this distance has polynomial size.
A second difficulty is uniformity: every intermediate bound must be one polynomial for all dimensions and data. Finally, Theorem 3 is itself a substantial result, cited rather than proved in the paper.
Points are Fin n → ℝ; data are ℚ-valued and cast coordinatewise. Bit-size is Schrijver's: 1 + Nat.size |num| + Nat.size den for a rational, n + Σ for a vector, m·n + Σ for a matrix; the instance size is the sum over . Polynomial bounds are Polynomial ℕ evaluated at a size. The objects defined are: the feasible set of (2); polyhedra , recession cones and pointedness (trivial lineality space); cone as the -span and int.cone as the additive monoid generated (non-negative integer coefficients only); extreme rays of a cone; simple cones as cones of linearly independent generators, whose faces are the cones of subsets of the generators; the Euclidean norm (not Lean's sup norm); and normalizing hyperplanes .
Readings committed to: "is in NP" (Theorem 3, first sentence; Proposition 5) is the existence of polynomial-size certificates; "a system of linear equations of small complexity whose solution is a global optimum" (Theorem 3) is a global optimum of small size, equivalent by Cramer's rule; Claims 1 and 2 are stated with their context (polytope, linearly independent rays, the positivity of on ) as hypotheses and bounds polynomial in those local data.
Every "small complexity" is formalized with the polynomial quantified before the dimensions and the data. With the quantifiers reversed, Theorem 1 is trivially true (take the bound to be the size of any rational feasible point), so such a statement does not count. Likewise the hypothesis of Theorem 1 is non-emptiness over the reals, not the existence of a rational point, and the bit-size counts numerator and denominator bits of every entry.
Needed infrastructure, reusable well beyond this mission: sizes of solutions of rational linear systems (Cramer's rule bounds), vertex and facet complexity of rational polyhedra (Schrijver, Chapter 10), the Minkowski–Weyl theorem with size bounds, Carathéodory's theorem for cones, and Vavasis's theorem. Proofs of any milestone, of these library facts, and of alternative arguments for the goal are all welcome.
Lie's third theorem says that every finite-dimensional Lie algebra is the Lie algebra of a Lie group. -algebras (strongly homotopy Lie algebras) generalize Lie algebras by allowing brackets of every arity, related by the Jacobi identity only up to coherent homotopy. They occur as symmetries in deformation theory, in higher gauge theory and in string theory; a central example is the string Lie 2-algebra of a compact simple Lie algebra. The question "what integrates an -algebra?" asks for a higher-categorical Lie group, and the natural candidate is a simplicial manifold satisfying a manifold version of the Kan condition.
Timeline:
Let be a non-negatively graded real vector space, finite dimensional in each degree. Its Chevalley–Eilenberg algebra is the graded-symmetric algebra on , where sits in degree . An -structure on is a linear map of degree which is a graded derivation and satisfies ; the brackets of are the transposes of the components of on generators.
Fix an integer . On the -simplex , let be the space of -forms such that and have coefficients of class , a Banach space for the norm of and . The integrating simplicial manifold is
with face maps given by restriction to the faces of the simplex. A DGA map is determined by the images of the generators, and generators of degree go to , so is a subset of the Banach space .
The Postnikov pieces and agree with below degree , have , resp. , in degree , and vanish above, where is the unary bracket. A map of simplicial manifolds is a Kan fibration if for all and the map from to the manifold of commutative squares is a surjective submersion (a surjective map with a smooth local section through every point); is Kan if is a Kan fibration.
For every such -algebra and every , each is a smooth manifold, satisfies the Kan condition, and all the maps of the tower
are Kan fibrations.
Theorem 5.10 gives a Lie integration procedure for all non-negatively graded -algebras of finite type, with no nilpotence assumption: its output is a Kan simplicial Banach manifold whose Postnikov tower consists of Kan fibrations. The paper uses it to compute the homotopy sheaves of (Theorem 6.4), to integrate Lie -algebras to Lie -groups by truncation (Theorem 7.5), and to construct a Lie 2-group integrating the string Lie 2-algebra (§8), compared with the Baez–Lauda notion in the appendix.
The result is proved in the paper. None of it is formalized: Mathlib has exterior and symmetric algebras, Fréchet derivatives within sets and the implicit function theorem on Banach spaces, but no -algebras, no Banach spaces of forms on a simplex, and no simplicial manifolds. A formal proof would supply the first machine-checked Lie integration theorem beyond Lie algebras, together with reusable infrastructure: Chevalley–Eilenberg algebras, de Rham forms on simplices with explicit extension operators from horns, and Kan conditions for simplicial Banach manifolds.
The levels are solution sets of nonlinear differential equations (Maurer–Cartan type) in Banach spaces, so their manifold structure is not visible directly. Banach spaces are forced: for Fréchet spaces of smooth forms the implicit function theorem fails, and surjective submersions are not known to form a Grothendieck pretopology. The base of the induction, , is the integration of the ordinary Lie algebra , so it already contains Lie's third theorem and requires maps into a Lie group. The higher stages involve equations twisted by the lower stages, whose solution spaces are not linear. The submersion claims require local smooth sections, not only surjectivity: it does not suffice to extend a form from a horn, the extension must depend smoothly on the data and on a prescribed differential (Lemma 5.11).
L : ℕ → Type, each L i a finite-dimensional real vector space; the -structure is LInfty L, the differential δ on CE L = ExteriorAlgebra(⊕_{i even} L∗ᵢ) ⊗ SymmetricAlgebra(⊕_{i odd} L∗ᵢ) (this tensor product is the graded-commutative one because the symmetric factor is concentrated in even degrees), with degree, graded Leibniz rule (sign from the degree of the left factor) and δ ∘ δ = 0.CrForms r m n, the closed span of the jets (all partial derivatives of order of the coefficients of and of , sup norms on ). The condition on is part of the space.integ r δ ⊤ m, a subset of the Banach space Amb r ⊤ m of generator images (a basis of each , ). The Postnikov pieces are generator systems (tauLe, tauLt) of sub-DGAs of ; .Ride-hailing platforms pay drivers per trip, and drivers are free to decline requests. When demand fluctuates, a trip accepted now also decides where and when the driver will be free next. During a surge (a period of high demand and high pay) a long trip keeps a driver busy after the surge may have ended, so a driver may rationally decline trips the platform wants served. Rejected requests cost riders and platforms reliability, and cherry-picking forces platforms to hide trip information from drivers. N. Garg and H. Nazerzadeh, Driver Surge Pricing (Management Science, 2022; arXiv:1905.07544), ask when a platform can set per-trip payments under which accepting every request is the driver's best response, i.e. payments that are incentive compatible (IC), and what such payments look like. The paper presents itself as "the theoretical foundation that has informed the design of Uber's new additive driver surge mechanism" (abstract), and shows that multiplicative surge, historically the industry standard, is not incentive compatible in a dynamic setting.
The world alternates between two states, a non-surge state and a surge state , as a continuous-time Markov chain that leaves state at rate ( the other state). A driver who is open in state receives trip requests at rate , each with a length drawn independently from a law on . The probability that the world is in state a time after being in state is
A payment function pays for a trip of length that starts in state , whatever the world does during the trip. A policy consists of open sets : the driver accepts a request of length arriving in state iff , is then busy for time , and loses requests arriving meanwhile. With the pay from the trips accepted by time , the driver's earnings rate is
With , and , the paper shows that almost surely
The platform targets per-state earnings for a driver who accepts everything, with . With , the values at accept-all, define
For primitives with bounded densities and finite mean trip lengths:
for all targets with there are prices
meeting the targets, and , such that the policy is optimal; and if , there are such prices for which accepting every request is optimal, and strictly better than every policy that rejects a set of positive - or -measure. Optimality is almost-sure dominance of the stochastic earnings rate, on every probability space carrying the model and from every initial state; prices and are chosen before the competing policy. The printed theorem allows , which nonnegative surge prices cannot meet, so the goal carries the correction .
(Lemma 6), with its continuity and monotonicity properties (Remark 1) and its shape under affine pricing (Lemmas 7, 8).
The theorem identifies when IC surge pricing exists and gives it in closed form: the surge state can always be made IC, while the non-surge state can be made IC exactly when the targets are close enough, . Below , no payment of this form can stop drivers from rejecting long non-surge trips, because accepting one risks missing the surge. The price form separates a per-time rate from a correction for the chance that the world changes during the trip, which is the opportunity cost a driver faces.
The results are proved on paper only; no machine-checked version is known. A formalization would check a proof whose appendix is long and informal in places: the derivative of a set function with respect to interval endpoints, the passage from local sign conditions to global optimality over all open sets, and the reduction from the stochastic process to the closed form. Formalizing it already corrected statements: Theorem 3 needs , Lemma 9 needs , Lemma 10 needs , Remark 1's sign change point may be and its derivative is continuous in only for continuous densities, and Lemma 1 needs integrable payments.
The obvious argument compares accept-all with policies that drop one interval of trip lengths. It fails because competing policies are arbitrary open sets, countable unions of intervals, and the reward is a ratio of integrals over them, so local improvements at one endpoint need not combine into a global maximizer; the paper needs a limiting argument over this set-function domain (Lemma 5). The second obstacle is the link between the closed form and the driver's actual earnings: the trip-start state, the world switching mid-trip and the lost requests make the earnings process a Markov-modulated renewal-reward process, and the liminf must be identified almost surely. Finally, the IC windows of Lemmas 9 and 10 must hold uniformly over the other state's policy, which is where the bound comes from.
Fin 2: Lean 0 is the paper's non-surge state 1 and Lean 1 the surge state 2; sw 0 is .EReal.Internet advertising markets sell impressions, clicks and conversions one auction at a time, and most advertisers attach a budget to a whole campaign. Bidding one's full value until the budget runs out is suboptimal: the buyer drops out early and misses later auctions that may offer the same value at a lower price. A widely used remedy is multiplicative pacing: the platform shades every bid of buyer by a common factor, bidding instead of , with the pacing multiplier chosen so that the budget lasts. When every buyer is paced, the multipliers interact through the prices, and the natural question is whether there is a stable profile of multipliers at all.
Conitzer, Kroer, Sodomka and Stier-Moses (arXiv:1706.07151, Operations Research, 2022) study the static game behind this mechanism for second price auctions, define its equilibrium notion and prove that an equilibrium always exists.
Timeline.
A pacing game has a finite set of buyers and a finite set of divisible goods. Buyer has a valuation for good and a budget . Buyer picks and bids on every good; each good is sold in a single-slot second price auction. Write for the highest bid on other than 's (it is when is the only buyer).
A second price pacing equilibrium (SPPE, Definition 2) is a triple of multipliers , allocations and per-unit prices such that, with spend :
The proof passes through the -smoothed pacing game (Definition 3). A reserve bid is added on every good, treated as one more bidder. With the highest bid, every bidder within of receives a share of good proportional to its distance above , and buyer pays per unit, the highest bid other than hers minus . Each buyer also receives units of an artificial good worth per unit at price . Her utility is the leftover budget , multiplied by when it is negative, plus .
No genericity, no tie assumption and no bound on or : one buyer, no buyers and goods nobody values are all covered.
Theorem 1 makes the SPPE a well-defined solution concept for every instance of the market. The rest of the paper builds on it: SPPE are shown to be best responses (Proposition 2), to refine competitive equilibria of the associated market (§5), and to be the outputs that a mixed-integer program can optimise over; the paper's complexity results (NP-hardness of finding revenue- or welfare-optimal equilibria) presuppose that equilibria exist. The later PPAD-completeness result of Chen, Kroer and Kumar concerns the computation of an object whose existence is this theorem.
The theorem has a published proof; nothing in it has been machine-checked. A formal development needs a pure Nash existence theorem for continuous quasiconcave games, a careful treatment of the smoothed game's continuity, and a compactness-and-limit argument. Each of these is reusable for other smoothing arguments in auction and market design (first price pacing equilibria, throttling equilibria).
The pacing game is discontinuous: a buyer's allocation jumps when her bid crosses another bid, and her utility drops to when she exceeds her budget. So standard existence theorems do not apply to it, and it is not evident a priori that the game with a fixed tie-breaking rule has a pure Nash equilibrium at all (p. 9). Definition 2 also demands a refinement, no unnecessary pacing, that an arbitrary Nash equilibrium need not satisfy. The obvious fixed-point argument on alone fails because the allocation is a correspondence, not a function, at ties.
The smoothing removes the discontinuities, but its limit must be controlled: the reserve buyer must win nothing in the limit on goods someone values, the budget penalty must force feasibility, and the artificial good must force every paced buyer to exhaust her budget. Each limit claim uses a different one of these devices.
N, G (Fintype, with DecidableEq N); all quantities are real. The game PacingGame N G carries and ; infinite budgets are outside the model.highestOther v α i j is a Finset.sup' over the buyers and equals when there is no other buyer, not a junk value of sSup ∅.IsSPPE P α x p has the five conditions of Definition 2 with . The prices are one vector shared by the second-price and the budget conditions; they are existentially quantified in the goal.Option N, with none the reserve bidder bidding . Band weights sum to at least , so the allocation never divides by zero. The price is per buyer (). The utility uses for and for , exactly the paper's two cases.Filter.Tendsto in and in with the product topology.A trivializing formalization is ruled out: the full-allocation condition makes fail whenever some , and the price in the budget condition is the same that the second-price condition pins down, so a zero price is not available to a winner facing a positive competing bid.
Needed infrastructure: a pure Nash equilibrium existence theorem for games with compact convex strategy sets and continuous, own-strategy-quasiconcave payoffs (the Proved platform theorems SocialEquilibrium.Existence.exists_equilibrium_point, Debreu 1952, and FanGlicksberg.kakutani_fan_glicksberg are the natural tools); continuity of finite maxima and quotients with positive denominators; monotonicity arguments for piecewise-linear functions of one variable; and Bolzano–Weierstrass on a bounded subset of . Proofs of any milestone, and alternative routes to Theorem 1, are welcome.
Firms increasingly observe enough about individual customers to charge them different prices, and regulators, platforms and sellers all ask the same quantitative question: how much more profit can personalization earn than a single posted price? The upper end of that comparison is idealized personalized pricing (first-degree price discrimination), where every customer is charged exactly their valuation. Its profit is an upper bound for every price-discrimination scheme, including feature-based pricing, so a bound on the ratio of idealized personalized profit to single-price profit bounds the value of any personalization at once.
Elmachtoub, Gupta and Hamilton (The Value of Personalized Pricing, Management Science 67(10), 2021; SSRN 3127719) give such bounds in terms of three summary statistics of the valuation distribution, all of which can be estimated from data. Their central result, Theorem 2, is a closed-form bound that is tight for every value of the statistics. The bound is exact rather than asymptotic, and it identifies the markets in which no form of price discrimination can be worth much.
A classical special case is the folklore statement that, with only the support known, the worst case is an equal-revenue (truncated Pareto) distribution. Theorem 2 refines it by also fixing the mean absolute deviation of valuations.
A seller has per-unit cost . A random customer's valuation is a random variable with law , finite mean , and almost surely (customers valuing the product below cost are never served profitably). The purchase probability at price is
which counts the customer who values the product exactly at as buying. A single price earns , and the single-pricing profit is
Charging each customer their valuation earns the personalized-pricing profit .
The three statistics are the scale (the essential supremum of relative to its mean, possibly ), the margin , and the coefficient of deviation . With and the negative real branch of the Lambert function (the solution of for ), the regime thresholds are
For every law with scale , margin and coefficient of deviation ,
and for unbounded support the first bound holds for every . Each bound is attained: for every mean, cost, and in a regime there is a law with those statistics for which the regime's bound holds with equality. The goal is stated for a general cost and mean, not only in the standardized case.
In the order the proof uses them:
The theorem turns three estimable numbers into a guarantee. Its reciprocal is the fraction of the personalized-pricing profit that the best single price is certain to earn. When that fraction is close to one (small , or close to its maximum ), no price-discrimination strategy, however refined its data, can improve much on one price. The paper uses Theorem 2 to bound feature-based pricing (its Theorems 4 and 5), and the tight distributions show that no better bound in these statistics exists.
The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. A complete development yields a formal treatment of single-price revenue for general valuation laws (atoms and unbounded support included), the integral representations of mean absolute deviation, and a usable negative Lambert branch, which neither Mathlib nor the platform currently provides (only the principal branch exists on the platform).
The upper bounds rest on bounding the purchase probability pointwise inside an integral representation of and solving the resulting transcendental inequality through . Each step is elementary on paper, but the formal statement has no slack. is a supremum that need not be attained when support is unbounded. counts atoms, so the tight laws sit on atoms at their optimal prices. Every application of must stay in , and the regimes meet at their endpoints, where two bounds coincide.
Tightness is the harder half. It needs genuine probability measures with prescribed cCDFs, mean, scale and deviation, and an exact computation of their single-price profit. Two printed details had to be corrected, and those corrections must be respected. At no law has scale , so tightness is stated for . The high-heterogeneity cCDF of Lemma EC.3 must be left-continuous at , so it keeps an atom at the top of the support.
All declarations live in the namespace ValuePersPricing.Deviation.
ν : Measure ℝ. Market ν c bundles the standing assumptions: probability measure, , almost surely, and integrability of . The margin condition is the hypothesis c < mean ν.(ν (Ici p)).toReal. is the real supremum over all real prices; it is not assumed attained, bounded by an extra hypothesis, or positive. Under Market the profits are bounded by , so the supremum is the true one.IsScale ν S: is the essential supremum. Unbounded ν is the case .lambertWm1 is defined by choice, with a junk value off that no statement reaches.A complete development needs the layer-cake (tail-integral) formula for expectations, the change of variables in interval integrals, pushforwards of measures under affine maps, and analytic facts about on . The Lambert facts and the tail-integral representations of mean absolute deviation are reusable beyond this mission. Contributions are welcome at every milestone. In particular, the milestone and Lemma 3 are independent entry points, and the explicit measures of Lemma EC.3 can be built without the upper-bound half.
Ride-hailing platforms such as Uber and Lyft raise prices when demand spikes, a practice known as surge pricing. The practice is controversial: customers see higher fares, and it is not obvious that anyone but the platform gains. Bernstein, DeCroix and Keskin (MSOM 2020; author version SSRN 3250224) study two competing platforms whose customers dislike waiting and whose drivers dislike idling, and show that in markets with spare driver capacity a demand surge met by re-optimized prices leaves both customers and drivers better off than keeping the old price. This mission formalizes that result (Proposition 3 of the paper) together with the equilibrium characterization it rests on.
Two platforms sell rides. Customers form a continuum of mass (the market size) spread uniformly over locations of a Hotelling line. Platform charges price , and its utilization is , the ratio of the mass of customers served to the mass of active drivers. A customer at gets utility
from platforms 0 and 1, where is the sensitivity to congestion, and chooses the better platform or neither. A driver with operating cost who works for platform keeps per ride (revenue share , commission ) and gets .
Demand depends on supply through and supply depends on demand; the fixed points are the balanced demand and balanced supply , given in closed form by Lemma 1 of the paper. They take one form, , , when the market is partially covered (each platform acts as a local monopoly; Case P, ) and another, , , when it is fully covered (the platforms compete for the customers in the middle; Case F).
Platform earns and must respect the supply constraint . A price is a symmetric Nash equilibrium if , satisfies the supply constraint, and no price in that satisfies the supply constraint against earns more. From §4.1 on, . Proposition 1 divides the plane into four regions; in the two supply-unconstrained ones, Region (a) ( and ) and Region (d) ( and ), drivers are not fully occupied in equilibrium.
For a common price and market size , write , and for the utilities above evaluated at that utilization.
Let , , and with and in Region (a) or (d). Symmetric equilibria and exist, and for all of them:
(i) after a surge with re-optimized prices, customers are worse off and drivers better off,
(ii) there is such that for , at the new market size both sides prefer the new price to the old one,
All inequalities are strict, for every customer location and every driver cost.
The result separates two effects of a demand surge. Part (i) is the expected one: re-optimized prices rise and customers pay more. Part (ii) is the managerial point: compared with a fixed-price policy facing the same surge, raising prices draws in drivers and relieves congestion by enough that customers, too, are better off. This gives a model-based argument for surge pricing in supply-unconstrained markets, and it holds under duopoly competition, not only for a monopolist.
The paper's proofs (in its online supplement) are written out by hand. As far as is known, none of these results has a machine-checked proof. The work here is formalizing the known proofs: the fixed-point computation behind the balanced demand and supply, the equilibrium characterization in two regions, and the comparative statics in the market size.
The obvious argument fixes the equilibrium formulas and differentiates the utilities in . That fails in two places. First, the equilibrium is defined by a best-response condition over a piecewise demand function: a deviating platform can move the market between partial and full coverage, so the global optimality of the candidate price requires controlling the profit across the switch between the two closed forms, not just a first-order condition. Second, the two regions meet along , and a surge from to can cross from Region (d) into Region (a). Part (i) then compares utilities given by different formulas on each side, and part (ii) compares the old price, evaluated in the new market where it may lie in a different coverage case, with the new equilibrium price.
All objects live in the namespace CongestedPlatforms.Surge and take the parameters lam γ α c as explicit real arguments (λ is a Lean keyword), so one game can be evaluated at two market sizes. Balanced demand D and supply S are defined by the closed forms (4.2)–(4.7) with the Case P/F switch on ; Lemma 1 ties them to the balance equations. The action set is read as the natural bounds , and the supply constraint is imposed on the equilibrium price as well as on deviations. Utilities are evaluated for every location and cost in (the location and cost terms cancel), and is an extended real. The source is the SSRN author version of September 16, 2019, whose online supplement holds the proofs.
Standing assumptions and corrections, all stated as hypotheses: ; for the propositions; (the paper's ); and , because at and every profit is zero and every feasible price is an equilibrium, which falsifies Propositions 1 and 3 as printed. Proposition 1(d) additionally assumes (for the printed price exceeds 1), and both parts of Proposition 1 state equality of demand and supply on the region boundaries, where the printed "strictly lower" fails. Proposition 1(a) is stated on a region slightly larger than the printed one (adding ), which contains it.
The goal speaks of symmetric equilibria of the game, not of Proposition 1's formulas: defining the equilibrium price by those formulas, dropping the existence clauses, allowing , evaluating the utilization at the wrong market size, or omitting the congestion term would each trivialize the statement and are excluded.
Only Mathlib is needed (Real.sqrt, min, EReal). Proofs of the milestones are welcome independently; Lemma 1 and the two parts of Proposition 1 are reusable for any comparative-statics question about this model.
A seller who has posted a price for some time usually knows one number about demand: the conversion rate , the fraction of customers who bought at . Whether that single number is enough to price well, and how well, is a basic question of data-driven pricing. Allouah, Bahamou and Besbes (arXiv:2103.05611, Management Science 2023) answer it in a robust, distribution-free model: the seller knows only and a shape restriction on the value distribution, nature chooses the worst distribution consistent with both, and performance is measured against the revenue of an oracle who knows the distribution.
The shape restrictions are the standard ones of mechanism design: regular distributions (non-decreasing virtual value) and distributions with a monotone hazard rate (mhr), both special cases of α-strong regularity (Cole and Roughgarden 2014; Schweizer and Szech 2016). Related robust pricing questions with samples or moment information have been studied by Huang, Mansour and Roughgarden (2018), Allouah, Bahamou and Besbes (2022) and others; the single-conversion-rate setting is the one where the answer can be written in closed form.
A buyer's value has a law ; its ccdf is , and posting the price earns . The oracle revenue is .
For let () and , the generalized Pareto tails. A law is α-strongly regular if is convex where ; gives the regular laws and the mhr laws. The information class is
A mechanism is a law of posted prices; the deterministic mechanisms are the point masses . The performance of against is , and the maximin ratio of a class is
The worst cases form the one-parameter family of truncated generalized Pareto laws , , with and ( at ).
For regular laws,
attained by the price on the same pieces. For mhr laws,
attained by , where is the Lambert function, , , and is the unique root in of , with . The goal states every clause: both values, both attaining prices, existence and uniqueness of , and its numerical bracket.
Theorem 2 gives the exact value of one data point for deterministic pricing and the price to post. For mhr laws, knowing that half of the customers bought at guarantees more than 85% of the oracle revenue; for regular laws a 25% conversion rate guarantees two thirds. It also identifies three regimes: at high conversion rates the incumbent price stays optimal, while at intermediate and low rates the seller should price below . Theorem 1, the reduction underneath it, holds for every mechanism class and is what makes the paper's approximation schemes for randomized mechanisms possible.
The results are proved in the paper; none of them has a machine-checked proof. A formalization would check a long case analysis (sixteen appendix pages) whose printed statements contain slips: Proposition D-1 and Lemma D-1 are false as printed at the normalized price , and Lemma C-2's "the optimal price" is not unique. The mission states the minimal corrections; the corrected statements, not the printed ones, are what the goal's proof needs.
The obvious argument fails at nature's problem. is infinite-dimensional and non-convex, and the ratio is a quotient of two functionals of , so neither convex duality nor a pointwise bound on alone gives the infimum: a law that lowers the numerator may lower even more. The reduction to has to fix the oracle price and its quantile first, and only then compare ccdfs. Afterwards, the closed forms require exact single-crossing and monotonicity facts about ratio curves built from the Lambert function, with separate regimes for below , between and , and above .
Value laws are probability measures on ℝ with no mass on . The ccdf is the closed tail : the paper's data counts values greater than or equal to and its worst cases are atoms at the top of their support, where the two tails differ. α-strong regularity is convexity of on , equivalent to the paper's density form with non-decreasing (p. 11 prints "non-increasing", a slip) and, like the paper, without absolute continuity, so the atom at the top of the support is allowed. Throughout, and . Suprema and infima are real sSup/sInf over sets that are nonempty and lie in ; a minimum over groups of worst cases that may be empty is the infimum of their union. The condition is written , so needs no extended reals, and is its limit form. The Lambert function is the inverse of on .
The goal is stated over the whole class : an infimum over , or Proposition D-1's three curves in place of , would assume the reductions the mission is meant to prove, and dropping the optimal-price clause or the clauses would leave out part of the theorem.
A complete development needs the generalized Pareto calculus (, its inverse, the identity ), convex-function comparison arguments, the Lambert function on (absent from Mathlib), and real-analysis bounds for the numerical bracket of . The α-strong-regularity layer, single crossing and the Lambert function are reusable for other robust pricing results. Proofs of any milestone, and of auxiliary facts about , are welcome.
In many clustering tasks the data come as pairwise judgements rather than as points in a metric space: a classifier says, for each pair of documents, whether they refer to the same entity or not. Correlation clustering asks for a partition that agrees with as many of these judgements as possible, without fixing the number of clusters in advance. The problem was introduced by Bansal, Blum and Chawla, motivated by document clustering and coreference resolution in natural-language processing (Machine Learning 56, 2004). It has since become a standard problem in approximation algorithms.
Timeline:
Let be a finite set and let every pair of distinct vertices carry a label ; this is a complete graph with signed edges. A clustering is a partition of . A pair is a mistake of a clustering if and lie in different clusters (a positive mistake), or and they lie in the same cluster (a negative mistake). The number of mistakes of a clustering is , and .
For a vertex let ; the vertex itself is included. For and , a vertex is -good with respect to if and , and -bad otherwise; is -clean if all its vertices are -good with respect to it. A triangle is erroneous if it has two positive edges and one negative edge.
Algorithm Cautious with maintains a set of remaining vertices, and all of , goodness and below refer to the graph induced on . It repeatedly picks an arbitrary , sets , deletes -bad vertices of one at a time while any exists (giving ), adds at once every vertex of that is -good with respect to , and deletes the resulting cluster from . It stops when is empty, or when every remaining vertex produces the empty set; the remaining vertices become singletons.
Cautious has a run on every , and for every run, with output clustering , and every clustering ,
The bound is required for every pivot sequence and every removal order, because the algorithm leaves those choices open.
In attack order:
Theorem 13 was the first proof that disagreement minimization on complete signed graphs admits a constant-factor approximation by a purely combinatorial algorithm, and its two ingredients have been reused since: erroneous-triangle packings, the standard lower bound behind the analyses of later algorithms, and clean clusters. The constant has since been improved by orders of magnitude, but the structural statements (clean clusterings are -approximate; a near-optimal clustering with clean clusters exists; a cautious greedy procedure recovers it) remain the paper's.
None of this is formalized in any proof assistant. The mission provides a reusable Lean layer for correlation clustering: signed complete graphs as SimpleGraph, disagreement counts over unordered pairs, goodness and cleanliness, triangle packings, and a nondeterministic algorithm specified as an inductive run relation. Formalizing it also repairs the printed argument. Lemma 12 as printed is false (an 18-vertex counterexample is recorded in the item), and the cleanliness clause of Theorem 7 holds only in the remaining graph. The milestones state the corrected versions, which together still yield Theorem 13 with the printed constant.
Every step is elementary counting, but the counts are tight. Lemma 4 needs a charging scheme that gives each mistake its own erroneous triangle while every edge carries total weight at most . Lemma 6 accounts for bad vertices cluster by cluster. Theorem 7 is a double induction, over the clusters produced and over the removal loop. Inside it one must show that no vertex of a clean cluster is ever removed and that the addition step pulls in the rest, uniformly over all removal orders.
The natural first idea, applying the clean-clustering bound (Corollary 5) to the clusters Cautious outputs, fails. The output clusters are clean only relative to the vertex set remaining when each was formed, and an earlier cluster can split a later one from many of its positive neighbours. Positive and negative mistakes therefore have to be bounded separately.
Fintype with decidable equality, possibly empty; G.Adj u v means .R, and the paper's -level notions are the case R = univ. Goodness compares real casts of cardinalities with real multiples of . The constant is the real number δ44, with thresholds , and written as multiples of it.Setoid V. Mistakes are counted over unordered pairs (Sym2).No trivializing reading is admitted. The goal quantifies over every run and asserts that a run exists, so an empty run relation, a single fixed pivot rule or a fixed removal order cannot satisfy it. It compares with every clustering, not with or with clean clusterings only, and goodness is evaluated in the remaining graph, not in .
The PTAS for maximizing agreements (Theorem 22), the NP-hardness reduction (Lemma 1), the warm-up Theorem 2 and the extensions of §7 are not part of this mission. Contributions are welcome on any milestone. The algorithm-free Lemmas 3, 4, 6, 8 and 9 are independent entry points, and a general library of facts about the run relation (termination, disjointness of the clusters, consisting of unclustered vertices) would serve Corollary 10, Theorem 7 and Lemmas 11–13.
Many allocation problems distribute work rather than benefits: household and office tasks, teaching loads, shifts, maintenance duties, or jobs assigned to parallel machines. Each item is a chore, which every agent would rather not receive, and chores cannot be split. Under indivisibility an exactly fair split usually does not exist, so the fair-division literature measures fairness against benchmarks that can be approximately met. The max-min share of Budish (J. Political Economy, 2011) is one of the most studied: it is what an agent could secure by dividing the items into as many bundles as there are agents and receiving the worst of them.
For goods, Kurokawa, Procaccia and Wang showed that an allocation giving every agent her full max-min share need not exist (J. ACM, 2018; conference version AAAI 2016), and attention moved to approximations. Aziz, Rauchecker, Schryen and Walsh (AAAI 2017) started the corresponding study for chores. They showed that chores behave differently from goods with the signs flipped, that a full max-min share allocation of chores may fail to exist, and that computing one is strongly NP-hard. Their first positive result is that the simplest protocol, greedy round-robin, already gives every agent a constant-factor approximation, with a factor that cannot be improved for the protocol.
Timeline:
There are agents and a finite set of items. Agent has an additive utility : is her utility for item , and a bundle is worth . The instance is a chores instance if for all and no is identically zero.
An allocation is a partition of into bundles, some of which may be empty; is the set of all allocations. Agent 's max-min share is
For chores it is non-positive.
The greedy round-robin protocol (Algorithm 1 of the paper) lets the agents pick one item at a time, in rounds; in each round the agents pick in the order , and each picker receives an item of highest utility for her among the items not yet picked. The paper does not specify how ties are broken. A run is the resulting sequence of picks under some tie-breaking rule, and is the set of items agent picked. The worst single chore of agent is .
For every chores instance, every run of greedy round-robin and every agent ,
and the factor cannot be improved: for every and every there is a chores instance with agents on which every run leaves some agent with . The goal also records that the protocol always produces an allocation. It covers every tie-breaking rule and every , so it is the paper's full claim and not a special case.
The theorem shows that the max-min share for chores admits a constant-factor approximation by a protocol that needs no computation beyond each agent's own ranking of the remaining chores. No optimization problem is solved, which matters because computing the max-min share itself is strongly NP-hard (Proposition 8 of the paper). The bound holds for every tie-breaking rule, so it applies to any implementation of the protocol, and the tightness clause shows that improving on needs a different algorithm, not a sharper analysis. Later chores algorithms are measured against this baseline.
The result has a complete paper proof. No machine-checked proof of it is known to exist. Formalizing it produces a checked statement of the round-robin protocol for chores under arbitrary tie-breaking, the pairwise comparison (1) between round-robin bundles, and the elementary upper bounds on the max-min share. These are reusable for other round-robin and max-min share results.
The arithmetic is short. The difficulty is in the protocol. Eq. (1) compares an agent's bundle with another agent's bundle pick by pick, and the comparison has to be set up differently depending on which of the two agents picks first in each round, and on whether their numbers of picks differ by one in the final, possibly incomplete, round. The paper's text calls one of the two orders "obvious", but there the earlier picker may hold one more chore than the later one, and that extra chore is what the term absorbs. The obvious attempt, comparing bundles of equal size, fails exactly in that case.
The tightness clause cannot be checked by running the protocol once: the claim covers every tie-breaking rule, so the instance has to defeat every run of the protocol, not one particular run.
Fin N, with the paper's agent at index (agent 1 is 0); chores are Fin m; utilities are d : Fin N → Fin m → ℝ; bval d i S is ; IsChores d is "all utilities and each agent has a nonzero utility".σ : Fin m ≃ Fin m from picks to chores satisfying IsRoundRobinRun d σ: pick (counted from ) is made by agent , and the chore it takes is, for that agent, at least as good as every chore taken at a later pick. Every tie-breaking rule gives such a , and every such comes from one. Agent 's bundle is rrBundle σ i, the chores taken at picks with .LittleCharity.MMS.mms is reused, applied to bval d i: a maximum over all maps from chores to Fin N (labelled partitions, empty bundles allowed) of the minimum bundle value. For both ranges are finite and nonempty, so the supremum and infimum are the true maximum and minimum.Finset.univ.inf'. The factor is the real number 1 / (N : ℝ). The guarantee is stated for all non-positive utilities, without the condition , which it does not need. The tightness clause requires a chores instance in the paper's full sense.Finset.inf', and suprema and infima over finite types are all in Mathlib. Results about round-robin bundles, such as eq. (1) and the averaged bound, and the two max-min share bounds are reusable beyond this mission. Contributions to any milestone are welcome, as are alternative proofs of the tightness computation.A quantum channel transmits classical information with an efficiency limited by the noise it adds. One measure of that noise is the minimal output entropy: the smallest entropy the channel's output can have when the input is a pure state. The additivity conjecture asked whether using two channels in parallel, with inputs that may be entangled across them, can ever produce less output entropy than the two channels used separately. Shor showed that this conjecture is equivalent to additivity of the Holevo capacity and of the entanglement of formation (Shor 2004); Hastings later showed that it fails in general (Hastings 2009). Before that counterexample, and independently of it, the question was settled channel by channel.
The Werner–Holevo channel is a standard test case. Werner and Holevo introduced it as a counterexample to multiplicativity of maximal -norms for large (Werner, Holevo 2002), so it is precisely the kind of channel for which additivity cannot be taken for granted. Its history in this question:
There are sites; site carries with , and the joint space has the product basis indexed by configurations . For the Werner–Holevo channel acts on matrices by
the transpose taken in the standard basis; on a density matrix this is , the paper's (6). The product channel is the linear map on matrices of the joint space that acts as on product matrix units.
For a density matrix (positive semidefinite, trace one), the von Neumann entropy is and the -Rényi entropy, , is
with . For a channel , the minimal -Rényi output entropy (1) is
the infimum over all unit vectors of the input space. For the product channel these are all unit vectors of , entangled ones included.
For every , every and every ,
together with the statement that both infima are taken over sets bounded below.
with the reduced matrix of on the sites in . 3. Trace of products of marginals ((8), second line): . 4. Purity of the output ((8)): every line of the computation, ending in
The theorem identifies an explicit family of channels, with an entangling structure and a known failure of -norm multiplicativity for large , on which the minimal output entropy is additive for any number of factors and any mixture of dimensions. Because the channels are irreducibly covariant, the Holevo capacity of such a product equals the log of its output dimension minus its minimal von Neumann output entropy, so the case makes the Holevo capacity of these products additive, with value in natural units. The range is equivalent to multiplicativity of the maximal -norms in that range, which complements the Werner–Holevo counterexample for large .
The result is proved, in the four pages of the paper; no machine-checked proof of it is recorded. Formalizing it produces a self-contained development, on Mathlib alone, of partial traces and tensor products of matrices over site-dependent dimensions, the matrix-unit tensor product of channels, Rényi entropies through the functional calculus, and a complete proof of an additivity theorem that covers entangled inputs.
The upper bound is easy: product inputs achieve the sum, by additivity of on tensor products. The whole content is the lower bound over entangled inputs, and the natural first idea, to bound of the output factor by factor, does not apply: an entangled input has no factors, and entropy is not subadditive in the needed direction. The paper avoids spectra entirely and bounds the purity ; carrying this out in Lean means proving the subset expansion of the product channel for arbitrary , a partial-trace identity for pairs of overlapping site sets, and an inclusion–exclusion collapse of a double sum over subsets, all over dependent configuration types, and then the comparison of Rényi orders for matrices.
Fin N from ; the joint basis is indexed by (j : Fin N) → Fin (d j), and site subsets are Finset (Fin N). Vectors are plain functions to ; is star φ.sInf of a set unbounded below is in Lean, the goal and milestone 1 conclude that the sets are bounded below.Contributions are welcome on each milestone. Milestones 3, 5 and 6 are general facts about partial traces and Rényi entropies, reusable beyond this mission.
We investigate the maximum rates for transmitting quantum information, distilling entanglement, and distributing secret keys between a sender and a receiver in a multipoint communication scenario, with the assistance of unlimited two-way classical communication involving all parties. First we consider the case where a sender communicates with an arbitrary number of receivers, so called quantum broadcast channel. Here we also provide a simple analysis in the bosonic setting where we consider quantum broadcasting through a sequence of beamsplitters. Then, we consider the opposite case where an arbitrary number of senders communicate with a single receiver, so called quantum multiple-access channel. Finally, we study the general case of all-in-all quantum communication where an arbitrary number of senders communicate with an arbitrary number of receivers. Since our bounds are formulated for quantum systems of arbitrary dimension, they can be applied to many different physical scenarios involving multipoint quantum communication.
This mission is the statement-level formalization of General bounds for sender-receiver capacities in multipoint quantum communications (arXiv:1603.07262v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Broadcast Choi teleportation simulation (§III, Eq.(28) and Fig.3: broadcast Choi teleportation simulation, PDF p. 6). 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.
16 results of the paper are not stated yet, because the library lacks an interface they need:
We consider quantum and private communications assisted by repeaters, from the basic scenario of a single repeater chain to the general case of an arbitrarily-complex quantum network, where systems may be routed through single or multiple paths. In this context, we investigate the ultimate rates at which two end-parties may transmit quantum information, distribute entanglement, or generate secret keys. These end-to-end capacities are defined by optimizing over the most general adaptive protocols that are allowed by quantum mechanics. Combining techniques from quantum information and classical network theory, we derive single-letter upper bounds for the end-to-end capacities in repeater chains and quantum networks connected by arbitrary quantum channels, establishing exact formulas under basic decoherence models, including bosonic lossy channels, quantum-limited amplifiers, dephasing and erasure channels. For the converse part, we adopt a teleportation-inspired simulation of a quantum network which leads to upper bounds in terms of the relative entropy of entanglement. For the lower bounds we combine point-to-point quantum protocols with classical network algorithms. Depending on the type of routing (single or multiple), optimal strategies corresponds to finding the widest path or the maximum flow in the quantum network. Our theory can also be extended to simultaneous quantum communication between multiple senders and receivers.
This mission is the statement-level formalization of Capacities of repeater-assisted quantum communications (arXiv:1601.00966v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Widest path: equality with the minimum maximum-edge cut (Proposition 12, Eq.(131), PDF p. 24). 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.
56 results of the paper are not stated yet, because the library lacks an interface they need:
We identify a special information-theoretic property of quantum field theories with holographic duals: the mutual informations among arbitrary disjoint spatial regions A,B,C obey the inequality I(A:BC) >= I(A:B)+I(A:C), provided entanglement entropies are given by the Ryu-Takayanagi formula. Inequalities of this type are known as monogamy relations and are characteristic of measures of quantum entanglement. This suggests that correlations in holographic theories arise primarily from entanglement rather than classical correlations. We also show that the Ryu-Takayanagi formula is consistent with all known general inequalities obeyed by the entanglement entropy, including an infinite set recently discovered by Cadney, Linden, and Winter; this constitutes strong evidence in favour of its validity.
This mission is the statement-level formalization of Holographic Mutual Information is Monogamous (arXiv:1107.2940v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two classical three-qubit states have opposite tripartite information (§2, (2.1)–(2.2): classical positive and negative I3, PDF p. 5). 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.
14 results of the paper are not stated yet, because the library lacks an interface they need:
This paper addresses some general questions of quantum information theory arising from the transmission of quantum entanglement through (possibly noisy) quantum channels. A pure entangled state is prepared of a pair of systems and , after which is subjected to a dynamical evolution given by the superoperator . Two interesting quantities can be defined for this process: the entanglement fidelity and the entropy production . It turns out that neither of these quantities depends in any way on the system , but only on the initial state and dynamical evolution of . and are related to various other fidelities and entropies, and are connected by an inequality reminiscent of the Fano inequality of classical information theory. Some insight can be gained from these techniques into the security of quantum cryptographic protocols and the nature of quantum error-correcting codes.
This mission is the statement-level formalization of Sending quantum entanglement through noisy channels (arXiv:quant-ph/9604023v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
29 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §6.2, equations (24)–(25): quantum Fano inequality (§6.2, equations (24)–(25): quantum Fano inequality, PDF p. 27). 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:
Mutual information is the reciprocal information that is common to or shared by two or more parties. Quantum mutual information for bipartite quantum systems is non-negative, and bears the interpretation of total correlation between the two subsystems. This may, however, no longer be true for three or more party quantum systems. In this paper, we propose an alternative definition of multipartite information taking into account the shared information between two and more parties. It is non-negative, observes monotonicity under partial trace as well as completely positive maps, and equals multipartite information measure in literature for pure states. We then define multiparty quantum discord, and give some examples. Interestingly, we observe that quantum discord increases when measurement is performed on a large number of subsystems. Consequently, the symmetric quantum discord, which involves measurement on all parties, reveals the maximal quantumness. This raises question on the interpretation of measured mutual information as classical correlation.
This mission is the statement-level formalization of Multiparty Quantum Mutual Information: An alternative definition (arXiv:1504.07176v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Alternative multipartite information is nonnegative (Theorem 1, 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.
6 results of the paper are not stated yet, because the library lacks an interface they need:
If two separated observers are supplied with entanglement, in the form of pairs of particles in identical partly-entangled pure states, one member of each pair being given to each observer; they can, by local actions of each observer, concentrate this entanglement into a smaller number of maximally-entangled pairs of particles, for example Einstein-Podolsky-Rosen singlets, similarly shared between the two observers. The concentration process asymptotically conserves {\em entropy of entanglement}---the von Neumann entropy of the partial density matrix seen by either observer---with the yield of singlets approaching, for large , the base-2 entropy of entanglement of the initial partly-entangled pure state. Conversely, any pure or mixed entangled state of two systems can be produced by two classically-communicating separated observers, drawing on a supply of singlets as their sole source of entanglement.
This mission is the statement-level formalization of Concentrating Partial Entanglement by Local Operations (arXiv:quant-ph/9511030v1). 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 Entropy-efficient exact singlet concentration (Abstract, §I: asymptotically efficient concentration of pure entanglement, PDF p. 1). 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.
5 results of the paper are not stated yet, because the library lacks an interface they need:
A unitary interaction coupling two parties enables quantum communication in both the forward and backward directions. Each communication capacity can be thought of as a tradeoff between the achievable rates of specific types of forward and backward communication. Our first result shows that for any bipartite unitary gate, coherent classical communication is no more difficult than classical communication -- they have the same achievable rate regions. Previously this result was known only for the unidirectional capacities (i.e., the boundaries of the tradeoff). We then relate the tradeoff curve for two-way coherent communication to the tradeoff for two-way quantum communication and the tradeoff for coherent communiation in one direction and quantum communication in the other.
This mission is the statement-level formalization of Bidirectional coherent classical communication (arXiv:quant-ph/0412126v3). 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 Bidirectional coherification with arbitrary signed entanglement (Theorem 1, Eqs. (2)–(3), 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:
A general method for proving continuity of the von Neumann entropy on subsets of positive trace-class operators is considered. This makes it possible to re-derive the known conditions for continuity of the entropy in more general forms and to obtain several new conditions. The method is based on a particular approximation of the von Neumann entropy by an increasing sequence of concave continuous unitary invariant functions defined using decompositions into finite rank operators. The existence of this approximation is a corollary of a general property of the set of quantum states as a convex topological space called the strong stability property. This is considered in the first part of the paper.
This mission is the statement-level formalization of Continuity of the von Neumann entropy (arXiv:0904.1963v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1: barycentric representation of the closed convex hull (Lemma 1: barycentric representation of the closed convex hull, PDF p. 5). 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.
19 results of the paper are not stated yet, because the library lacks an interface they need: