Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Formalize sample-path stability for a continuous-time, unit-rate, infinite-buffer single-server queue. Starting from cumulative arriving service work, define the reflected transient workload, the workload constructed from the infinite past, long-run offered load, and two-time stationarity. Prove that subcritical load forces finite-time coupling and consequently that every finite initial workload converges in its two-time finite-dimensional distributions to the stationary workload law.
Formalize sample-path Little's Law for deterministic continuous-time queueing trajectories, decomposed into area, sojourn, arrival-rate, boundary, and squeeze lemmas.
First raised for two variables by Ludwig Kraus in 1884 and stated in full generality by Ott-Heinrich Keller in 1939, the Jacobian conjecture asks something that sounds almost like freshman calculus: if a polynomial map from complex n-space to itself has a Jacobian determinant equal to a nonzero constant, must it be invertible by another polynomial map? That constant-Jacobian condition is precisely the algebraic shadow of the inverse function theorem, yet producing a polynomial — not merely analytic — inverse has resisted every attack for over eighty years. Shreeram Abhyankar championed the problem because it can be stated 'using little beyond a knowledge of calculus,' and Stephen Smale placed it sixteenth on his 1998 list of problems for the new century. Its notoriety is sharpened by a graveyard of published 'proofs' that later collapsed. Deep reductions exist — Bass, Connell, and Wright showed in 1982 that the general case reduces to maps of degree three — and the problem is equivalent, through work of Tsuchimoto, Belov-Kanel, and Kontsevich, to the Dixmier conjecture on the Weyl algebra. A formal statement anchors this famously slippery problem so that progress can be verified rather than merely believed.
This mission formalizes K. Juschenko and N. Monod, Cantor systems, piecewise translations and simple amenable groups, Ann. of Math. (2) 178 (2013) 775–787, doi:10.4007/annals.2013.178.2.7. Page numbers are those of the journal.
The topological full group of a Cantor system is the group of homeomorphisms of given piecewise by powers of , on open pieces. Matui showed that for minimal its commutator subgroup is simple, and finitely generated exactly when is a minimal subshift. Grigorchuk and Medynets conjectured that is amenable. Juschenko and Monod proved the conjecture (Theorem A). Together with Matui's results this gave the first examples of infinite, finitely generated, simple, amenable groups (Corollary B); in the paper's words, “Until now, no example of a finitely generated simple group that is amenable (and infinite) was known.”
JuschenkoMonod, which reuses (IntervalExchange.wobbling ℤ), the topological full group (CantorSystems.topologicalFullGroup), amenability (Garrido.IsAmenable) and local finiteness (Chou.IsLocallyFinite) from published bundles.Theorem A (p. 776): the topological full group of any minimal Cantor system is amenable.
Theorem A is the first amenability proof for a class of groups that contains finitely generated infinite simple groups. Its method, a family of almost invariant densities on the Bernoulli space, became the starting point of extensive amenability (Juschenko, Matte Bon, Monod and de la Salle), which also yields amenability of interval exchange groups of low rank. The milestones also state the cited results that Corollary B combines with Theorem A: Matui's simplicity theorem and finite generation criterion, and Matui's uncountable family of pairwise non-isomorphic examples.
The analytic core (§2) is elementary but delicate: Theorem 2.1 shows that the densities are almost invariant under each piecewise translation, through a signed series controlled by Abel summation. §3 converts this into Theorem C, an invariant mean on finite subsets of concentrated on the sets containing , by Fourier analysis on and the Reiter criterion. §4 embeds into and shows the relevant stabilisers are locally finite, by the ubiquitous pattern property. The amenability of is then assembled from two general facts: an action with an invariant mean and amenable stabilisers forces amenability of the group (Lemma 3.2), and for a subgroup of it suffices that the stabilisers of the sets are amenable (Proposition 3.3). The external results on topological full groups (Matui, Giordano–Putnam–Skau, Elek–Monod) are substantial papers of their own; the Elek–Monod example shows that the one-dimensional structure is essential, since Theorem A fails for minimal -systems.
The definitions follow the paper closely, with a few encodings worth knowing. is the type of functions X → Fin 2 with the product of uniform measures. The lamplighter acts on finite subsets by . Means are finitely additive probability measures on all subsets, as in the bundle Garrido_Amenability. The net of almost invariant vectors in Lemma 3.1 is stated with finite sets of group elements and tolerances . Where a reading was needed — the range of in §2, how the constants of Lemma 2.6 depend on , the size of Matui's family — the milestone's Formalization note says which was taken.
Every numbered result is a milestone, with the unnumbered steps the proofs use: the inequality (2.ii), the remark after Theorem C, the finiteness of , and the homomorphism . The cited results stated as external milestones are Matui's simplicity theorem, finite generation criterion and uncountable family, the Giordano–Putnam–Skau classification, and the Elek–Monod -system. Left out: Schreier's remark on free subgroups of and the Grigorchuk–Medynets local embeddability theorem (motivation only), the local finiteness of forward-orbit stabilisers via Putnam's AF-algebras (context for Lemma 4.1, which the paper reproves), and Matui's theorem that the groups are never finitely presented.
The selfish-mining mission took the stationary distribution of Eyal and Sirer's equation (7) as a definition and proved it is invariant with total mass 1. That leaves a gap a careful reader will point out: the revenue analysis is only meaningful if the chain has no other stationary distribution. This mission closes it: every nonnegative, lead-summable, mass-one function that is invariant under one step of the chain is the paper's distribution.
stationary_isStationary): the paper's distribution satisfies the predicate.balance_zero_of, balance_tie_of, balance_one_of, balance_two_of, balance_lead_of): the five balance identities follow from invariance alone, for every and .geometric_of_isStationary): on the lead states every stationary distribution is geometric with ratio ; the recurrence's constant mode is excluded by summability.stationary_unique, the goal): every stationary distribution equals stationary α state by state.The hypotheses are essential: for the chain is not positive recurrent and no such distribution exists. Nonnegativity of is in the predicate for faithfulness to the notion of a distribution but is not needed by the proof. No limit theorem is proved: that the chain converges to this distribution from any start, or that time averages of the revenue process converge to the stationary rates, remains outside the formalization. (arXiv:1311.0243)
The HTLC mission proved which witnesses spend a received HTLC output under the script interpreter, and that its timeout path runs through OP_CHECKLOCKTIMEVERIFY <cltv_expiry>. That is a statement about one script evaluation. The claim Lightning actually needs is one block higher: no block can contain a non-revocation spend of a received HTLC by the timeout path before the expiry height. This mission composes the script result with the block mission's finality rule (IsFinalTx, required by ContextualCheckBlock for every transaction in a block) to state exactly that, and the same bound for a pre-signed HTLC-timeout transaction whose lock time is the expiry.
isFinalTx_height): with a nonzero lock time below the threshold and an input that is not SEQUENCE_FINAL, a transaction is final at height iff its lock time is below .presigned_timeout_height): lock time cltv_expiry means acceptance only in a block above the expiry.received_spend_height, the goal): a two-element witness accepted by VerifyScript for a received HTLC output, in a transaction final at height , is a revocation spend or has cltv_expiry < h.The composition uses only published theorems: received_p2wsh_spend, cltv_concrete, checkLockTime_iff (HTLC mission) and the block mission's isFinalTx. It does not say that a transaction final at a height is in a block at that height, which is the block mission's ContextualCheckBlock characterization, nor anything about the offered HTLC's timeout path beyond the pre-signed transaction's own lock time (there the bound rests on the remote node signing only a transaction with that lock time, a key-level fact outside the script). Time-based expiries (lock times at or above the threshold) are excluded by hypothesis; BOLT #3 uses heights. (BOLT #3, tx_verify.cpp)
A Lightning channel's funds sit in the funding transaction's output, a pay-to-witness-script-hash of the 2-of-2 script 2 <pubkey1> <pubkey2> 2 OP_CHECKMULTISIG. Everything else in the protocol (commitment transactions, penalties, HTLCs) rests on one fact about this output: it moves only with both parties' signatures. This mission proves that fact against the script interpreter as transcribed from Bitcoin Core, and completes the on-chain script set of a channel begun by the to_local, HTLC and anchor missions.
funding_witness): the 2-of-2 loop's verdict, with the NULLDUMMY condition on the dummy element.funding_spends_iff): the witness-v0 success condition holds iff the stack is exactly [sig2, sig1, dummy] with each signature valid for its key in order; no other shape succeeds.VerifyScript (parseScript_funding, funding_p2wsh_spend, the goal): the byte form parses as intended, and VerifyScript accepts a witness for the P2WSH output exactly when it is dummy sig1 sig2 with both signatures valid for the spending transaction's own checker.The signature checks are the signature mission's checker with the witness-v0 sighash; which transaction the signatures commit to (a commitment transaction, a mutual close) is a matter of what was signed, outside the script. BOLT #3's lexicographic ordering of the two keys is not a script-level condition and is not stated. (BOLT #3, interpreter.cpp)
Modern Lightning channels use option_anchors: the remote balance and both HTLC kinds carry a one-block OP_CHECKSEQUENCEVERIFY so that a commitment transaction's outputs cannot be spent in the same block it confirms in, and each side gets an anchor output that it can spend at any time to bump the fee, and that anyone can sweep after 16 blocks so that anchors do not litter the UTXO set. This mission proves what those scripts enforce, against the script interpreter as transcribed from Bitcoin Core, completing the BOLT #3 commitment-transaction script set begun by the to_local and HTLC missions.
to_remote_eval, to_remote_spends_iff, parseScript_toRemote, to_remote_p2wsh_spend): spendable by the remote key, only after the one-block delay, and by nothing else.anchor_eval, anchor_holder, anchor_anyone, anchor_spends_iff, parseScript_anchor, anchor_p2wsh_spend, anchor_anyone_concrete, anchor_anyone_delay): the funding-key holder spends at any time; a clean-false signature (the empty signature) spends exactly after the 16-block delay; under the concrete checker, the empty-signature witness verifies iff the spending transaction is version 2 or later with nSequence ≥ 16. A signature the checker rejects outright fails the script.spends_iff, the two parse theorems, the two p2wsh_spend): the HTLC mission's three paths each, with the one-block delay added to every non-revocation path and the revocation path unchanged.The signature checks stay at the level of the signature mission's checker; the 20-byte hashes are parameters. anchor_anyone_concrete holds under consensus flags: under the policy flag WITNESS_PUBKEYTYPE an uncompressed funding key would make the empty-signature path fail, which is not modelled. With the CHECKSEQUENCEVERIFY flag off (pre-BIP112 blocks) the anchor is spendable by anyone at once; the activation mission fixes the flag on for every current height. The HTLC-success and HTLC-timeout second-stage transactions pay to the to_local script, already covered. (BOLT #3, interpreter.cpp)
A Lightning commitment transaction carries one output per in-flight payment: an offered HTLC (the local node pays if the remote reveals the preimage, or recovers the funds after the timeout) or a received HTLC (the local node claims with the preimage before expiry, else the remote takes the funds back). BOLT #3 gives each a witness script with three branches (revocation, preimage, timeout), and the channel's security rests on those three being the only ways to spend. The to_local mission proved this for the balance output; this mission proves it for both HTLC scripts, against the script interpreter as transcribed from Bitcoin Core.
cltv_step, multisig_two): OP_CHECKLOCKTIMEVERIFY passes exactly under CltvPasses; a 2-of-2 OP_CHECKMULTISIG passes iff each signature verifies for its key in order.offered_revocation, offered_preimage, offered_timeout, received_revocation, received_success, received_timeout): on the BOLT #3 witness shapes the interpreter leaves exactly the expected check, including the NULLDUMMY condition on the multisig dummy.offered_spends_iff, received_spends_iff): over an arbitrary stack, the witness-v0 success condition holds iff one of the three paths' conditions holds. Two facts the interpreter forces that the BOLT text leaves implicit: the inner selector is "is the top element 32 bytes long", not "is it empty"; and every non-revocation path requires the top element not to hash to the revocation hash, because OP_DUP OP_HASH160 … OP_EQUAL hashes whatever is on top.VerifyScript (parseScript_offered, parseScript_received, offered_p2wsh_spend, received_p2wsh_spend, the goal): the byte forms parse as intended, and the pay-to-witness-script-hash outputs are spent exactly by the three paths, with the spending transaction's own signature checker and lock-time check.cltv_concrete, checkLockTime_iff): with the CLTV flag active the check is Core's CheckLockTime, which for a block-height expiry is "nLockTime is a height at least the expiry and the input is not final".The two 20-byte hashes are parameters, not tied to any key or preimage; signature checks stay at the level of the signature mission's checker. The HTLC-success and HTLC-timeout transactions themselves (second-stage, with their own to_local-style scripts) and the anchor-output variants of the scripts are not modelled, nor is the protocol-level argument about who holds which key when. (BOLT #3, interpreter.cpp)
A Lightning commitment transaction pays the local node's balance to a to_local output whose witness script (BOLT #3) reads
OP_IF <revocationpubkey> OP_ELSE <to_self_delay> OP_CHECKSEQUENCEVERIFY OP_DROP <local_delayedpubkey> OP_ENDIF OP_CHECKSIG
The channel's security rests on two claims about this script: the counterparty can spend it at any time with the revocation key, and the local node can spend it with its delayed key only after to_self_delay blocks, and nobody can spend it any other way. This mission proves both, and the "no other way", against the script interpreter as the script, signature and verification missions transcribed it from Bitcoin Core.
eval_cons, csv_step, serialize_length): the script on any stack b :: tl of admissible size fails unless tl is a single element, and otherwise leaves the result of the selected signature check; the OP_CHECKSEQUENCEVERIFY step passes exactly under CsvPasses.spends_iff): for any stack whatsoever, the witness-v0 success condition (one element left, and true) holds iff the stack is [b, sig] and either b is true and sig verifies for the revocation key, or b is false, the sequence check passes, and sig verifies for the delayed key.parseScript_toLocal, p2wsh_spend, the goal): the byte form of the script parses as intended, and VerifyScript accepts a witness for the pay-to-witness-script-hash output exactly when the witness is [sig, b, script] and the selected branch's conditions hold for the spending transaction's own signature checker and sequence check.csv_concrete, checkSequence_iff, lightning_delay): with the CHECKSEQUENCEVERIFY flag active, the sequence check is Core's CheckSequence, which for a 16-bit delay and a flag-free nSequence (as Lightning sets it) is exactly "version ≥ 2 and nSequence ≥ to_self_delay".The signature checks are the signature mission's checkSigPreTapscript with the witness-v0 sighash; nothing here says who holds the keys or how they are derived (BOLT #3's key derivation and the revocation secret are outside the script). The P2WSH program must be a true value, which VerifyScript requires of every witness program and which is a fact about one SHA-256 output the model cannot evaluate symbolically. MINIMALIF is policy, so under consensus any true selector opens the revocation branch; the relative lock time itself (whether the spending transaction may enter a block) is the block mission's BIP68 check, not the script's. (BOLT #3, interpreter.cpp)
"Bitcoin is secure as long as honest miners hold the majority of the hashrate" is the informal reading of Garay, Kiayias and Leonardos's backbone analysis: in a synchronous network, if the adversary finds fewer blocks than there are uniquely successful honest rounds over every long enough window, then honest chains grow (chain growth), agree on all but their last blocks (common prefix), and contain honest blocks regularly (chain quality). This mission states the synchronous model and proves these three properties from that combinatorial hypothesis.
maxvalid adoption, and valid chains in which every block sits on exactly the chain its creator extended (the hash-chain abstraction).chain_growth, chain_growth_self): between rounds and every honest chain grows by at least the number of successful rounds in between.uniquely_successful_height, common_prefix_private, common_prefix_rounds, common_prefix, the goal): a uniquely successful round pins the honest block at its height; a private fork that stays adversarial for a window loses; hence the chains of any two honest parties agree once the last blocks are dropped.chain_quality): any consecutive blocks of an honest chain contain an honest block.chainWork_const_bits): at constant difficulty the block mission's chainWork is the block count times one block's proof, so "longest" and "most work" coincide in this regime.Nothing probabilistic is proved: Typical (adversarial blocks in every window of length strictly fewer than the uniquely successful rounds strictly inside it) is assumed, where the paper derives it from Chernoff bounds and honest majority. The constants are and rather than the paper's ; only the weak form of chain quality is proved. The model is synchronous with one honest block per party per round, no explicit message layer, and static difficulty. (ePrint 2014/765)
Philippe Flajolet and Robert Sedgewick's Analytic Combinatorics is the standard reference for counting discrete structures exactly and asymptotically. Its methods are used throughout the analysis of algorithms, random structures and enumerative combinatorics. This mission collects formally verified versions of the book's chapter-level results in one connected development.
A combinatorial class is a set of objects with a size such that each size has finitely many objects. Its generating function records how many objects have each size: the ordinary generating function for unlabelled classes and the exponential generating function for labelled ones. The symbolic method translates constructions on classes (disjoint union, product, sequence, set, cycle, pointing) into equations between generating functions. For example, if a class has counting series and no size-zero objects, the series for ordered sequences of its objects satisfies
Lagrange inversion recovers the coefficients of implicitly defined series. Singularity analysis and the saddle-point method turn the analytic behaviour of a generating function into asymptotic estimates for its coefficients, and the same machinery gives limit laws for parameters of random structures.
The goal is the ordered-sequence identity above for a class with finitely many objects of each size and none of size zero, stated for formal power series over . The sequence class includes the empty sequence of size zero.
The 132 milestones are the remaining results, listed in the order of the book's chapters. Counts per chapter, goal included:
| Book chapter | Topic | Results |
|---|---|---|
| I | Ordinary generating functions, the symbolic method, Pólya enumeration, Lagrange inversion | 21 |
| II | Exponential generating functions, labelled structures, random mappings | 15 |
| III | Bivariate generating functions, moments and variance of parameters | 7 |
| IV and VI | Complex analysis, coefficient transfer and singularity analysis | 10 |
| V | Rational and meromorphic functions, continued fractions | 8 |
| VII | Applications of singularity analysis to trees and lattice-path classes | 16 |
| VIII | Saddle-point estimates and integer-partition asymptotics | 50 |
| IX | Limit laws for parameters of random structures | 6 |
The total is 133 results.
The results are classical; the book proves them. This mission adds machine-checked proofs: every listed result has a Lean 4 proof accepted on the platform against a fixed Mathlib revision. Formalizing them pins down hypotheses that informal statements leave implicit: which objects a series counts, which convergence and nonvanishing conditions an estimate needs, and which limits are taken.
Informal treatments identify a generating function with "the" counting sequence of a construction; a formal statement must fix the finite type of objects being counted and the exact construction, so the symbolic-method results here are stated against explicit finite object types. Analytic estimates cannot be read off formal series: they need the analyticity domain, the behaviour near the dominant singularity and explicit error terms. Several saddle-point estimates require uniform local and tail bounds that informal arguments state only loosely; where the source assumes such bounds, the statements here keep them as hypotheses.
Formal power-series identities are stated coefficientwise and do not require analytic convergence. Analytic estimates and probability limits keep their convergence, nonvanishing, parameter and measurability conditions. Results that the source proves under explicit assumptions remain conditional on those assumptions. Some results import supporting lemmas that are proved as separate theorems of the mission.
The mission covers 133 chapter-level results of the source development. It does not claim that every theorem of the book is formalized; coverage is exactly the verified declarations in the mission. Further results, sharper variants and alternative proofs are welcome as additional theorems.
Atlases I–IV certified four-dimensional vacuum and Einstein–Maxwell metrics on a registered coordinate definition layer. Atlas VI extends the certificate notion to total dimension and asks two concrete questions: inside one explicit static ansatz, exactly when is the five-dimensional Einstein–Maxwell certificate satisfied; and for the cohomogeneity-one equal-spin ansatz, is the full system of field equations equivalent to a finite set of radial equations.
Total dimension , signature , , coupling with . VI-01: , , , on for all real . VI-02: , , , , radial data on an open with (ESData).
A machine-checked reduction of a five-dimensional Einstein–Maxwell system to seven radial equations, with explicit domains and hypotheses, usable as a certificate checker for equal-spin candidates; the VI-01 criterion derives the charge normalisation.
All curvature data are explicit closed forms generated as CAS hints and re-proved in Lean component by component (Christoffel, derivative, Ricci and Einstein–Maxwell tables); the reduction needs frame reconstruction lemmas for every residual component.
A transaction's identifier is the hash of its serialization without witnesses, and that serialization still contains every scriptSig. Before SegWit, anyone could take a valid transaction, re-encode a signature inside a scriptSig (a different DER length byte, a negated S value, an extra push), and broadcast a transaction that was equally valid and had a different txid. Any protocol that referred to an unconfirmed transaction by its txid — a refund signed against a funding transaction, which is how payment channels start — could be broken this way. BIP141 fixed it by moving signatures into the witness, which the txid does not hash, and by requiring the scriptSig of a native witness spend to be empty.
This mission proves that the fix does what it claims, against the published VerifyScript and CheckInputScripts: for a transaction whose inputs spend native witness programs and whose scripts verify, the txid is a function of the sender's intent — version, prevouts, sequence numbers, outputs, lock time — and of nothing else.
native_scriptSig_empty — under CheckInputScripts with WITNESS, every input spending a native witness program has an empty scriptSig (SCRIPT_ERR_WITNESS_MALLEATED, lifted from the VerifyScript mission's native_witness_malleated).txid_of_intent — for such a transaction, txid tx = txid (ofIntent (intentOf tx)): the identifier of the canonical transaction with empty scriptSigs and witnesses.txid_determined (goal) — two transactions with the same intent, both verifying against the same ledger, with native witness-program inputs, have the same txid.p2sh_wrapped_scriptSig — for a P2SH output spent with witness data, VerifyScript succeeds only if the scriptSig is exactly the single push of the witness program it evaluates to (SCRIPT_ERR_WITNESS_MALLEATED_P2SH); the scriptSig of a wrapped spend is determined by the redeem script.The serialization mission's txid_strip (the txid ignores witnesses), the VerifyScript mission's native_witness_malleated, and the block mission's CheckInputScripts. The statements are about the executable VerifyScript; no assumption about hash functions or signatures is needed, because the theorems say nothing about whether a valid spend exists, only that its identifier is fixed once it does. (interpreter.cpp, transaction.h, BIP141)
"There will only ever be 21 million bitcoin" is the most repeated statement about the system, and it is usually justified by the subsidy schedule alone: fifty coins, halved every 210,000 blocks, summing to just under 21 million. The schedule is proved in the subsidy mission (BitcoinSubsidy.issuance_total). But the schedule is a bound on what a coinbase may create; whether the chain's spendable supply stays within it depends on the whole validation path — that every non-coinbase transaction spends at least what it creates, that no input is spent twice, that the coinbase is bounded by the subsidy plus the fees actually collected, and that these checks run against the right ledger at every step. The inflation bug CVE-2018-17144 was a failure of exactly this composition, not of the schedule.
This mission states the bound as a property of every chain state reachable from the genesis under the block mission's validate, and proves it.
With totalValue u the sum of the values of the coins of a ledger and issued n the subsidy GetBlockSubsidy has issued to a chain of n blocks:
update_bound — UpdateCoins raises the total by at most the value created and lowers it by the value spent (ledger arithmetic on a distinct-key ledger).values_in_range — every coin of a reachable state has a value in [0, MAX_MONEY], because coins only enter as outputs that passed CheckTransaction.block_supply — one accepted block raises the total by at most GetBlockSubsidy(height): the coinbase bound of ConnectBlock against the fees, through the acceptance theorem and ApplySpec of the block mission.supply_bound (goal) — on every reachable state, totalValue S.utxo + genesisSubsidy ≤ issued S.nextHeight.supply_lt_maxMoney — hence totalValue S.utxo < MAX_MONEY on every reachable state.The genesis subsidy appears on the left because the source never adds the genesis coinbase to the UTXO set (ConnectBlock's genesis shortcut), so it is issued but unspendable; the inequality is exact at the genesis state.
The block mission's acceptance (the executable validation accepts iff the declarative specification holds), apply_spec (the resulting state is ApplySpec), reachable_wellFormed (distinct ledger keys), and the subsidy mission's core_eq_spec and issuance_bound. Nothing about the rules is re-transcribed here; the mission adds the quantities and the induction. (validation.cpp, tx_verify.cpp, coins.cpp)
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. SourceThe 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.