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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
Every Bitcoin transaction input is authorized by running a small stack program: the input's scriptSig followed by the spent output's scriptPubKey, on the same stack, and the spend is valid when the program leaves a true value on top. Nearly every historical consensus failure in Bitcoin touched this interpreter — the disabled opcodes (CVE-2010-5137), the concatenation bug that let any output be spent (CVE-2010-5141), the overflow in numeric opcodes that prompted the four-byte limit, the CHECKMULTISIG off-by-one that consumes an extra element. Bitcoin Core's EvalScript is 800 lines of C++ with a switch over a hundred opcodes, and VerifyScript wraps it with the pay-to-script-hash and witness-program rules. (interpreter.cpp, script.h)
This mission transcribes the legacy execution path (SigVersion::BASE) — the number representation CScriptNum, the truth test CastToBool, the full non-push opcode table of EvalScript with its resource limits, and VerifyScript for output scripts that are neither pay-to-script-hash nor witness programs — and proves the properties the rest of validation relies on: that script numbers round-trip and are minimal, that truth is "nonzero as a number", that the resource limits and the disabled-opcode rule behave as stated, and that the two classic payment templates do exactly what they are meant to.
A byte is an 8-bit word and a stack element is a list of bytes. A script number is a little-endian magnitude whose last byte's top bit is the sign: reads it, writes the shortest such encoding (appending a sign byte when the magnitude's top bit is already set), and the CScriptNum constructor rejects encodings longer than four bytes (five for the lock-time opcodes) and, under MINIMALDATA, non-minimal ones. is true when some byte is nonzero, except that a negative zero (0x80 after zero bytes) is false.
A script is the sequence of instructions GetOp yields: a data push carrying its bytes, or a non-push opcode. The interpreter's state is the main stack, the alt stack, the condition stack vfExec, and nOpCount; stacks are lists with the top first. One step on a push checks the 520-byte element limit and pushes when all conditions are true; on an opcode it counts it against the 201-operation limit (only opcodes above OP_16 count, as in the source: OP_1NEGATE, OP_RESERVED and the small-integer pushes are exempt), rejects the fifteen disabled opcodes regardless of execution state, and when executing (or for IF/NOTIF/ELSE/ENDIF always) runs the opcode's case — pushes of small integers, flow control, the stack-manipulation family, EQUAL, the numeric family on four-byte operands, WITHIN, the hash opcodes, CODESEPARATOR, CHECKSIG, CHECKMULTISIG with its key-count accounting, the NOPs, and CHECKLOCKTIMEVERIFY/CHECKSEQUENCEVERIFY when their flags are set — then checks the 1000-element stack limit. Hashes, the lock-time checks, and the signature check (with its encoding rules and FindAndDelete) are an abstract oracle, exactly the role of BaseSignatureChecker and the hash primitives in the source. Running a script steps through it and fails on an unbalanced conditional; verifying evaluates scriptSig then scriptPubKey and requires a non-empty stack with a true top.
for all signatures, keys and hashes within the 520-byte element limit, every flag setting and every oracle. This is BitcoinScript.p2pkh_correct: the template that carries most of Bitcoin's history is correct against the transcribed interpreter, in both directions, with the signature check and hash left abstract. It is the weakest stable statement, since it fixes nothing about the oracle.
serialize_roundtrip): for every integer.serialize_minimal): the serializer's output always passes the minimal-encoding test; (toNum_serialize): a serialized number of at most four bytes is accepted by the strict constructor and reads back as itself.castToBool_iff): , for every byte string, including both encodings of zero.eval_pushes): a push-only script within the element and stack limits leaves exactly its pushes, top-first.disabled_fails): a script containing any of the fifteen disabled opcodes fails from every state, executed or not.op_count_fails): a script with more than 201 counted opcodes (non-push opcodes above OP_16) never succeeds.p2pk_correct): against succeeds iff the oracle accepts the signature.The goal and milestones give kernel-checked semantics for the pieces of the legacy interpreter that every later layer consumes. The number theorems fix what CScriptNum means on the wire and show the interpreter's own outputs are always minimal — which is why MINIMALDATA can be a policy rule. The truth theorem is what makes VERIFY, IF and the final check well-defined on arbitrary byte strings. The limit and disabled-opcode theorems are the denial-of-service and CVE-2010-5137 defences, stated as universal properties of the transcription rather than of test cases. And the template theorems are the first end-to-end statements that a real Bitcoin spending condition is enforced by the code, modulo the cryptography.
What is deliberately abstract: hash functions, the signature check with its DER/strict-encoding rules and FindAndDelete, and the lock-time checks. These are oracle fields, so every theorem holds for every oracle; instantiating them is the work of the hash, sighash and signature layers. Not modeled: byte-level script parsing (GetOp, MAX_SCRIPT_SIZE), pay-to-script-hash and witness programs in VerifyScript, SegWit v0 and Tapscript execution, and the policy flags (MINIMALDATA, NULLFAIL, CONST_SCRIPTCODE, DISCOURAGE_UPGRADABLE_NOPS, MINIMALIF), which are fixed to off as in block validation.
Status: all statements are open with intentional placeholder proofs. The opcode table has been checked by evaluation against the source's documented stack effects (x1 x2 x3 -- x2 x3 x1 and the like) and the CVE-2010-5137 and limit behaviours; nothing about compiled Bitcoin Core is claimed.
The number round-trip looks like bookkeeping until the sign byte: when the magnitude's top byte already has bit 7 set, the serializer appends a whole byte for the sign, and the reader must then see a cleared top bit on that extra byte while the magnitude is unchanged. The proof splits on this case and on the sign, and needs the precise effect of |= 0x80 and & 0x7f on bytes below 128. Minimality has the matching trap: the serializer never emits a trailing zero magnitude byte, which is what makes its output pass the test.
For the templates, the naive approach is to compute. It works, but only after the interpreter's resource checks are discharged on every step — the element size on each push, the op count on each opcode, the stack size after each step — which is why the template theorems carry element-size hypotheses and why the push lemma is stated with its limits. For the op-count theorem the trap is CHECKMULTISIG, which adds its key count to nOpCount mid-execution; the invariant has to allow that increase while keeping it under the limit.
Bytes are BitVec 8; numbers are Int with natAbs for the magnitude; bit tests are the source's masks (& 0x80, & 0x7f, | 0x80) read through toNat. Stacks are Lists, top first; the stacktop(-k) indexing of the source becomes position . Scripts are List Instr. execOp is one if-chain mirroring the switch; step performs the per-iteration checks in the source's order; run is the loop plus the final conditional check; evalScript returns the main stack. Flags carries CHECKLOCKTIMEVERIFY, CHECKSEQUENCEVERIFY and NULLDUMMY; fRequireMinimal is false. The oracle's checkSig returns none where an encoding check fails the whole script and some b for the signature verdict.
A trivializing formalization would define verifyScriptPlain on the two templates directly, or let the oracle see the script; the interpreter is the full opcode table and the oracle sees only the stack elements it is handed. Restricting the templates to canonical sizes beyond the 520-byte limit is out of scope.
No Mathlib is required; the development imports only Std. Proofs in any order are welcome; lemmas about individual opcodes' stack effects are reusable for every later script theorem.
EvalScript, VerifyScript, CastToBool, EvalChecksigPreTapscript, src/script/interpreter.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. SourceCScriptNum, opcode table, MAX_SCRIPT_ELEMENT_SIZE, MAX_OPS_PER_SCRIPT, MAX_STACK_SIZE, MAX_PUBKEYS_PER_MULTISIG, src/script/script.h, and GetScriptOp, src/script/script.cpp, same revision. SourceBitcoin has no trusted clock. A block's timestamp is chosen by its miner, so the consensus rules constrain it from two sides: it must exceed the median time past of the previous eleven blocks (time-too-old), and it must not run more than two hours ahead of the validating node's own clock (time-too-new). The median, rather than the previous block's time, is what makes the rule robust to a few manipulated timestamps, and since BIP113 the same median is the clock against which time-based lock-times are evaluated. The remaining contextual header rules fix the required difficulty bits and refuse block versions that predate the BIP34, BIP66 and BIP65 soft forks once those are active. (GetMedianTimePast, ContextualCheckBlockHeader, CMainParams)
One property of this design is used everywhere but stated nowhere in the code: along any chain that obeys time-too-old, the median time past never decreases. It is what makes a time-based lock, once satisfied, stay satisfied. This mission transcribes the median and the contextual rules and proves that property.
A chain of ancestors is represented by the list of its block times, most recent first. The window is the first eleven entries (nMedianTimeSpan), or all of them for a shorter chain. The median time past sorts the window and takes the element at index ; for an even-length window this is the upper of the two middle elements, as the source's pbegin[(pend - pbegin) / 2]. For an empty chain the model returns , a case the source never queries.
A header carries a version, a time and nBits. For a buried deployment, DeploymentActiveAfter(prev) holds when reaches the activation height: for BIP34, for BIP66, for BIP65. The version floor rejects a version below 2, 3 or 4 when the corresponding deployment is active. The contextual check of a header against its predecessor requires: nBits equals the required work (supplied by the caller, as GetNextWorkRequired computes it in the proof-of-work development); the time strictly exceeds the predecessor's median time past; the time is at most the local clock plus seconds; and the version is not outdated. Mainnet has enforce_BIP94 = false, so the testnet timewarp rule is absent.
For a chain of block times (most recent first) in which every block satisfies time-too-old against its predecessor — for every — the median time past of every suffix is at most that of every shorter suffix:
This is BitcoinHeader.mtp_mono_chain. It is the clock-monotonicity that BIP113 and BIP68 time locks rely on.
mtp_mem_window, mtp_mem): for a non-empty chain the median is one of the window's times, hence one of the chain's.mtp_bounds): the median lies between any lower and upper bound of the window.mtp_take): the median of a chain equals the median of its first eleven times.mtp_mono): if then . The heart of the goal, by a counting argument on the sorted window.versionOutdated_iff): the rejection condition as a disjunction of height thresholds.contextualCheck_iff): acceptance as a conjunction of the four rules.version_floor): an accepted header has version at least 2, 3, 4 after the respective heights.The goal is a kernel-checked statement about the transcribed median: appending blocks that pass time-too-old can only move the median forward. Together with the characterization of the contextual check it gives the exact semantics of Bitcoin's block clock: bounded from below by a non-decreasing median, from above by local time plus two hours.
Formalizing adds the general proof of a fact usually argued by example. The argument is a counting one: the median of a window of sorted times is the smallest value with at least window elements at or above it; appending a time above the old median and dropping at most one old element keeps that count high enough, including when the window is still growing in the first ten blocks of a chain.
Not in scope, and stated as such: the computation of the required nBits (the proof-of-work mission), the local-clock model behind NodeClock::now(), checkpoints, minimum chain work, and the CheckBlockHeader proof-of-work test itself. Status: all statements are open with intentional placeholder proofs.
The naive argument — "the new time is larger than the median, so the median cannot fall" — overlooks that the window also loses its oldest element, which may have been one of the elements above the median. The proof must show that losing one such element and gaining one keeps at least elements at or above the old median. A second subtlety is the growing window: for the first ten blocks the window length increases by one and the median index may move, so the count required changes from to ; the two cases are not the same inequality. The even-length convention (upper middle) is what makes the bookkeeping close.
Times are Int, as int64_t block times. The window is List.take 11, the sort is List.mergeSort on ≤, and the median is getD (length / 2) 0. The required nBits is a parameter of the check. Heights are Nat. enforce_BIP94, checkpoints and minimum chain work are not modeled.
A trivializing formalization would define the median as the previous block's time, or sort with a different index convention; the definitions follow the source's sort-and-index. Assuming the chain's times are themselves sorted is ruled out: the goal assumes only the time-too-old rule.
No Mathlib is required; the development imports only Std. The counting lemmas on sorted lists are reusable for any later median-based rule.
CBlockIndex::GetMedianTimePast, src/chain.h at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. SourceContextualCheckBlockHeader, src/validation.cpp, same revision. SourceDeploymentActiveAfter, src/deploymentstatus.h, and CMainParams activation heights, src/kernel/chainparams.cpp, same revision. SourceBitcoin nodes must agree on whether a transaction may spend its inputs yet. Since 2016 that decision includes relative lock-time: an input may declare that the output it spends must have been confirmed for a minimum number of blocks or a minimum elapsed time before it becomes spendable. The rule is defined by BIP68 and enforced on mainnet by three helper functions in Bitcoin Core: CalculateSequenceLocks, EvaluateSequenceLocks, and SequenceLocks (pinned source). Payment channels, atomic swaps, and vault constructions depend on this rule to enforce dispute windows; a node that decodes a sequence word differently from its peers can accept or reject a block the rest of the network treats the other way.
The specification is short and the implementation is about seventy lines, yet the two are written in different languages. BIP68 speaks of bits, masks, and elapsed delays; the implementation folds inputs into two signed thresholds compared against the candidate height and its ancestor's median time. Whether these agree, for every 32-bit sequence word and every input list, is the question this mission settles. Absolute lock-time (nLockTime) already has a Lean treatment in btc-verified, whose consensus documentation lists BIP68 as outstanding work.
An input is a pair : an unsigned 32-bit sequence word and the coin height of the output being spent. A context is a pair : the candidate block height and a total function giving the median time past of each ancestor height. Write ; natural-number subtraction in Lean truncates at zero and realizes this directly.
Three fields of matter. The disable bit is bit 31. The type bit is bit 22: set means a time-based lock, clear means a height-based lock. The delay is the low sixteen bits; for a time lock it denotes seconds. Enforcement holds when the transaction version is at least 2 and bit 0 of the validation flags is set.
The declarative model (BIP68_Model) expresses these as arithmetic on viewed as a natural number: , . A single input is satisfied when
A transaction satisfies BIP68 when or every input is satisfied. The model also fixes the expected height list: each input's coin height, replaced by exactly when holds and is set.
The Core transcription (BIP68_Core) uses bit-vector masks 0x80000000, 0x00400000, 0x0000ffff and a left shift by 9. An accumulator holds two signed thresholds and a reversed height list, starting at . Each enabled, non-disabled input updates for a time lock or for a height lock. Evaluation succeeds when and . When is false, the fold is skipped and the original heights are returned.
Under the admissible domain (, every , every for ) and the no-overflow condition (for every enforced, non-disabled input, the sum selected by fits its signed destination before the subtraction of one),
and the height list returned by the fold equals the expected height list. This is BitcoinBIP68.core_correct.
decode_sequence): for every 32-bit word, the mask tests agree with the quotient-and-remainder tests, the masked delay equals , and the shifted seconds equal . No hypothesis on unused bits.fold_acceptance): for any starting accumulator, evaluating the fold succeeds iff evaluating the starting accumulator succeeds and every input is satisfied. No range or monotonicity assumptions.height_vector): the returned list has the original length and order, with zeroes exactly at enforced, disabled inputs, including repeated entries and the empty list.calculated_bounds): under admissibility and no-overflow, and , preserving the sentinel.The goal is a kernel-checked statement that a Lean transcription of the pinned Core helpers decides exactly the BIP68 spending condition on the admissible domain, and that its side effect on the per-input height list is the one BIP68 describes. Both directions matter: a lock the implementation accepts is one the specification accepts, and a lock the specification accepts is one the implementation accepts.
Formalizing it adds three things beyond the prose specification. It makes the overflow preconditions explicit, which BIP68 leaves implicit and Core leaves to callers. It separates the bit-level decoding (a bv_decide-style fact) from the aggregation logic (an induction over the input list), so each can be audited on its own. And it produces reusable definitions — Input, Context, the admissibility and overflow predicates — for a later whole-block validation development in which the caller obligations (supplying coin heights, ancestor clocks, activation flags, and coinbase exclusion) are discharged.
Status: the statements compile with intentional sorry placeholders and have independent read-backs. Differential checks ran 2,014 cases against extracted Core helper bodies; these test the transcription, not the theorems. No proof of any statement is claimed.
The natural first idea is to prove core_correct by unfolding everything and calling a decision procedure. It fails because the two sides live in different arithmetic. The implementation computes thresholds in signed integers after subtracting one; the specification compares unsigned sums with . The equivalence holds only because the sentinel is below every admissible height and because each is formed without wrap-around. Both facts need the admissibility and no-overflow hypotheses, and the proof must thread them through the fold.
A second trap is the disabled input. In the model, a disabled input is satisfied unconditionally; in the fold, it leaves both thresholds unchanged but still appends to the height list only when enforcement is on. height_vector records this asymmetry; a proof that treats disabled inputs as absent gets the height list wrong.
A third is the median-time function. is arbitrary: not monotone, not bounded outside . The theorems are stated for this weaker model deliberately, so any proof that assumes a well-formed chain is proving a different statement.
The development commits to the following conventions, all fixed in BIP68_Model and BIP68_Core. Sequence words, versions, and flags are BitVec 32. Heights and times are Nat in the model and Int in the accumulator. on Nat truncates at zero, matching max(h-1, 0) in the source. Input lists are finite Lists; the empty list is in scope. The predicates specEnabled, specDisabled, and specTimeBased are Prop with decidability instances; the Core-side tests are Bool. Admissibility and no-overflow are the only hypotheses on core_correct; fold_acceptance and height_vector carry none.
A trivializing formalization would define satisfiesBIP68 by calling sequenceLocks; the model is written independently from the BIP text and must stay that way. Weakening the no-overflow hypothesis to a vacuous one, or restricting to nonempty lists, is out of scope.
Dependencies: Lean 4 core and Std only; no Mathlib. The two definitions are published first and imported by every theorem. Proofs of the four milestones in any order are welcome, as are lemmas on coreStep reusable by the goal. Out of scope: the C++-to-Lean correspondence (documented, not proved), coinbase exclusion, activation selection, and block-level composition, which belong to a separate whole-consensus mission that will import these results.
CalculateSequenceLocks, EvaluateSequenceLocks, SequenceLocks, src/consensus/tx_verify.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Source2fdeb40c. LockTime.lean, consensus coverageA Bitcoin block header commits to its transactions through a single 32-byte Merkle root: the transaction hashes are paired and hashed, the results paired and hashed again, until one hash remains. Every node recomputes this root from the block body and rejects the block if it does not match the header. Bitcoin's construction has a quirk that later became a vulnerability: when a level has an odd number of hashes, the last one is duplicated before pairing. Consequently the transaction lists and have the same root, and an attacker could relay the second, invalid, block with the first block's header; a node that marked that header permanently invalid would then reject the genuine block (CVE-2012-2459). Bitcoin Core defends by detecting, at every level, two equal adjacent hashes in an aligned pair and treating the block as having a bad root. (ComputeMerkleRoot and the comment above it.)
This mission transcribes that loop and proves that the defence does what its comment claims for the general form of the construction: duplicating any aligned block of trailing leaves preserves the root and is detected, at the level where that block has collapsed to one node.
Hashes are an arbitrary type with decidable equality; the pairwise hash is an abstract (in the source, SHA256D64 on the two concatenated hashes), and the zero hash returned for an empty list is an abstract . The three operations are, for a list of hashes :
hashes.push_back(hashes.back()) followed by the pairwise hashing.computeMerkleRoot returns the pair (root, mutated), exactly as ComputeMerkleRoot(hashes, &mutated).
For every , every non-empty prefix whose length is a multiple of , and every block of exactly hashes,
This is BitcoinMerkle.dup_block. The alignment hypotheses are what make collapse to a single node at level , where the duplicate then sits in an aligned pair; is needed because a list of one hash is its own root while a list of two is not. With it is the classic duplicated-last-transaction case; with it is the example of the source comment.
root_nil, root_single, root_pair): the empty list gives ; one hash gives ; two give .rootLoop_fst): the root does not depend on the incoming flag.rootLoop_sticky): once set, the flag stays set through the remaining levels.pairUp_append_even, hasEqualPair_append_even): for even, and likewise for the pair test.dup_leaf): the goal at , stated directly.The goal is a kernel-checked statement about the transcribed loop: for the entire family of duplications that CVE-2012-2459 is built on, the root is unchanged and the mutation flag is raised. Together with the base cases it fixes the exact semantics of the odd-level rule and of the check, including the fact that the self-pairing of a duplicated trailing element is never itself flagged.
What the result does not say is also worth stating. It does not claim that every root collision is detected; that would require assumptions on the hash function (the source comment says "assuming no double-SHA256 collisions"), and is here an arbitrary function. Nor does it claim anything about the byte-level SHA256D64 or about transaction serialization; those belong to the hash and serialization layer. What formalizing adds is the general statement with its precise alignment conditions, which the source states only by example.
Status: all statements are open with intentional placeholder proofs. Nothing about compiled Bitcoin Core is claimed.
The natural first attempt is to compute both sides for small lists and generalize. It fails on the -level statement because the two lists differ in length by and go through levels before the duplicate appears as a pair. The argument has to track two facts through the loop at once: that the root is insensitive to the flag (so the two runs can be compared level by level with different flags), and that the flag, once raised at level , survives to the end. Both are separate milestones for that reason.
The alignment hypotheses are the second trap. Without the block straddles a pair boundary and its two copies do not collapse to equal nodes; without the copies collapse at different levels. The theorem is false without them, and the base case shows that non-emptiness is needed too.
is a type parameter with DecidableEq; and are parameters. Lists are Lean Lists, so pairUp and hasEqualPair are structurally recursive, and rootLoop is defined by well-founded recursion on the list length with the lemma supplied in the definition file to justify termination. Equality in hasEqualPair is decide (a = b) on , matching hashes[pos] == hashes[pos + 1] on uint256. The mutated pointer being null in the source (as in BlockWitnessMerkleRoot) only suppresses the output; the model always computes the flag.
A trivializing formalization would restrict to a type with a trivial hash or define the root by a different, non-duplicating rule; the definitions are fixed to the source's loop. Out of scope: MerkleComputation (Merkle branches), BlockMerkleRoot's leaf extraction, the witness root's zero coinbase leaf, and any collision-resistance assumption on .
No Mathlib is required; the development imports only Std. Proofs of milestones in any order are welcome, and the distribution lemmas are reusable by any later Merkle-branch work.
ComputeMerkleRoot, src/consensus/merkle.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48, lines 16–73 including the CVE-2012-2459 comment. SourceEvery Bitcoin block may create new coins through its coinbase transaction, and the amount it may create is fixed by consensus: a block subsidy that starts at fifty bitcoin and halves every 210,000 blocks, plus the fees of the block's other transactions. The schedule is the mechanism behind the often-quoted cap of twenty-one million bitcoin, yet the cap appears nowhere in the code as a rule. What the code enforces is the per-block subsidy, computed by GetBlockSubsidy in validation.cpp, and the check in ConnectBlock that the coinbase pays no more than fees plus subsidy. The cap is a consequence, and the only place a number near it appears is MAX_MONEY, a sanity bound on individual amounts whose comment says explicitly that it is "not the total money supply". (GetBlockSubsidy, amount.h, CMainParams)
This mission makes the consequence a theorem about the pinned implementation: the sum of the subsidies of all blocks, at every height the chain can reach, is strictly below MAX_MONEY, and in fact equals a specific constant once the subsidy reaches zero. It is the arithmetic core of the ledger-supply results that a whole-consensus development will need, and it is small enough to be verified completely.
Amounts are counted in satoshi. One bitcoin is satoshi and . The mainnet halving interval is blocks.
The Core subsidy at height is the transcription of GetBlockSubsidy: with the number of halvings, the subsidy is if , and otherwise , the right shift of the initial subsidy by bits. Heights are nonnegative integers in the source, and the shift acts on the nonnegative value , so natural numbers represent both exactly. The explicit halvings >= 64 branch exists because a shift by 64 or more is undefined in C++.
The declarative schedule is : fifty bitcoin, halved once per interval with the remainder discarded.
Issuance below height is the running sum of Core subsidies, and . The interval sum collects one subsidy per interval. The zero height is .
This is the weakest stable statement: it survives any refinement of the constants below and is what a supply argument downstream consumes. It is BitcoinSubsidy.issuance_bound.
core_eq_spec): for every , including heights where the 64 branch fires.subsidy_le_maxMoney): , so the subsidy is always a valid amount.subsidy_antitone): .subsidy_halving): .subsidy_zero_iff): . The subsidy is one satoshi throughout the thirty-third interval and zero from the thirty-fourth on.issuance_total): satoshi.issuance_le_total): for every .The goal is a kernel-checked statement that the implemented subsidy schedule can never issue MAX_MONEY or more in total, for any chain length, and the milestones pin down the exact figure: bitcoin, satoshi short of twenty-one million because of the floor in each halving. Milestones 1 and 5 record two facts about the implementation worth having on the record: the halvings >= 64 guard is never the reason the subsidy is zero (division already gives zero from 33 halvings), and the subsidy is exactly one satoshi for the 210,000 blocks of the thirty-third interval.
What formalizing adds is separation of the arithmetic from the accounting. The supply bound on an actual ledger needs more than this: fees move value without creating it, unclaimed coinbase value is never issued, and outputs can be made unspendable. Those are statements about the UTXO transition and belong to a separate mission; this one supplies the exact upper bound they will cite.
Status: every statement is open with an intentional placeholder proof. The constants and the shift are checked against the pinned source; nothing about compiled Bitcoin Core is claimed.
The naive proof of the goal is to evaluate the sum: unfold issuedBelow at and compute. The kernel cannot do that in reasonable time, and the statement is for every , not one. The argument has to be structural: within an interval the subsidy is constant, so the sum over the first intervals is ; past the zero height every term vanishes, so the sum is stable; and for below the zero height the sum is bounded by monotonicity. Only the thirty-three-term interval sum is evaluated by computation.
A second trap is the shift. equals only because the value is nonnegative; the schedule theorem is what licenses replacing the bitwise operation with division everywhere else.
Heights, amounts and counts are Nat. coreSubsidy uses Lean's >>> on Nat, which is exact division by . issuedBelow and intervalSum are structurally recursive, so proofs about them are inductions on the height or the interval count. No Mathlib is required; the development imports only Std.
A trivializing formalization would define issuedBelow through specSubsidy and prove the bound about the schedule alone; the definition is fixed on coreSubsidy so that the result is about the transcription. Weakening the goal to a bound at one fixed height is out of scope.
Out of scope: the coinbase check GetValueOut() > blockReward in ConnectBlock, fee accounting, and the UTXO set. Those take this mission's definitions as inputs. Proofs of the milestones in any order are welcome, as are reusable lemmas on issuedBelow.
GetBlockSubsidy, src/validation.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. SourceCOIN, MAX_MONEY, MoneyRange, src/consensus/amount.h, same revision. SourceCMainParams::nSubsidyHalvingInterval, src/kernel/chainparams.cpp, same revision. SourceChainstate::ConnectBlock, src/validation.cpp, same revision. SourceBitcoin's consensus rules are not a single ruleset but a history of them. Each soft fork — P2SH, strict DER signatures (BIP66), CHECKLOCKTIMEVERIFY (BIP65), sequence locks (BIP68/112/113), SegWit with NULLDUMMY (BIP141/147), Taproot — began enforcing at a particular block height, and a node validating the chain from genesis must apply to each block exactly the rules in force at its height. Bitcoin Core implements this with buried deployments: fixed activation heights in CMainParams, consulted by DeploymentActiveAt, and a function GetBlockScriptFlags that assembles the script-verification flags for a block. Two historical blocks are special-cased by hash: one that violated P2SH before the rule was enforced, and one that violated Taproot rules before activation; for these the flag set is replaced. (GetBlockScriptFlags, deploymentstatus.h, CMainParams)
A whole-chain correctness statement needs this table to be exact: which rules apply at which height, and precisely how the two exceptions deviate. This mission transcribes it and proves its structural properties: rules are only ever added as height increases, in a fixed order, and the exceptions only ever remove rules.
A buried deployment is one of HEIGHTINCB (BIP34), CLTV (BIP65), DERSIG (BIP66), CSV, SEGWIT, with mainnet heights , , , , . It is active at a block when the block's height is at least that height, and active after a previous block when the previous height plus one is.
A flag set records which of P2SH, WITNESS, TAPROOT, DERSIG, CHECKLOCKTIMEVERIFY, CHECKSEQUENCEVERIFY, NULLDUMMY are enforced. The base is P2SH | WITNESS | TAPROOT for an ordinary block, NONE for the BIP16 exception block, and P2SH | WITNESS for the Taproot exception block. GetBlockScriptFlags adds DERSIG, CHECKLOCKTIMEVERIFY, CHECKSEQUENCEVERIFY and NULLDUMMY to the base when DERSIG, CLTV, CSV and SEGWIT respectively are active at the block's height. Flag sets are compared by inclusion: every rule enforced by the first is enforced by the second. Separately, ConnectBlock sets LOCKTIME_VERIFY_SEQUENCE for BIP68 exactly when CSV is active.
for ordinary (non-exception) blocks. This is BitcoinActivation.flags_mono: at no height is a script rule enforced that a later height would not enforce. It is the weakest statement that makes "the rules in force at height " a well-ordered notion.
activeAt_mono); after is at of the next height (activeAfter_eq).flags_before_bip66): only the base P2SH | WITNESS | TAPROOT.flags_after_segwit): every flag.flags_order): CHECKLOCKTIMEVERIFY implies DERSIG, CHECKSEQUENCEVERIFY implies CHECKLOCKTIMEVERIFY, NULLDUMMY implies CHECKSEQUENCEVERIFY.bip16_exception): no flags at all at its height (170,060, before BIP66).taproot_exception): every flag except TAPROOT at its height (692,261, after SegWit).exception_le): at any height, an exception's flags are included in the default's.lockTimeFlags_eq): LOCKTIME_VERIFY_SEQUENCE exactly from height .The goal and milestones pin down, as kernel-checked facts, the exact ruleset function of the pinned implementation: which script rules apply at every mainnet height, that the function is monotone and that its four height-dependent rules switch on in a fixed order, and that the two hash-keyed exceptions are the only departures and only ever relax. For the whole-consensus development this is the "historical rule selection" input: a block at height is validated against , and these theorems are what a composition proof cites when it reasons about rules across heights.
Status: all statements are open with intentional placeholder proofs. The exception blocks are identified by their hashes in the source; the model names them and states their flags at any height in the relevant range, so no claim about a specific hash is made.
There is little depth here by design; the point is exactness. The trap is the exceptions: P2SH, WITNESS and TAPROOT are not height-gated at all in the pinned source (they are "always on except for the two violating blocks"), so a formalization that gates them by their historical activation heights would be wrong for the pinned revision. Likewise the height-dependent flags are OR-ed onto the exception's base, so the Taproot exception block does enforce DERSIG, CLTV, CSV and NULLDUMMY.
Heights are Nat; flag sets are a structure of seven Booleans; inclusion is pointwise implication. Versionbits deployments (DEPLOYMENT_TESTDUMMY, the historical Taproot signalling) are not modeled, since the pinned source consults no versionbits state for mainnet consensus flags. The exception table is modeled as a three-valued classification of a block rather than a hash lookup; the hash-to-block correspondence is a serialization matter.
A trivializing formalization would define the flags directly as a monotone function of height, dropping the exceptions; the definition follows the source's base-then-OR structure with the exception table.
No Mathlib is required; the development imports only Std.
GetBlockScriptFlags, src/validation.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48, lines 2249–2288. SourceDeploymentActiveAt, DeploymentActiveAfter, src/deploymentstatus.h; BuriedDeployment, DeploymentHeight, src/consensus/params.h; CMainParams, src/kernel/chainparams.cpp, same revision. SourceLOCKTIME_VERIFY_SEQUENCE, src/consensus/consensus.h, same revision. Source100ba872c808946155b1eeb8c4568058f2eea0a7. CollectionA Bitcoin block header is valid only if its hash, read as a 256-bit number, is at most a target encoded in the header's 32-bit nBits field, and only if that nBits is the one the consensus rules require at that height. Every 2016 blocks the required target is recomputed from the time the previous 2016 blocks took, so that blocks keep arriving roughly every ten minutes. Three pieces of arithmetic carry the whole rule: the lossy compact encoding between a 32-bit word and a 256-bit target (arith_uint256::SetCompact and GetCompact), the retarget computation with its clamped timespan and cap (CalculateNextWorkRequired), and the transition check that a header's claimed difficulty change is within the permitted range (PermittedDifficultyTransition), which Bitcoin Core uses to reject headers cheaply before it has the full chain. (pow.cpp, arith_uint256.cpp, CMainParams)
These functions are short but intricate: the encoding has sign and overflow flags, a mantissa that must be re-normalized when its top bit is set, and a rounding step that discards low bits; the retarget multiplies inside 256 bits where a carry would be lost. A disagreement in any of them splits the network. This mission states what the pinned implementation computes and proves that its own pieces are consistent: the retarget never produces a target the transition check rejects.
A compact word is a 32-bit value with size (the top byte) and mantissa (the low 23 bits; bit 23 is the sign). Its exact value is when and otherwise. SetCompact computes the same quantity but inside a 256-bit register, so its result is for . It also reports negative ( and bit 23 set) and overflow ( and , or and , or and ).
GetCompact encodes a 256-bit value : with the bit length of and , the mantissa is shifted to its top three bytes (shifted left into three bytes when ); if bit 23 of that mantissa is set, the mantissa is divided by 256 and incremented; the word is mantissa . Because only three bytes survive, is rounded down.
Mainnet parameters: , target timespan seconds, spacing seconds, interval blocks; minimum-difficulty blocks, no-retargeting, and BIP94 are all off.
DeriveTarget rejects a word that is negative, zero, overflowing, or above ; proof of work holds when the hash is at most the derived target. CalculateNextWorkRequired takes the last target and the signed elapsed time of the period, clamps it to , computes , caps at , and re-encodes with GetCompact. PermittedDifficultyTransition at a retarget height decodes the claimed new word and requires it to lie between the re-encoded caps of and ; off a retarget height it requires the word to be unchanged. GetNextWorkRequired returns the last word off a retarget height and calls the retarget on one.
The hypothesis on holds for every target DeriveTarget accepts, hence for every block on a valid chain. This is BitcoinPow.nextWork_permitted. It is the weakest stable statement: it says only that the two functions are consistent, without fixing the rounding constants that make them so.
overflow_iff): the overflow flag is set iff .setCompact_eq_spec): if the flag is clear, .checkProofOfWork_iff): acceptance iff the word is non-negative, non-overflowing, positive, at most , and .getCompact_le): for .getCompact_valid): GetCompact never produces a negative or overflowing word.round_mono): .clamp_bounds): the clamped timespan lies in for every signed input.nextWork_le_powLimit): the next target decodes to at most , for every input.nextWork_off_boundary): off a retarget height the required word is the last word, and that transition is permitted.The goal is a kernel-checked consistency property of the pinned implementation: whatever the last target and the two block times, a block carrying the required nBits is never rejected by the cheap header-chain check. Milestones 1–3 give an exact mathematical reading of what nBits means on the wire, including when the implementation refuses it. Milestones 4–6 characterize the lossy re-encoding: it rounds down, keeps the top bit, and is order-preserving, which is the property the transition check silently relies on when it compares re-encoded bounds against a decoded value.
Formalizing adds two things to the C++. It makes the 256-bit wrap-around explicit: the retarget's multiplication is proved not to wrap only under the bound on the previous target, and the overflow flag is proved to be exactly the "does not fit" condition rather than an approximation. And it isolates the rounding as a function of the top-bit position, which is what the monotonicity argument needs and what the source never states.
Status: all statements are open with intentional placeholder proofs. Nothing about compiled Bitcoin Core is claimed; the value-level model of arith_uint256 (a natural number below , shifts and products reduced modulo , exact division) is the documented correspondence.
The naive proof of the goal is to unfold both functions and compare. It fails at the re-encoding: the new word is and the check compares against for the two bounds . These are not and ; they are and with low bits cleared, and how many bits are cleared depends on the bit length of each. The argument needs that the rounding map is monotone across different bit lengths, which holds because the rounded value always retains the top bit — a value with fewer bits is below the top bit of any value with more.
A second trap is the mantissa normalization. When the top three bytes have bit 23 set, GetCompact shifts by a further byte, so the number of discarded bits is not a function of the size byte alone; the case split in the proofs is on the bit position modulo 8.
A third is nActualTimespan, a signed 64-bit difference that can be negative when timestamps go backwards. The clamp is stated on signed integers and the conversion to a natural number happens after it.
arith_uint256 values are Nat below width = 2 ^ 256; <<= and *= reduce modulo width, /= is Nat division, bits() is Nat.log2 + 1 with 0 for zero, and GetLow64 is % 2 ^ 64. The uint32_t assignment in GetCompact is % 2 ^ 32. Compact words are BitVec 32; their fields are read through toNat. Block times are Int; the clamped timespan is converted with Int.toNat after clamping. Hashes enter checkProofOfWork already as natural numbers; the byte-order correspondence of UintToArith256 is a serialization matter outside this mission. fPowAllowMinDifficultyBlocks, fPowNoRetargeting, enforce_BIP94, and the fuzz-determinism shortcut are fixed to their mainnet values and not modeled as parameters.
A trivializing formalization would define permittedTransition by calling calculateNextWork; both are transcribed independently from the source. Assuming the previous target is already a GetCompact output, which would make rounding exact, is also ruled out: the goal assumes only the powLimit bound.
No Mathlib is required; the development imports only Std. Proofs of milestones in any order are welcome, and lemmas on the rounding map are reusable by any later header-validation work.
GetNextWorkRequired, CalculateNextWorkRequired, PermittedDifficultyTransition, DeriveTarget, CheckProofOfWorkImpl, src/pow.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. Sourcearith_uint256::SetCompact, arith_uint256::GetCompact, base_uint::operator<<=, operator*=, operator/=, bits, src/arith_uint256.cpp and .h, same revision. SourceCMainParams proof-of-work parameters, src/kernel/chainparams.cpp, same revision. SourceBitcoin's ledger is a set of unspent transaction outputs: every coin that exists is an output of some transaction that no later transaction has spent. A transaction consumes outputs and creates new ones; the rule that it may not create value — that its outputs total at most its inputs — is what makes the supply finite, and the one exception, the coinbase transaction of each block, may create at most the block subsidy plus the fees the block's other transactions paid. Bitcoin Core enforces this through a handful of functions: CheckTransaction rejects negative or overflowing output values (CVE-2010-5139) and duplicate inputs (CVE-2018-17144); CheckTxInputs requires every input to be an existing, mature coin and computes the fee; UpdateCoins spends the inputs and adds the outputs; ConnectBlock accumulates the fees and rejects a coinbase that pays more than fees plus subsidy, after a BIP30 check that no output of the block already exists as an unspent coin. (tx_check.cpp, tx_verify.cpp, coins.cpp, validation.cpp)
Each of these checks has been the site of a real inflation bug. This mission transcribes them and proves the ledger-level consequence: starting from an empty ledger, after any sequence of accepted blocks the total value of all unspent outputs is at most the sum of the block subsidies.
Amounts are integers in satoshi; MoneyRange is . Transaction ids form an arbitrary type with decidable equality. An outpoint is a pair (txid, index). A coin is an output value together with its creation height, its coinbase flag, and whether its script is unspendable (the only script property the accounting reads: AddCoin never stores an unspendable output). A transaction has a txid, a list of input outpoints, a list of outputs, and a coinbase flag standing for IsCoinBase(). The UTXO set is a list of (outpoint, coin) entries with pairwise distinct outpoints; getCoin looks an outpoint up, spendCoin removes it, addCoin inserts (replacing any entry with the same outpoint, as possible_overwrite permits), and totalValue sums the stored values.
The transcribed rules: checkTransaction (non-empty inputs and outputs, the output-value loop with its running MoneyRange test, no duplicate inputs); checkTxInputs (all inputs present, coinbase inputs mature by COINBASE_MATURITY = 100, each input value and the running nValueIn in range, nValueIn \ge GetValueOut(), fee in range); updateCoins (spend inputs unless coinbase, add outputs); bip30Ok; checkBlockTxs (first transaction coinbase, others not, all passing checkTransaction); connectLoop (per-transaction fee accumulation with the running MoneyRange test, then updateCoins); connectBlock (the above, then GetValueOut(coinbase) \le nFees + subsidy(height)); and connectChain, which connects blocks at consecutive heights. The subsidy is a parameter .
for every subsidy function , starting height , and sequence of blocks whose transactions have pairwise distinct txids within each block. This is BitcoinUtxo.ledger_bound. It is the weakest stable statement: the subsidy schedule is a parameter, so the result survives any change to it, and composing with the subsidy mission's bound gives the twenty-one-million cap as a corollary.
checkTransaction_outputs): an accepted transaction has distinct inputs and every output value in .checkTxInputs_some): CheckTxInputs returns exactly , in range, with every input present.totalValue_spend): removing a present coin lowers the total by exactly its value.totalValue_add_fresh): adding at a fresh outpoint raises the total by the value, or by nothing if unspendable.totalValue_spendInputs): spending distinct, present inputs lowers the total by .tx_conservation): an accepted ordinary transaction with fresh outputs lowers the ledger by at least its fee.coinbase_bound): a coinbase with fresh outputs raises the ledger by at most its output value.block_bound): an accepted block raises the ledger by at most and keeps outpoints distinct.chain_bound): the same, summed over consecutive blocks, from any ledger.The goal is a kernel-checked statement that the transcribed rules, applied from genesis, cannot put more value into the ledger than the subsidy schedule allows, for any transactions whatsoever: fees only move value, unspendable outputs only destroy it, and the coinbase is bounded by fees plus subsidy. The milestones give the exact per-transaction accounting the proof rests on, including the role of each historical fix: the MoneyRange loop (milestone 1), the duplicate-input rejection (milestones 5 and 6 need distinct inputs), and the BIP30 check (milestones 6 to 8 need fresh outputs).
Three hypotheses are the honest boundary of the result. Distinct txids within a block stand for the collision-freedom of transaction hashes, which an abstract id type cannot provide. The BIP30 check is modeled as enforced, which is true at every mainnet height except the two historical duplicate-coinbase blocks. And the genesis coinbase, which Bitcoin Core never connects to the UTXO set, is simply not among the blocks.
Status: every statement is open with an intentional placeholder proof. Nothing about compiled Bitcoin Core is claimed.
The naive argument — "inputs exceed outputs, so value cannot grow" — fails at three places that the actual code guards. Without distinct inputs, a transaction that lists the same outpoint twice would be credited its value twice while the view removes it once (CVE-2018-17144); the accounting lemma for spending needs Nodup. Without the BIP30 check, an output could overwrite an existing unspent coin and silently destroy or replace its value; the lemma for adding a coin needs the outpoint fresh, and freshness must be carried through the block from the initial view, which is where distinct txids enter. And the output values must be known non-negative before any sum is bounded, which is exactly what the MoneyRange loop supplies.
The fee is a second trap: CheckTxInputs computes it with signed arithmetic and tests it separately, so the proof must recover the identity from the loop rather than assume it.
Amounts are Int; heights are Nat, and the maturity test uses truncated subtraction, which rejects a spend below the coin's height as the signed source does. The UTXO set is a keyed list; keysNodup is the map invariant and is proved preserved. Serialization-size, script-length, null-prevout and script-validity rules are not modeled; the coinbase flag is a field. The BIP30 enforcement flag, fEnforceBIP30, is fixed to its post-exception mainnet value.
A trivializing formalization would define connectBlock so that it fails whenever value would grow; every rule is transcribed from its source function. Restricting to blocks with no unspendable outputs or to transactions with a single input is out of scope.
No Mathlib is required; the development imports only Std. The composition with the subsidy mission's BitcoinSubsidy.issuance_bound, giving the absolute cap, is the intended follow-up theorem.
CheckTransaction, src/consensus/tx_check.cpp at revision a773e1e33b349dc819b5a0edc1c7a4839dc73b48. SourceConsensus::CheckTxInputs, src/consensus/tx_verify.cpp, same revision. SourceCCoinsViewCache::AddCoin, SpendCoin, HaveInputs, AddCoins, src/coins.cpp, same revision. SourceUpdateCoins, BIP30 check and fee accounting in Chainstate::ConnectBlock, src/validation.cpp, same revision. SourceErdős Problem 624 (erdosproblems.com/624) is a problem of Erdős and Hajnal about how few elements of a set can be enough to "see" the whole set through a function on its subsets. For a finite set with , let be the least for which some map has the following property: for every with ,
The problem asks to prove that .
The question belongs to extremal set theory. It asks whether the trivial counting bound can be beaten by an unbounded additive amount.
Timeline.
ErdosProblems/624.lean and published here as the definition Erdos624_defs.Much of the supporting development works in a two-map (PAIR) reformulation:
More generally, the -track version allows maps .
stated as Erdos624.erdos_624 exactly as in Formal Conjectures.
For every fixed there is such that for all and all , some -set and colour satisfy for all and all .
The implication "bounded-track resilience Erdős 624" is proved in Lean (erdos_624_of_bounded_track_resilience). Whether the hypothesis is true is open.
For all sufficiently large , every pair has a -set with .
This is the case of the condition above. On its own it does not imply Erdős 624, and it is false at (pair_common_hole_false_k3).
A proof of the goal would settle a 1968 question of Erdős and Hajnal. It would show that the information-theoretic bound is never tight up to bounded error.
The present mission collects machine-checked partial and structural results obtained while attacking the PAIR case:
Status, stated plainly: none of these results proves PAIR, the "Step 17" target of the underlying analysis, or Erdős 624. All of them are partial or structural. Some theorems are pure arithmetic consequences of an unproved packing statement (P), which enters only as a numeric hypothesis. In particular, the rank-rich exclusion () is conditional on (P), and (P) is neither claimed nor formalized here.
Every linked theorem has an accepted, sorry-free Lean proof on this platform using only the standard axioms (propext, Classical.choice, Quot.sound).
Alon's pigeonhole argument gives a missed colour for a single map. For two or more maps the missed sets of different maps can be disjoint: pair_common_hole_false_k3 shows exactly this at , where each map misses half the colours on every 3-set yet no colour is missed by both. The underlying analysis also shows that separately convexified (fractional) relaxations of the fibre constraints admit fractional "covering pairs", so integrality or genuinely joint information across colours must enter any proof. The holes produced on small sets for different colours do not obviously combine, because the union of two holes can contain a new witness.
0df444a).Finset with arbitrary finite types and two maps , or list maps .Mathematics derived from GPT 6.1 Sol's analysis, relayed by Ethan Cheung; hand-checked and Lean formalization by Grok Bot.
FormalConjectures/ErdosProblems/624.lean, https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/624.leanThe Odd Goldbach campaign asks how many prime summands suffice to represent every odd integer greater than one, while tracking bounds supported by formal proofs. This mission supplies the bound 23. Its starting point is the accepted 25-prime formalization, which uses the elementary Schnirelmann–Mann method and explicit sieve estimates. The improvement concerns the constants in that formalized development. It does not assert a new mathematical solution of the three-prime problem.
An explicit bound is useful here because it turns a qualitative additive-basis statement into a theorem with a precise, auditable conclusion. Each improvement must still cover every allowed input, including the smallest odd integers. The campaign statement fixes that common standard, so a smaller displayed value has the same mathematical meaning as the earlier bound.
A prime is a natural number greater than one with no positive divisors other than one and itself. A representation is a finite multiset of primes: order does not matter, and the same prime may occur more than once. Both the sum and the number of summands count multiplicities. In particular, the prime 2 is allowed in the mission's conclusion.
The supporting two-prime counting function counts integers representable as a sum of two odd primes. An integer with several such representations is counted once. For a natural number , write for the number of representable integers in the interval from zero through . The formalization uses the existing shared representation function and tests whether that function is positive; it does not replace the represented set with a more convenient surrogate.
The finite sieve input uses a set of 1000 odd primes, each at most 7927. For a positive difference , its weight is
where the product runs over distinct odd prime divisors. The finite certificate counts each unordered pair of distinct entries once, using the condition .
The goal is
where every member of the multiset is prime. This is exactly the campaign template specialized to 23. There is no unspecified lower threshold and no additional arithmetic hypothesis on .
The supporting finite milestone establishes
The two counting milestones establish
on the respective ranges and . Natural logarithms and real exponentials are used throughout. The boundary at is included in both estimates; no gap between the ranges is intended or permitted.
The mission improves the previously formalized constant from 25 to 23 while retaining the shared mathematical definitions. Its reusable outputs are the explicit finite sieve certificate and the two counting estimates. These can support later work without requiring another author to repeat the finite prime-weight computation or reconstruct the same numerical bounds.
The finite certificate is published with a closed dependency frontier. The medium-range, large-range, and goal records carry their own verification status and dependency graphs. A verified reduction and a theorem with every dependency proved are distinct statuses. Campaign attestation additionally requires review of the mission and the numeric value established by its goal.
The central difficulty is retaining enough quantitative information across the finite sieve input, the two counting ranges, the density comparison, and the small-value transition. An asymptotic estimate alone would leave unboundedly many inputs outside the theorem's scope. A numerical calculation performed outside the proof assistant would also leave the crucial finite certificate unsupported.
Large exact computations pose a separate formalization constraint: a correct proof can exceed the verification service's per-file time limit. The finite computation is therefore organized into genuine mathematical subclaims with independently checked statements. Their combination is a short list-sum argument; a successful helper submission is not substituted for the final endpoint.
The development uses Lean 4.33.1 and the campaign's pinned Mathlib environment. Natural numbers encode inputs and prime summands; real numbers encode logarithms, densities, and analytic inequalities. Finite sets are used for the sieve shifts and counted integers, while the final representation is a multiset. The distinction matters: shift primes are distinct, but final summands may repeat.
The existing Schnirelmann definitions, Mann basis theorem, sieve constants, prime-pair estimate, and two Riesel–Vaughan interval estimates remain shared dependencies. The submitted proofs introduce no new axiom, admitted proof, weakened quantifier, or external computation oracle. Local interface files are only mirrors of platform declarations; complete dependency closure is checked on the platform separately from local compilation.
Further contributions may sharpen these explicit estimates or reuse the finite and counting certificates. The stable objects for such work are their published statements and definitions. Any future lower campaign value must still satisfy the full quantified goal.
Atlas IV certified the Kerr–Newman background as an exact Einstein–Maxwell solution and proved that its linearised operators are the true first variations of the nonlinear residuals. Atlas III proved, for frozen Kerr–Newman radiation systems taken from Hintz (arXiv:2609.33661v1), the local equivalence of systems (1) and (7). Atlas V connects the two: under an explicit phantom gauge and single-mode conditions, IV's linearised equations imply III's systems.
Boyer–Lindquist coordinates , Atlas signature ; parameters with , , ( allowed); exterior and . The Kinnersley frame with , complex-bilinear contractions (no conjugation), NP spin coefficients and Weyl/Faraday scalars are registered local coordinate definitions; Riemann and Weyl come from Atlas II's curvature. A complex tangent is a pair of real first-order tangents of metric, field and frame, each , with antisymmetric , the frame reality pattern ( real, ) and the first-order Gram relation.
Goal (atlasV03_main): if is such a tangent on , IV's linearised residuals of the complexified tangent
vanish, the complex phantom gauge holds on , and the scaled
radiative variables of both branches are single modes (amplitude in ) with real
, then III's positive and negative systems (1) hold on , and (via III) systems (7).
Milestones: the frame/Faraday/mode bridges (V-01), the frame curvature bridge, the background and the sourced NP Bianchi identity (V-02), the kinematic realisation and the Ricci source formula through IV's , and the four per-branch statements (V-03).
The radiation systems of Atlas III are no longer free-standing: each of the eight frozen residuals res1a–d, res1aN–dN is derived in Lean from a linearised Newman–Penrose identity of an actual metric/field/frame perturbation, with sources written through IV's certified operators. Divisions are only by , , , , , , (nonzero on the exterior) and, in res1d/res1dN, by using ; never by , or .
The frame varies with the perturbation; the curvature bridge needs the commutator term; the complex gauge is a condition on the complex combination and may not be split into real parts; sources appear under frame derivatives and must be shown to vanish on an open set; amplitude regularity has to be derived, not assumed.
Lean 4 with Mathlib (0df444a3…), autoImplicit off; smoothness is ContDiffOn ℝ ∞ (, not analytic). Pinned
Mathlib has no Lorentzian Levi-Civita connection, Ricci tensor or Newman–Penrose objects; the coordinate definitions are a
registered local definition layer (B3 policy), reused unchanged from Atlas I–IV and extended in V (registry §K–§M). This is a
forward source derivation under the chosen gauge and single-mode conditions, not a two-way reconstruction; no gauge
reachability, mode completeness, spectrum, stability, global flow or new exact solution is claimed; zero_instance only shows
the hypothesis bundle is non-empty.
This campaign entry establishes the bound 25 for every odd integer greater than 1, with repetitions allowed. It refines xuanji's existing formalized 27-prime Schnirelmann–Mann argument by replacing the two-prime sum count n/25 with 100n/2399. The middle range is covered by 278 exact rational interval certificates; the large-range final comparison has an explicitly positive quartic numerator. The shared definitions and existing sieve inputs are unchanged. The resulting density 1/12 gives 24 odd primes plus 3, with small integers handled explicitly.
This is a numerical refinement of an existing elementary formalization, not a new proof of weak Goldbach. The goal is the campaign template with value 25. Complete source and mathematical explanation are attached to theorem ba75c64f-9452-4582-83b3-77b31da8e4dc; proof submission 2e9b3af7-c5c8-4ec8-bcfa-87ed00efecd0 was ACCEPTED by the server on 2026-10-24 at 11:09:45 UTC, and the theorem is Proved with empty open frontier. The prior campaign record is 27.
Formal verification complete: all 12 mission targets, including Theorem 2, are Proved. These results apply to the formalized independent-box model described below. Paper: Cost-aware Bayesian Optimization via the Pandora's Box Gittins Index, NeurIPS 2024. The formalization follows Theorem 2 and Appendix B.5 of the paper.
An experiment can be valuable without being worth its price. In Bayesian optimization, a function evaluation may require training a model, running a simulation, or carrying out a laboratory experiment. The decision is therefore both where to evaluate and how much information to buy. A rule that responds only to relative costs can miss the effect of making every evaluation expensive.
Xie, Astudillo, Frazier, Scully, and Terenin connect this question to Pandora's box, a sequential search problem with independent hidden rewards. Their paper uses the exact solution of this simpler model to motivate an acquisition function for Bayesian optimization. This mission formalizes the paper's fixed expected-budget result, Theorem 2. Theorem 1, the classical cost-per-sample result attributed to Weitzman, is supporting material. Paper, Sections 2–3.
There are finitely many boxes in a nonempty set . Box contains a real random reward with a known distribution and finite absolute first moment. The rewards are mutually independent. Opening it costs a deterministic amount and reveals its reward exactly.
A policy chooses a first box, then uses its observed history and independent randomization to choose an unopened box or stop. It must open at least one box, cannot reopen a box, and cannot resume after stopping. Its terminal reward is the largest observed reward. There is no outside option of zero. Define
For a fixed real budget , feasibility means . This is an expected-budget constraint; individual runs may exceed . Write
For , the reservation index is the unique finite solution of
At zero multiplier, the formalization defines
A generalized Gittins policy first opens a maximal-index box. It subsequently opens a remaining maximal-index box when its index exceeds the incumbent, and stops when the incumbent exceeds every remaining index. Equality permits either action. Ties between boxes and stopping ties may be randomized. Positive-cost rule, equation (5) and Section 3.2.
Theorem 2 assumes the budget condition
Define the dual envelope
The main target is the existence of minimizing this envelope on and a generalized Gittins policy satisfying
Thus the policy is optimal for the fixed expected budget. Positive multipliers require exact expected expenditure; zero multipliers permit slack.
Why the zero-multiplier case matters. A strictly positive multiplier need not yield a budget-optimal policy. For example, take independent rewards , , unit costs, and . Opening box 2 and then box 1 exactly when achieves within budget, whereas every positive-multiplier index policy has strictly smaller reward. Source statement and proof, Appendix B.5.
Supporting targets include the reservation root; Theorem 1; exact-budget and complementary-slackness certificates; convexity and attainment of the dual minimum; joint expected-cost and expected-reward limits at positive multipliers; budget matching and Gittins cost extrema; a zero-multiplier policy-limit lemma; and a feasible zero-index policy when zero minimizes the dual. Some milestones isolate or strengthen steps used in the proof rather than reproducing a numbered statement verbatim. A supporting corollary gives a sufficient condition for a positive multiplier:
Budgeted Pandora’s box is motivated by a common feature of Bayesian optimization in practice: experiments, simulations, and model evaluations must be chosen within a limited resource budget. It asks how to choose evaluations sequentially to maximize the expected best observed reward, subject here to a bound on expected total cost. An optimal index policy for this problem provides a theoretical benchmark for budget-aware Bayesian optimization.
All 12 linked theorem targets have completed Lean proofs, including the zero-multiplier boundary and the supporting probability, policy-limit, and optimization results. The verified development establishes the paper's expected-budget theorem and supplies reusable components for finite adaptive search and constrained optimization.
The empirical performance of the acquisition function and the extension to correlated Gaussian-process Bayesian optimization are outside the goal. No global Bayes-optimality claim is made for that correlated extension. Paper, Section 3.3.
An optimal penalized policy need not meet a prescribed budget. Atoms and tied indices can make expenditure jump as the multiplier changes. The targets therefore include expected-cost extremes within the index-policy class and randomization that interpolates those costs.
At zero multiplier, finite reservation roots can escape to positive infinity. Arbitrary ties in the resulting extended indices need not respect the budget; the zero-dual-minimum milestone asserts existence of a feasible choice, rather than feasibility of all choices.
The convergence target records both expected reward and expected cost, including the slope needed in the envelope argument. The directional derivative of an affine objective uses its linear part, as stated in Lemma 13. Supporting arguments, Appendices B.5–B.6.
The Lean model uses boxes, integrable Borel probability laws on , their product measure, and an independent uniform seed on . Measurable policies observe ordered padded histories. Finite recursion enforces irreversible stopping and distinct openings. Terminal maxima start at the first observation, not zero.
Expectations are Bochner integrals; their integrability and the boundedness of real policy suprema are established from the model in the verified supporting lemmas. Zero indices use EReal and the infimum of almost-sure upper bounds. Index conditions apply to all valid histories, including histories of probability zero. Negative multipliers are excluded by the generalized-rule definition. The strict-gap predicate is used only for the positivity corollary.
Verification was performed by Prove2Me's server using Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474.
We investigate Gaussian quantum states in view of their exceptional role within the space of all continuous variables states. A general method for deriving extremality results is provided and applied to entanglement measures, secret key distillation and the classical capacity of Bosonic quantum channels. We prove that for every given covariance matrix the distillable secret key rate and the entanglement, if measured appropriately, are minimized by Gaussian states. This result leads to a clearer picture of the validity of frequently made Gaussian approximations. Moreover, it implies that Gaussian encodings are optimal for the transmission of classical information through Bosonic channels, if the capacity is additive.
This mission is the statement-level formalization of Extremality of Gaussian quantum states (arXiv:quant-ph/0509154v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1, (2): general Gaussian extremality (original seed) (Lemma 1, (2): general Gaussian extremality (original seed), 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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
Additivity of the Holevo capacity is proved for product channels, under the condition that one of the channels is in a certain class of unital qubit channels, with the other completely arbitrary. This qubit class includes the depolarizing channel. As a byproduct this proves that the Holevo bound is the ultimate information capacity of such qubit channels (assuming no prior entanglement between sender and receiver). Additivity of minimal entropy and multiplicativity of p-norms are also proved under the same assumptions.
This mission is the statement-level formalization of Additivity for a class of unital qubit channels (arXiv:quant-ph/0103156v2). 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 Unital qubit channels: norm multiplicativity and entropy and Holevo additivity (Theorem 1, equations (5)–(7), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
We study the symmetric-side-channel-assisted private capacity of a quantum channel, for which we provide a single-letter formula. This capacity is additive, convex, and, for degradable channels, equal to the unassisted private capacity. While a channel's (unassisted) capacity for for private classical communication may be strictly larger than its quantum capacity, we will show that these capacities are equal for degradable channels, thus demonstrating the equivalence of privacy and quantum coherence in this context. We use these ideas to find new bounds on the key rate of quantum key distribution protocols with one-way classical post-processing. For the Bennett-Brassard-84 (BB84) protocol, our results demonstrate that collective attacks are strictly stronger than individual attacks.
This mission is the statement-level formalization of The private classical capacity with a symmetric side channel and its application to quantum cryptography (arXiv:0705.3838v1). 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 Theorem 5 (seed paper result): single-letter ss-private capacity (Theorem 5 (seed paper result): single-letter ss-private capacity, 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.
3 results of the paper are not stated yet, because the library lacks an interface they need:
A partition of a nonnegative integer is a way to express it as a sum of positive integers, with the order of the summands ignored. For example, the partitions of 4 are 4, 3+1, 2+2, 2+1+1, and 1+1+1+1. If denotes their number, then and , with the empty partition counted once. Although this definition is elementary, the values of obey identities and divisibility laws that are difficult to see from lists of partitions.
A generating function records a sequence as coefficients of a power series. For partitions it is . Product and series identities give different descriptions of the same coefficients, connecting counting problems with algebra and complex analysis. Hei-Chi Chan's An Invitation to q-Series develops these connections through Jacobi's product identity, the Rogers–Ramanujan identities, and Ramanujan's partition congruences. This collection imports the proved statements in the accompanying Lean development, with Ramanujan's partition identity as its main result.
A formal power series over a ring is a sequence of coefficients written as ; equality means equality of every coefficient. Multiplication uses the finite sum . The symbol is an indeterminate, so a formal identity requires no choice of a numerical value for and no analytic convergence assumption.
Write . This formal product is well defined because, for a fixed degree , factors with do not change its coefficient. Euler's partition identity states that . Substituting for multiplies every exponent by the positive integer ; in particular, .
The analytic results use a complex number in place of the formal variable. Their finite product notation is , and denotes the corresponding infinite product when it converges. Conditions such as , , and the nonvanishing of other parameters are part of the individual statements. The formal and analytic settings remain distinct throughout the collection.
The main theorem identifies the generating function for partition numbers whose indices are 4 modulo 5. In , it asserts the unconditional identity
Since , this is the usual expression . The inverse exists because has constant coefficient 1. The displayed equality concerns the whole infinite series, rather than a fixed number of initial coefficients.
The associated milestones include Euler's pentagonal identity, Jacobi's triple product, the two Rogers–Ramanujan identities, and the partition congruences
for every natural number . Additional milestones record formal identities involving the Rogers–Ramanujan quotient and the parity of Ramanujan's tau coefficients. Each reference retains its own hypotheses and coefficient ring; the collection does not treat identities over different rings as interchangeable.
The partition identity gives an exact generating function for an infinite arithmetic progression of partition numbers. The three congruences likewise apply to all indices in their stated progressions. Their scope is therefore different from the numerical partition and tau values that also appear in the library. Both kinds of result are included, with their ranges stated explicitly.
The source development supplies Lean proofs of these known mathematical results. The imported collection makes their definitions, statements, and supporting lemmas available in one compatible environment for subsequent work on partition identities and Ramanujan notebook formulas. Its reusable components include finite product algebra, coefficient extraction, substitutions in formal series, and the links between analytic products and formal coefficient identities.
Agreement of many initial coefficients cannot establish equality of two arbitrary infinite series. A formalization must account for every coefficient and justify any infinite product or sum used to define it. In an analytic statement, moving between a limit and a sum or product also requires convergence under the stated parameter conditions. These obligations remain present even when the final displayed identity is short.
Division presents a separate issue. A quotient of formal series needs an invertible denominator, while analytic quotients need the relevant complex values to be nonzero. Residue-class extraction introduces another distinction: retaining terms of degree and replacing their exponents by is different from leaving those exponents unchanged. The imported definitions specify the convention used by each theorem.
The main result uses rational formal power series and the ordinary partition-counting function. Supporting statements use integers, commutative coefficient rings, finite residue fields, or complex analysis as required by their types. The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The mathematical source is pinned to revision 5df34b280b6a9c4a68ab09105b4e5d3c7bbe88d1; compatibility adaptations are recorded with the imported items.
This is a collection of the source's proved results, including auxiliary and conditional lemmas. It does not assert that every statement discussed in the book has been formalized. In particular, the continued-fraction convergence discussion, the closed-form special value at , the general core-partition characterization, and the full modularity and multiplicativity theory of the tau function must not be inferred from the narrower entries provided here. A definition of a proposed value is kept distinct from a theorem evaluating a function at that value.
The referenced theorem statements are fixed to the audited import. Further work can reuse these results to formalize additional identities or supply separate, stronger theorems. Conditional reductions remain conditional in their titles and statements, and finite computations retain their explicit bounds.
Hei-Chi Chan, An Invitation to q-Series: From Jacobi's Triple Product Identity to Ramanujan's Most Beautiful Identity, World Scientific, 2011. DOI: 10.1142/8129.
Xiang Huang, Lean formalization of An Invitation to q-Series, source revision 5df34b280b6a9c4a68ab09105b4e5d3c7bbe88d1. Pinned source repository.
Offline reinforcement learning and off-policy evaluation start from a single logged trajectory of a controlled system. The policy that generated the log is often unknown, history-dependent and not stationary. Model-based methods first estimate the transition probabilities of the system from this log, then plan or evaluate policies in the estimated model (Agarwal, Kakade & Yang, 2020; Li et al., 2024). How many samples that estimate needs is the question of Banerjee, Honnappa & Rao.
For an uncontrolled, geometrically ergodic Markov chain on states, Wolfer & Kontorovich (2021) showed that the transition matrix can be learned to accuracy in the -norm from of order samples, where is the smallest stationary probability, and that this rate is minimax. Banerjee, Honnappa and Rao extend this to controlled chains whose controls may depend arbitrarily on the past. Stationarity, irreducibility and aperiodicity then need not hold.
A controlled Markov chain with states and controls consists of:
Both processes are adapted to a filtration , and
The controls are otherwise arbitrary.
From a sample of length , the visit counts are and . The empirical estimator is , and its error is measured by
Three conditions control the chain:
The uniform mixing coefficient compares the conditional law of the window given the whole history up to with its unconditional law. With the paper defines
and , . Here depends on only.
(a) Sample complexity. There are a universal and a positive function such that every controlled Markov chain satisfying Assumptions 1, 2 and 4 has, for and ,
The printed threshold lacks the second and third terms and is false without them: i.i.d. uniform states satisfy all assumptions with , but the printed threshold is then , far below the samples that are needed.
(b) Minimaxity. This is the paper's Appendix G.3 Part 1. For (a universal threshold), and , let be the transition matrix on states whose first rows are and whose last row is perturbed by in consecutive pairs of coordinates (the page takes even; for odd the leftover coordinate is left unperturbed). These chains exist. They satisfy the three assumptions with , and . For and ,
Since on this family, the term of (a) cannot be improved beyond a universal constant.
Clause (a) gives an estimate of all transition matrices from one trajectory logged by an arbitrary adapted policy, with explicit dependence on the return-time constant , the visitation constants and the mixing constant. Error bounds for off-policy evaluation and for recovering optimal values follow from it in the paper's Section 5. Clause (b) shows that no estimator does better than the empirical one by more than a universal factor in the leading term.
Neither clause has a machine-checked proof. Four printed statements on the path are false as stated and are posed here in corrected form, each with a counterexample in its item:
Proposition 3 is posed in the regime where its printed bound holds. A complete formalization would give the first checked minimax result for estimating a controlled Markov chain. It would also give the first checked concentration inequality for visit counts of a non-stationary mixing process.
Under arbitrary adapted controls the visit counts are not sums of independent or stationary terms, and the number of transitions observed from a state is random and correlated with the transitions themselves. Applying a fixed-sample-size concentration bound row by row therefore fails. The deviation of around its mean has to be controlled by a Bernstein-type inequality for non-stationary, geometrically mixing bounded sequences, with constants that depend on the mixing rate alone. The constants must not depend on , or the chain. Such an inequality is not in Mathlib. The lower bound needs Fano's method, or an equivalent, for path laws of Markov chains.
Fin d and controls Fin k, with , and time is from .Filtration ℕ. It carries adapted , , row-stochastic matrices and the conditional transition law.A complete development needs several pieces of infrastructure, all reusable beyond this mission:
Contributions of any of these, and proofs of the milestones, are welcome.
A classification problem specifies when two objects should count as equivalent. Descriptive set theory compares such problems by asking whether an assignment of invariants transforms one equivalence relation into another. Requiring that assignment to be Borel measurable prevents arbitrary choices from obscuring the topological complexity of classification. A universal relation for a class would provide one common target for every classification problem in that class.
This mission asks for a Lean formalization of Theorem 1.1 of Ruijun Wang, There is no universal equivalence relation, arXiv:2610.31052v1. The paper proves a negative answer for equivalence relations whose graphs are countable unions of closed sets. The requested mission category is OpenProblem; the open task is the formalization of this known paper theorem, rather than a claim that the mathematical question remains unanswered.
The historical comparison is with the smaller class of relations whose graphs are countable unions of compact sets. Rosendal proved a universality theorem for that class and asked whether its bounded-difference benchmark also captures all relations. The source introduction and bibliography identify Proposition 19 and Problem 28 of his paper as the relevant result and question. The timeline is: Rosendal's compact-cover universality result and question in 2005; the question's subsequent appearance in the descriptive-set-theory literature cited in Wang's introduction; and Wang's 22 October 2026 preprint giving the stronger nonuniversality theorem targeted here.
A Polish space is a topological space admitting a complete separable metric compatible with its topology. An equivalence relation on a space is reflexive, symmetric, and transitive. Its graph is the subset of consisting of pairs with . A set is when it is a countable union of closed sets. For relations this condition refers to the graph in the product topology.
Given equivalence relations on and on , a reduction is a function satisfying
No injectivity on points is required. A Borel measurable reduction has Borel preimages of open sets. A Baire measurable reduction has preimages of open sets with the Baire property: each such preimage differs from an open set by a meager set. A meager set is a countable union of nowhere dense sets. These conventions follow Sections 2.1–2.3 of the source.
The domain of the main construction is the real Hilbert space of square-summable real sequences, with its norm topology. For a real linear subspace , its coset equivalence relation is
The subspace need not be closed, complete, or Polish in its inherited topology. If is , its coset graph is also because subtraction is continuous.
The main goal is the full existence assertion of Theorem 1.1:
The last clause excludes every Baire measurable reduction, with no auxiliary assumptions on its range or on the constructed subspace.
Two supporting targets accompany the goal. Lemma 2.4 says that a Baire measurable map from a Polish space to a second-countable space is continuous on some comeager subset of its domain. Here means a countable intersection of open sets, and comeager means that the complement is meager. The second target is the final clause of Theorem 1.1: no equivalence relation on a Polish space is universal under Borel reducibility for all equivalence relations on Polish spaces. Their exact declarations share the same definitions as the main target.
The result rules out a single relation as a common Borel classification target for this entire class. Its main clause supplies an obstruction already among coset relations of real linear subspaces of one fixed Hilbert space. Thus the obstruction does not require varying the source among arbitrary Polish spaces or arbitrary kinds of equivalence relations.
The mathematical result is proved in the cited preprint. This draft supplies definitions and open Lean statements. Completing the mission means proving the submitted statements against those definitions using the supported Lean and Mathlib environment. Local compilation checks that the statements are well formed; the present sorry proof bodies do not constitute formal proofs. A completed development would also expose reusable interfaces for descriptive-set-theoretic reductions and coset relations.
An graph has a closed cover, but those closed pieces need not themselves be equivalence relations. In particular, composing two pairs belonging to one piece need not stay in that piece. A proof cannot assume transitivity at each closed approximation merely because the union is transitive. Likewise, the compact-cover universality result does not automatically extend to arbitrary closed covers in noncompact Polish spaces. The source distinguishes these issues explicitly in its treatment of a fixed target.
The target also quantifies over Baire measurable reductions, which can be discontinuous on the ambient space. A proof limited to continuous maps would leave a weaker theorem. The continuity-on-a-comeager-set milestone records the precise regularity available without adding continuity as a hypothesis to the main goal.
The shared namespace is NoUniversalFSigma. Real is Mathlib's lp (fun _ : ℕ => ℝ) 2; linear subspaces are Submodule ℝ RealL2, and equivalence relations are Setoid. The definition of uses a sequence indexed by all natural numbers, including zero. Baire measurability uses Mathlib's Baire-property predicate on open preimages. Borel measurability refers explicitly to the Borel sigma algebra of the given topology, so an arbitrary measurable-space instance cannot change the assertion.
The main theorem permits targets in any universe and includes empty targets. The nonuniversality target quantifies over ordinary Type Polish source and target spaces, sufficient for the usual presentations of Polish classification problems. Its universal quantifier includes itself. Neither target assumes a chosen closed cover, a rank bound, or the desired obstruction. Restricting the source to a finite-dimensional space, requiring the subspace to be closed, or excluding only continuous reductions does not meet the goal.
Contributions may develop the source's intermediate constructions and the necessary category, Hilbert-space, and ordinal machinery, or give another proof of the same statements. The supporting declarations can be reused independently; the acceptance boundary remains the stated quantifiers and conclusions without additional hypotheses.
This problem asks for a formal proof of the complete conditional geometric K24 change-of-slice result, including its regularity obstruction. The source gives informal analytic arguments; this publication does not claim a new proof or a new unsolved conjecture for the standard perturbation lemma. It does not assert existence of the still-missing geometric organizer in the four-dimensional Einstein research program.
Let be a closed smooth real four-manifold with an actual common smooth circle action. Write for its normalized Haar average on the relevant tensor, covector, or vector bundle and . Let the positive metrics and be invariant under that same action; the actual nearby positive metric need not be invariant. The scalar is arbitrary. Define
where , is the symmetrized covariant derivative with factor , and . These are actual geometric differential operators, not freely supplied linear maps.
Fix the numerical data for a uniformly bounded local finite-cover system, metric ellipticity and coefficient bounds, , and a uniform pullback bound for the common action. These bounds are fixed before the conclusion constants are chosen. Covering degree is not globally bounded, and the downstairs overlap count is kept separate from the internal coordinate atlas on each covering manifold. The proposition requires all of the following.
Invariance makes the middle term vanish. On the genuine zero-Haar-mean tensor sector, identify the difference of the fixed-reference and re-anchored derivatives as
The target also includes the actual connection/Bianchi coefficient expansions, principal-symbol identification by a quadratic-jet test and its intrinsic norm bound, sector preservation and equivariance. It requires the displayed variation to be the Fréchet derivative in the specified section norms on a positive-radius metric neighborhood, not just a pointwise or directional derivative.
For every real , with the corresponding fixed local Sobolev coefficient/atlas bounds, require a uniform with
The Sobolev clause is not restricted to integer order and does not impose higher Hölder regularity on the metric. It uses local real-order metric and inverse-metric bounds; it does not impose a fixed global bound on the degree-dependent norm of the whole metric.
Prove the natural estimate by a uniform constant times . For the shifted pair, both metric differences must instead be controlled in . The actual Bianchi–Killing/rough-Laplacian identity is also included.
Geometric inverse transfer. In each stated pair of actual zero-mean section spaces, suppose the re-anchored projected operator is a bounded linear isomorphism with inverse bound (or ). If that bound times the norm of the actual difference operator is strictly below , prove that the fixed-reference operator is an isomorphism with inverse bound at most (respectively ), including surjectivity and the corresponding Banach-dual gap. Mere absence of kernel is not substituted for the initial isomorphism. Norm, completeness, Haar integrability/boundedness and projection facts needed for this argument are requested conclusions about the concrete spaces; they are not assumed copies of the desired theorem.
Actual flat-torus sharpness. On the genuine four-torus with coordinates of period , use the flat metric, the circle translation in , and
Require positivity of for , finite norms, , bounded norms, and a lower bound for the norm of the projected actual vector-operator difference tested on . Consequently no uniform shifted estimate using only the metric difference can hold. This is a statement about genuine torus tensors and operators, not an abstract sequence of scalar exponents.
Norm and formalization choices. The definition packages specify full big Hölder norms from actual iterated derivatives and top-order Hölder seminorms, hierarchical local finite covers, and real-order Bessel–Sobolev norms with explicit partitions. Sobolev carriers use the continuous/C² representatives justified by the requested ranges; their completeness and norm properties remain to be proved. The adapted Sobolev norm is an explicit upstairs sum and is not identified with downstairs independently of covering degree. Haar averaging is pointwise in finite-dimensional fibers, avoiding an unsupported assumption of norm-continuous action on big Hölder space. The projection bounds are and ; and apply only in the isometric case. Raw inverse, derivative and integral definitions are totalized in Lean, while positivity, regularity, integrability and the analytic properties are enforced by the full statement's hypotheses or required conclusions. Definitions have no admissions or new axioms. There is exactly one intentional unproved theorem placeholder.
Remaining application boundary. K24 does not construct the common marked action, the required same-window / closeness, or the adapted re-anchored inverse from an arbitrary Einstein degeneration. Those organizer inputs remain open. The nonlinear diffeomorphism-chart and quadratic-remainder applications in K16/K21 are separate supporting questions; they require their own loss-aware regularity hypotheses/proofs. Neither those applications nor the original Einstein conjecture is claimed proved by this publication.
The 3SUM problem — does an integer array contain three values, at three distinct positions, that sum to zero — is a canonical benchmark of fine-grained complexity. Hundreds of reductions sit beneath it in the 3SUM-hardness lattice, so its worst-case exponent governs the reported complexity of convex-hull degeneracies, motion planning, and many computational-geometry tasks. On the real-RAM side the best known bounds are barely subquadratic; on the integer side, Alman and Vassilevska Williams opened a line of subquadratic deterministic word-RAM exponents built on truly subquadratic triangle detection in lopsided graphs.
A recent development is that the entire algorithmic pipeline — data structure, compiled word-RAM program, and runtime certificate — has been written down in Lean 4 and machine-checked, turning a numerical-exponent claim into a verified theorem. Along the way a refinement ladder formed, each step exported as a theorem EndStatement.ThreeSum.SolvedInTime r against the same benchmark specification:
ThreeSum1960614 tree here);The benchmark model is the source word RAM of the Alman–Vassilevska Williams formalization (EndStatement, already on the platform in TrulySubcubicAPSP_SourceSpecification): a deterministic machine over signed words of width with arithmetic, memory, and conditional-jump instructions. One says SolvedInTime r when for every magnitude exponent there is a single finite program , a width bound , and a time function with for some — the rational-power encoding of — such that , run at every width , decides 3SUM on every instance of integers of absolute value at most within steps. Instances are functions Fin n → Int; yes requires the three summands at three distinct indices.
i.e. deterministic 3SUM in word-RAM steps. The constant is hard-coded: this mission certifies this exact exponent, the sharpest point of the current chain.
The proof is the ternary-radix refinement of the construction: the same color-coding data structure reorganized around base-3 digits, banks, and queries, compiled to an explicit machine program, with the runtime charged combinatorially stage by stage. The milestone list follows the costing chain of the source: radix-3 machinery and the ternary data structure, the principal-cost certificate (, the bank term ), the finite-block certificate (), the frontend budget (), the executed colored solver (), and the exported benchmark target ().
The result is, at the time of writing, the best formalized deterministic 3SUM exponent available anywhere: previous formalized entries on this platform bottom out at . Once proved end to end here it becomes the platform's record value for this benchmark, and every lemma of the ternary layer becomes reusable platform infrastructure — falsifiable, importable, and improvable by others, since a cheaper stage immediately yields a better SolvedInTime value by the same costing bridge.
Formalizing it also stress-tests something beyond the number: an end-to-end compiled program execution with a certified asymptotic runtime, not just an abstract algorithm. The runtime margins are certified against strict gaps ( at the largest scale), so the verification is quantitative, not just qualitative.
The difficulty is not one deep lemma but a long, load-bearing chain: thousands of small Meets-specifications about program fragments, the radix-3 generalization of the binary machinery, entropy and logarithm interval arithmetic for the exponent, and the assembly of a single compiled program whose correctness and runtime must both hold simultaneously. A tempting shortcut is to postulate the data-structure spec and prove only the runtime analysis — but the benchmark statement is about one concrete word-RAM program, so nothing may be assumed about the implementation: the compiler, the machine semantics, and the runtime ledger are all part of the statement's content.
This mission is a transplant of an existing, checked Lean 4 development (Apache-2.0) pinned to this platform's default environment (Lean 4.33.1, Mathlib 0df444a…). Statements keep the source's model and names; the benchmark Problem/SolvedInTime layer is reused from the platform's existing TrulySubcubicAPSP_SourceSpecification and the preceding 3SUM trees, and only the new ternary layer is added. No sorry, no assumed oracle, no weakening of SolvedInTime to a per-instance or per-width reading is admissible.
This project gives a completed Lean 4/mathlib formalization of the main theorem of A uniform bound of five for Diophantine tuples in imaginary quadratic integer rings by Zrinka Franušić and Tomislav Pejković.
A Diophantine tuple, or -tuple, in a commutative ring with identity is a finite set of nonzero elements such that is a square in the ring whenever and are distinct elements of the set. The theorem gives a uniform upper bound of five for such tuples in the full rings of integers of all imaginary quadratic number fields.
Let be an imaginary quadratic number field, that is, an extension of of degree two that admits no embedding into . Let denote its full ring of integers, consisting of the elements of that are integral over .
A finite set is a -tuple if
The value is allowed, with . Requiring the square roots to lie in instead of gives the same notion, since is integrally closed in .
For every imaginary quadratic number field and every -tuple in ,
Equivalently, contains no -tuple with six elements.
Adžaga established a uniform bound of . Cipu and Fujita established bounds of in 2024 and in 2026. Whether a -tuple with five elements exists in the ring of integers of any imaginary quadratic field remains an open question (Dujella, Problem 1.11).
The theorem concerns the full ring of integers in every case. In particular, for a positive squarefree integer , it applies to , whose ring of integers strictly contains . No further hypotheses are imposed on the entries.
The formalization is complete. The main theorem has status Proved on Prove2Me. The formalization was completed on 24 October 2026. The Lean source repository contains the full source code and instructions for reproducing the verification.
The theorem card displays the formal statement with a by sorry placeholder; the accepted proof is stored separately and can be followed through its dependency graph.
The Lean 4 development D1Bound5 uses mathlib's full ring of integers 𝓞 K. Its main declaration is D1Bound5.main_statement, whose type is D1Bound5.MainStatement.
The proposition D1Bound5.MainStatement quantifies over types K with instances Field K, NumberField K and NumberField.IsTotallyComplex K, subject to Module.finrank ℚ K = 2, and over finite sets A : Finset (𝓞 K). It asserts A.card ≤ 5 whenever D1Bound5.IsD1 A holds. The definition D1Bound5.IsD1 requires every member to be nonzero and, for distinct members x and y, a witness r in the same ring satisfying r * r = x * y + 1.
Zrinka Franušić and Tomislav Pejković, A uniform bound of five for Diophantine tuples in imaginary quadratic integer rings, preprint, 15 October 2026.
Fault-tolerant quantum computers implement Clifford gates cheaply and the non-Clifford T gate expensively, because T gates are obtained by magic-state distillation (Fowler, Stephens and Groszkowski). Single-qubit rotations by small, arbitrary angles appear throughout quantum simulation and must be compiled into Clifford+T circuits, so the T-count of a small rotation is a standard cost measure. Selinger's ancilla-free method uses about T gates for a -rotation by (arXiv:1212.6253), and the paper's own search puts optimal ancilla-free Clifford+T synthesis near (Sec. VI).
Wiebe and Kliuchnikov (arXiv:1305.5528) proposed non-deterministic circuits with ancillas and measurement, the gearbox circuit and its recursive composed gearbox circuit, which, like the linear-combination-of-unitaries circuits of Childs and Wiebe, turn a coarse rotation into a much finer one and whose failures are undone by a Clifford gate, so they can be repeated until they succeed. The cost of such a repeat-until-success scheme is a random variable. Theorem 2 of the paper computes its mean exactly and bounds its variance; this mission formalizes that result together with the circuit identities it rests on.
A qubit has basis ; a gate is a unitary with entry . Let and .
Gearbox circuit . Prepare ancillas in and a target in . Apply to the ancillas, then a -controlled on the target (active when every ancilla is ), then , and measure the ancillas in the computational basis. Outcome is success.
Composed gearbox circuit (Definition 1). is , and : the gate fed to the outer gearbox is the rotation the inner composed circuit enacts on success. Write for the angle with and, for ,
Cost. Level of is attempted until its measurement succeeds; the number of attempts is geometric on . Each attempt at level needs one successful copy of and one of its inverse. With the number of applications of before succeeds, Appendix A's equation (A1) reads
with distributed as and everything independent. Each uses one and one , so the number of applications of or is .
For every unitary and ,
and, for ,
Both clauses are stated as printed; the mean is exact for every .
The theorem shows that the composed gearbox reaches a rotation angle of order , doubly exponentially small in , while using applications of in expectation, with a variance of the same squared order. Since levels give angle , the gate cost scales like with a constant that depends on only through ; this is the basis of the paper's floating-point synthesis scheme, which combines a mantissa rotation with an exponent rotation produced this way (Sections IV–V).
The result has a complete written proof in Appendix A. As far as is known it has no machine-checked proof. The formalization adds three things: the circuit identities of Theorem 1 and Corollary 1 as exact matrix statements, including the boundary case ; the identification of the circuit's Born-rule success probabilities with the closed forms ; and the random-sum identities (A3), (A6) in a form where infinite moments cannot be hidden.
The computational parts are elementary but long. The real difficulty is that the theorem joins two models: a quantum circuit, whose success probabilities come from matrix entries of a post-selected block, and a nested random sum whose summands are themselves random sums. A naive approach postulates the success probabilities and proves a lemma about compound geometric sums. That approach proves nothing about the circuit: the content linking the two is milestone 3, which needs Theorem 1 at every level of the recursion and Corollary 1 to identify the gate fed to level . On the probabilistic side, the variance identity for a random number of independent summands requires finiteness of all second moments, and the bound requires unfolding a recursion whose coefficients vary with the level, which is where the monotonicity of enters.
States are vectors Fin 2 → ℂ; gates are Matrix (Fin 2) (Fin 2) ℂ, unitarity is membership in Matrix.unitaryGroup, and are indices 0, 1. The ancillas are Fin d → Fin 2, and the joint space is (Fin d → Fin 2) × Fin 2 with ancillas first; the controlled gate fires on the all-ones string. The rotation is the matrix , so is the rotation by . Because Lean's Real.tan returns at , the angles and are defined to be when the cosine vanishes, the paper's value ; the case is not excluded. is the recursively defined success unitary: the outcome- block of the one-ancilla gearbox fed with , normalized by the norm of its first column.
The number of applications of or used to enact is modelled by Appendix A's recursion (A1): Theorem 2 speaks of "a given attempt", but its proof defines as the count until succeeds, and that is the quantity formalized. Laws are Mathlib PMF ℕ with independence built into bind; the geometric law is Mathlib's geometricMeasure shifted to ; means and variances are ℝ≥0∞-valued sums.
Three trivializing formalizations are ruled out. The law of uses the circuit's Born-rule success probabilities, never supplied as an input, so Theorem 1 and Corollary 1 are needed for the goal. Moments are in , so a divergent variance is , never the junk value that would make the bound trivially true. The angle convention above excludes the false reading in Theorem 1 and Corollary 1.
Everything needed is in Mathlib: matrices, unitaryGroup, Real.arctan, PMF.bind/PMF.map, geometricMeasure. Reusable beyond this mission: the moments of the shifted geometric law and the mean and variance identities for a sum of a random number of i.i.d. summands, in ℝ≥0∞ form. Contributions to any milestone are welcome; the probabilistic milestones (3–6) do not depend on the circuit milestones except through part 1 of milestone 3.
Quantum information carried by continuous variables, such as the quadratures and of an optical mode, is cheap to manipulate with beam splitters, squeezers and homodyne detectors, but these Gaussian tools cannot protect Gaussian states against Gaussian noise: Niset, Fiurášek and Cerf proved in 2008 that no Gaussian error-correcting code can do better than direct transmission against Gaussian channels (arXiv:0811.3128). Peter van Loock's note (arXiv:0811.3616) shows that this no-go does not cover non-Gaussian noise: a stochastic error that displaces a mode by a fixed amount with probability turns a Gaussian state into a discrete mixture, and against it a purely Gaussian three-mode repetition code (offline squeezing, two beam splitters, homodyne detection, feedforward) reduces the error probability from to .
The example is the continuous-variable analogue of the three-qubit bit-flip code. Unlike that code, it identifies double errors as well as single ones, so it improves on direct transmission without the qubit code's requirement .
A single optical mode is described by its Wigner function , a real function on phase space ; three modes by a function of and . Units are those in which the vacuum has variance .
An error pattern is a set of erring channels. After decoding it shifts the signal by and the ancillas to a syndrome point . The paper's feedforward for pattern is a linear function of that undoes the signal shift at .
For every measurable that equals on the Euclidean disc of radius around , for each pattern :
and this limit exceeds the exact direct-transmission fidelity if and only if .
The paper asserts the comparison "for any " against , an approximation valid for . With the exact direct fidelity the claim fails for small and large (, : against ), so the goal poses the comparison in its exact, corrected form. It holds for every and, for each , once is large enough.
The displays the derivation passes through, in order: the encoded state (6); the eight-term expansion (7) under three independent channels; the decoded state (8); the syndrome table, which shows that only "no error" and "error in every channel" share a syndrome; the homodyne marginal with feedforward (9); and the delta-function limit of the squeezed-ancilla marginals as .
The result. The code reduces the error probability of a stochastic displacement channel from to using only Gaussian operations, which shows that the Gaussian no-go theorem depends on the noise being Gaussian. The syndrome table also shows that a continuous-variable code has more distinguishable error subspaces than its qubit analogue: double errors are identified and corrected.
Formalizing it. The paper's derivation is a chain of displayed formulas with no stated decision regions and no fidelity formula. A formal version fixes what the feedforward is allowed to know (only the measured ), turns "the Gaussians become delta functions" into a limit theorem, and replaces the comparison with by an exact criterion. To our knowledge none of these statements has been machine-checked.
Eqs. (6)–(9) are Gaussian algebra and Gaussian integrals: tedious but mechanical. The difficulty is the limit. The feedforward is one function of , not a different correction for each error pattern as Eq. (9) is printed, and it is pinned down only near the seven distinct syndrome points. Passing to needs the squeezed marginals to concentrate on those points while the integrand, which involves the arbitrary measurable elsewhere, stays controlled. The fidelity limit then needs a second exchange of limit and integral over phase space.
(Fin 3 → ℝ) → (Fin 3 → ℝ) → ℝ, with the paper's mode at Lean index . Units: vacuum variance .Minimizing a convex Lipschitz function over the unit ball of to accuracy takes first-order queries when is small compared with , and cutting-plane methods such as the center-of-mass method attain this rate (Nemirovski–Yudin 1983). They do so by storing their whole cutting history, about bits. Gradient descent stores one vector, bits, but needs queries. Woodworth and Srebro asked at COLT 2019 whether a method with bits can keep the near-optimal query count (Woodworth–Srebro 2019).
Timeline.
An -bit memory-constrained deterministic algorithm (Definition 3) has a query map , an update map and a stopping rule. Starting from , at iteration it queries , receives and stores . Here is convex and -Lipschitz, and is any subgradient selection: for all . The algorithm stops at some iteration ; its output is .
It solves convex optimization to accuracy with queries if on every pair it stops at some with for every . In Lean these are MemAlg d M, IsCOInstance f g, memAt and SolvesCO alg Q ε.
The proof introduces further objects: a sign matrix with ; the uniform law (sphereLaw) and its restriction to slabs (slabLaw); a partition of the sphere into equal-measure cells with representatives (SphereDisc); the parameters , , and of Eq. (3); the Orthogonal Vector Game with Hints (Game 2, Player, winProb); and the adaptive hard functions built by Procedure 1 (procRun).
For every there are , and such that for every and every -bit algorithm with that solves convex optimization to accuracy with queries,
The constants depend on , and none of them is fixed numerically.
The result. Cutting-plane methods are Pareto-optimal for deterministic algorithms up to logarithmic factors: between and bits, any saving in memory costs queries polynomially. Proposition 14 is a memory-sample trade-off for a game with adaptive side information, reusable for other learning problems with hints. The paper also proves a feasibility-problem version (Theorem 2) by the same method.
Formalizing it. The theorem is proved on paper but has no machine-checked proof. A formalization has to make several steps exact that the paper leaves informal: finite-precision hints, the joint law of adaptively sampled slabs, the information-theoretic chain rule of Proposition 14, and the case analysis of Procedure 1. Several statements needed small repairs to be true as written (see below), so writing them precisely is part of the work.
The obvious route is to let the hard function hide its structure in the kernel of and argue that each query reveals little about it. It breaks on information leakage. The vectors built in earlier periods depend on the algorithm's queries, which depend on . So the subgradients returned later can carry information about that the -bit memory never had to store, and a lower bound that ignores this leakage cannot reflect the memory constraint. The central difficulty is to bound this leakage by bits while the adaptively built function stays convex and indistinguishable, for the algorithm, from a fixed function queried through an ordinary first-order oracle (Proposition 8).
Conventions committed to:
EuclideanSpace ℝ (Fin d).Fin M → Bool, and stopping is a map on memory, read after each update.Hints are represented by their cells, so every probability of Game 2 and Procedure 1 is a finite sum. Disclosed repairs:
The reduction step carries the hypotheses and , which the paper's proof uses silently.
SolvesCO is not vacuous. An algorithm without memory cannot satisfy it at accuracy below (proved in a sanity file), while a subgradient method with rounded iterates and an iteration counter can satisfy it with bits. A formalization in which the output is not the query at the stopping time, or in which stopping may happen at time , would make the goal trivial; the definitions rule this out.
Needed infrastructure: the uniform sphere law and its conditioning on slabs; Beta-type laws of projections of uniform vectors; equal-measure partitions of the sphere; entropy and mutual information on finite spaces; singular values of rectangular matrices (Lemma 22). The sphere and information-theoretic lemmas are reusable beyond this mission. Proofs of any milestone are welcome, and so are proofs of the cited Lemmas 5 and 12.
Not formalized: Theorem 2 and the feasibility procedure (§4), and Remark 4.