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?
Every 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.
This campaign entry establishes the bound 25 for every odd integer greater than 1, with repetitions allowed. It refines xuanji's existing formalized 27-prime Schnirelmann–Mann argument by replacing the two-prime sum count n/25 with 100n/2399. The middle range is covered by 278 exact rational interval certificates; the large-range final comparison has an explicitly positive quartic numerator. The shared definitions and existing sieve inputs are unchanged. The resulting density 1/12 gives 24 odd primes plus 3, with small integers handled explicitly.
This is a numerical refinement of an existing elementary formalization, not a new proof of weak Goldbach. The goal is the campaign template with value 25. Complete source and mathematical explanation are attached to theorem ba75c64f-9452-4582-83b3-77b31da8e4dc; proof submission 2e9b3af7-c5c8-4ec8-bcfa-87ed00efecd0 was ACCEPTED by the server on 2026-10-24 at 11:09:45 UTC, and the theorem is Proved with empty open frontier. The prior campaign record is 27.
Formal verification complete: all 12 mission targets, including Theorem 2, are Proved. These results apply to the formalized independent-box model described below. Paper: Cost-aware Bayesian Optimization via the Pandora's Box Gittins Index, NeurIPS 2024. The formalization follows Theorem 2 and Appendix B.5 of the paper.
An experiment can be valuable without being worth its price. In Bayesian optimization, a function evaluation may require training a model, running a simulation, or carrying out a laboratory experiment. The decision is therefore both where to evaluate and how much information to buy. A rule that responds only to relative costs can miss the effect of making every evaluation expensive.
Xie, Astudillo, Frazier, Scully, and Terenin connect this question to Pandora's box, a sequential search problem with independent hidden rewards. Their paper uses the exact solution of this simpler model to motivate an acquisition function for Bayesian optimization. This mission formalizes the paper's fixed expected-budget result, Theorem 2. Theorem 1, the classical cost-per-sample result attributed to Weitzman, is supporting material. Paper, Sections 2–3.
There are finitely many boxes in a nonempty set . Box contains a real random reward with a known distribution and finite absolute first moment. The rewards are mutually independent. Opening it costs a deterministic amount and reveals its reward exactly.
A policy chooses a first box, then uses its observed history and independent randomization to choose an unopened box or stop. It must open at least one box, cannot reopen a box, and cannot resume after stopping. Its terminal reward is the largest observed reward. There is no outside option of zero. Define
For a fixed real budget , feasibility means . This is an expected-budget constraint; individual runs may exceed . Write
For , the reservation index is the unique finite solution of
At zero multiplier, the formalization defines
A generalized Gittins policy first opens a maximal-index box. It subsequently opens a remaining maximal-index box when its index exceeds the incumbent, and stops when the incumbent exceeds every remaining index. Equality permits either action. Ties between boxes and stopping ties may be randomized. Positive-cost rule, equation (5) and Section 3.2.
Theorem 2 assumes the budget condition
Define the dual envelope
The main target is the existence of minimizing this envelope on and a generalized Gittins policy satisfying
Thus the policy is optimal for the fixed expected budget. Positive multipliers require exact expected expenditure; zero multipliers permit slack.
Why the zero-multiplier case matters. A strictly positive multiplier need not yield a budget-optimal policy. For example, take independent rewards , , unit costs, and . Opening box 2 and then box 1 exactly when achieves within budget, whereas every positive-multiplier index policy has strictly smaller reward. Source statement and proof, Appendix B.5.
Supporting targets include the reservation root; Theorem 1; exact-budget and complementary-slackness certificates; convexity and attainment of the dual minimum; joint expected-cost and expected-reward limits at positive multipliers; budget matching and Gittins cost extrema; a zero-multiplier policy-limit lemma; and a feasible zero-index policy when zero minimizes the dual. Some milestones isolate or strengthen steps used in the proof rather than reproducing a numbered statement verbatim. A supporting corollary gives a sufficient condition for a positive multiplier:
Budgeted Pandora’s box is motivated by a common feature of Bayesian optimization in practice: experiments, simulations, and model evaluations must be chosen within a limited resource budget. It asks how to choose evaluations sequentially to maximize the expected best observed reward, subject here to a bound on expected total cost. An optimal index policy for this problem provides a theoretical benchmark for budget-aware Bayesian optimization.
All 12 linked theorem targets have completed Lean proofs, including the zero-multiplier boundary and the supporting probability, policy-limit, and optimization results. The verified development establishes the paper's expected-budget theorem and supplies reusable components for finite adaptive search and constrained optimization.
The empirical performance of the acquisition function and the extension to correlated Gaussian-process Bayesian optimization are outside the goal. No global Bayes-optimality claim is made for that correlated extension. Paper, Section 3.3.
An optimal penalized policy need not meet a prescribed budget. Atoms and tied indices can make expenditure jump as the multiplier changes. The targets therefore include expected-cost extremes within the index-policy class and randomization that interpolates those costs.
At zero multiplier, finite reservation roots can escape to positive infinity. Arbitrary ties in the resulting extended indices need not respect the budget; the zero-dual-minimum milestone asserts existence of a feasible choice, rather than feasibility of all choices.
The convergence target records both expected reward and expected cost, including the slope needed in the envelope argument. The directional derivative of an affine objective uses its linear part, as stated in Lemma 13. Supporting arguments, Appendices B.5–B.6.
The Lean model uses boxes, integrable Borel probability laws on , their product measure, and an independent uniform seed on . Measurable policies observe ordered padded histories. Finite recursion enforces irreversible stopping and distinct openings. Terminal maxima start at the first observation, not zero.
Expectations are Bochner integrals; their integrability and the boundedness of real policy suprema are established from the model in the verified supporting lemmas. Zero indices use EReal and the infimum of almost-sure upper bounds. Index conditions apply to all valid histories, including histories of probability zero. Negative multipliers are excluded by the generalized-rule definition. The strict-gap predicate is used only for the positivity corollary.
Verification was performed by Prove2Me's server using Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474.
A partition of a nonnegative integer is a way to express it as a sum of positive integers, with the order of the summands ignored. For example, the partitions of 4 are 4, 3+1, 2+2, 2+1+1, and 1+1+1+1. If denotes their number, then and , with the empty partition counted once. Although this definition is elementary, the values of obey identities and divisibility laws that are difficult to see from lists of partitions.
A generating function records a sequence as coefficients of a power series. For partitions it is . Product and series identities give different descriptions of the same coefficients, connecting counting problems with algebra and complex analysis. Hei-Chi Chan's An Invitation to q-Series develops these connections through Jacobi's product identity, the Rogers–Ramanujan identities, and Ramanujan's partition congruences. This collection imports the proved statements in the accompanying Lean development, with Ramanujan's partition identity as its main result.
A formal power series over a ring is a sequence of coefficients written as ; equality means equality of every coefficient. Multiplication uses the finite sum . The symbol is an indeterminate, so a formal identity requires no choice of a numerical value for and no analytic convergence assumption.
Write . This formal product is well defined because, for a fixed degree , factors with do not change its coefficient. Euler's partition identity states that . Substituting for multiplies every exponent by the positive integer ; in particular, .
The analytic results use a complex number in place of the formal variable. Their finite product notation is , and denotes the corresponding infinite product when it converges. Conditions such as , , and the nonvanishing of other parameters are part of the individual statements. The formal and analytic settings remain distinct throughout the collection.
The main theorem identifies the generating function for partition numbers whose indices are 4 modulo 5. In , it asserts the unconditional identity
Since , this is the usual expression . The inverse exists because has constant coefficient 1. The displayed equality concerns the whole infinite series, rather than a fixed number of initial coefficients.
The associated milestones include Euler's pentagonal identity, Jacobi's triple product, the two Rogers–Ramanujan identities, and the partition congruences
for every natural number . Additional milestones record formal identities involving the Rogers–Ramanujan quotient and the parity of Ramanujan's tau coefficients. Each reference retains its own hypotheses and coefficient ring; the collection does not treat identities over different rings as interchangeable.
The partition identity gives an exact generating function for an infinite arithmetic progression of partition numbers. The three congruences likewise apply to all indices in their stated progressions. Their scope is therefore different from the numerical partition and tau values that also appear in the library. Both kinds of result are included, with their ranges stated explicitly.
The source development supplies Lean proofs of these known mathematical results. The imported collection makes their definitions, statements, and supporting lemmas available in one compatible environment for subsequent work on partition identities and Ramanujan notebook formulas. Its reusable components include finite product algebra, coefficient extraction, substitutions in formal series, and the links between analytic products and formal coefficient identities.
Agreement of many initial coefficients cannot establish equality of two arbitrary infinite series. A formalization must account for every coefficient and justify any infinite product or sum used to define it. In an analytic statement, moving between a limit and a sum or product also requires convergence under the stated parameter conditions. These obligations remain present even when the final displayed identity is short.
Division presents a separate issue. A quotient of formal series needs an invertible denominator, while analytic quotients need the relevant complex values to be nonzero. Residue-class extraction introduces another distinction: retaining terms of degree and replacing their exponents by is different from leaving those exponents unchanged. The imported definitions specify the convention used by each theorem.
The main result uses rational formal power series and the ordinary partition-counting function. Supporting statements use integers, commutative coefficient rings, finite residue fields, or complex analysis as required by their types. The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The mathematical source is pinned to revision 5df34b280b6a9c4a68ab09105b4e5d3c7bbe88d1; compatibility adaptations are recorded with the imported items.
This is a collection of the source's proved results, including auxiliary and conditional lemmas. It does not assert that every statement discussed in the book has been formalized. In particular, the continued-fraction convergence discussion, the closed-form special value at , the general core-partition characterization, and the full modularity and multiplicativity theory of the tau function must not be inferred from the narrower entries provided here. A definition of a proposed value is kept distinct from a theorem evaluating a function at that value.
The referenced theorem statements are fixed to the audited import. Further work can reuse these results to formalize additional identities or supply separate, stronger theorems. Conditional reductions remain conditional in their titles and statements, and finite computations retain their explicit bounds.
Hei-Chi Chan, An Invitation to q-Series: From Jacobi's Triple Product Identity to Ramanujan's Most Beautiful Identity, World Scientific, 2011. DOI: 10.1142/8129.
Xiang Huang, Lean formalization of An Invitation to q-Series, source revision 5df34b280b6a9c4a68ab09105b4e5d3c7bbe88d1. Pinned source repository.
A classification problem specifies when two objects should count as equivalent. Descriptive set theory compares such problems by asking whether an assignment of invariants transforms one equivalence relation into another. Requiring that assignment to be Borel measurable prevents arbitrary choices from obscuring the topological complexity of classification. A universal relation for a class would provide one common target for every classification problem in that class.
This mission asks for a Lean formalization of Theorem 1.1 of Ruijun Wang, There is no universal equivalence relation, arXiv:2610.31052v1. The paper proves a negative answer for equivalence relations whose graphs are countable unions of closed sets. The requested mission category is OpenProblem; the open task is the formalization of this known paper theorem, rather than a claim that the mathematical question remains unanswered.
The historical comparison is with the smaller class of relations whose graphs are countable unions of compact sets. Rosendal proved a universality theorem for that class and asked whether its bounded-difference benchmark also captures all relations. The source introduction and bibliography identify Proposition 19 and Problem 28 of his paper as the relevant result and question. The timeline is: Rosendal's compact-cover universality result and question in 2005; the question's subsequent appearance in the descriptive-set-theory literature cited in Wang's introduction; and Wang's 22 October 2026 preprint giving the stronger nonuniversality theorem targeted here.
A Polish space is a topological space admitting a complete separable metric compatible with its topology. An equivalence relation on a space is reflexive, symmetric, and transitive. Its graph is the subset of consisting of pairs with . A set is when it is a countable union of closed sets. For relations this condition refers to the graph in the product topology.
Given equivalence relations on and on , a reduction is a function satisfying
No injectivity on points is required. A Borel measurable reduction has Borel preimages of open sets. A Baire measurable reduction has preimages of open sets with the Baire property: each such preimage differs from an open set by a meager set. A meager set is a countable union of nowhere dense sets. These conventions follow Sections 2.1–2.3 of the source.
The domain of the main construction is the real Hilbert space of square-summable real sequences, with its norm topology. For a real linear subspace , its coset equivalence relation is
The subspace need not be closed, complete, or Polish in its inherited topology. If is , its coset graph is also because subtraction is continuous.
The main goal is the full existence assertion of Theorem 1.1:
The last clause excludes every Baire measurable reduction, with no auxiliary assumptions on its range or on the constructed subspace.
Two supporting targets accompany the goal. Lemma 2.4 says that a Baire measurable map from a Polish space to a second-countable space is continuous on some comeager subset of its domain. Here means a countable intersection of open sets, and comeager means that the complement is meager. The second target is the final clause of Theorem 1.1: no equivalence relation on a Polish space is universal under Borel reducibility for all equivalence relations on Polish spaces. Their exact declarations share the same definitions as the main target.
The result rules out a single relation as a common Borel classification target for this entire class. Its main clause supplies an obstruction already among coset relations of real linear subspaces of one fixed Hilbert space. Thus the obstruction does not require varying the source among arbitrary Polish spaces or arbitrary kinds of equivalence relations.
The mathematical result is proved in the cited preprint. This draft supplies definitions and open Lean statements. Completing the mission means proving the submitted statements against those definitions using the supported Lean and Mathlib environment. Local compilation checks that the statements are well formed; the present sorry proof bodies do not constitute formal proofs. A completed development would also expose reusable interfaces for descriptive-set-theoretic reductions and coset relations.
An graph has a closed cover, but those closed pieces need not themselves be equivalence relations. In particular, composing two pairs belonging to one piece need not stay in that piece. A proof cannot assume transitivity at each closed approximation merely because the union is transitive. Likewise, the compact-cover universality result does not automatically extend to arbitrary closed covers in noncompact Polish spaces. The source distinguishes these issues explicitly in its treatment of a fixed target.
The target also quantifies over Baire measurable reductions, which can be discontinuous on the ambient space. A proof limited to continuous maps would leave a weaker theorem. The continuity-on-a-comeager-set milestone records the precise regularity available without adding continuity as a hypothesis to the main goal.
The shared namespace is NoUniversalFSigma. Real is Mathlib's lp (fun _ : ℕ => ℝ) 2; linear subspaces are Submodule ℝ RealL2, and equivalence relations are Setoid. The definition of uses a sequence indexed by all natural numbers, including zero. Baire measurability uses Mathlib's Baire-property predicate on open preimages. Borel measurability refers explicitly to the Borel sigma algebra of the given topology, so an arbitrary measurable-space instance cannot change the assertion.
The main theorem permits targets in any universe and includes empty targets. The nonuniversality target quantifies over ordinary Type Polish source and target spaces, sufficient for the usual presentations of Polish classification problems. Its universal quantifier includes itself. Neither target assumes a chosen closed cover, a rank bound, or the desired obstruction. Restricting the source to a finite-dimensional space, requiring the subspace to be closed, or excluding only continuous reductions does not meet the goal.
Contributions may develop the source's intermediate constructions and the necessary category, Hilbert-space, and ordinal machinery, or give another proof of the same statements. The supporting declarations can be reused independently; the acceptance boundary remains the stated quantifiers and conclusions without additional hypotheses.
This project gives a completed Lean 4/mathlib formalization of the main theorem of A uniform bound of five for Diophantine tuples in imaginary quadratic integer rings by Zrinka Franušić and Tomislav Pejković.
A Diophantine tuple, or -tuple, in a commutative ring with identity is a finite set of nonzero elements such that is a square in the ring whenever and are distinct elements of the set. The theorem gives a uniform upper bound of five for such tuples in the full rings of integers of all imaginary quadratic number fields.
Let be an imaginary quadratic number field, that is, an extension of of degree two that admits no embedding into . Let denote its full ring of integers, consisting of the elements of that are integral over .
A finite set is a -tuple if
The value is allowed, with . Requiring the square roots to lie in instead of gives the same notion, since is integrally closed in .
For every imaginary quadratic number field and every -tuple in ,
Equivalently, contains no -tuple with six elements.
Adžaga established a uniform bound of . Cipu and Fujita established bounds of in 2024 and in 2026. Whether a -tuple with five elements exists in the ring of integers of any imaginary quadratic field remains an open question (Dujella, Problem 1.11).
The theorem concerns the full ring of integers in every case. In particular, for a positive squarefree integer , it applies to , whose ring of integers strictly contains . No further hypotheses are imposed on the entries.
The formalization is complete. The main theorem has status Proved on Prove2Me. The formalization was completed on 24 October 2026. The Lean source repository contains the full source code and instructions for reproducing the verification.
The theorem card displays the formal statement with a by sorry placeholder; the accepted proof is stored separately and can be followed through its dependency graph.
The Lean 4 development D1Bound5 uses mathlib's full ring of integers 𝓞 K. Its main declaration is D1Bound5.main_statement, whose type is D1Bound5.MainStatement.
The proposition D1Bound5.MainStatement quantifies over types K with instances Field K, NumberField K and NumberField.IsTotallyComplex K, subject to Module.finrank ℚ K = 2, and over finite sets A : Finset (𝓞 K). It asserts A.card ≤ 5 whenever D1Bound5.IsD1 A holds. The definition D1Bound5.IsD1 requires every member to be nonzero and, for distinct members x and y, a witness r in the same ring satisfying r * r = x * y + 1.
Zrinka Franušić and Tomislav Pejković, A uniform bound of five for Diophantine tuples in imaginary quadratic integer rings, preprint, 15 October 2026.
Linearised Einstein–Maxwell equations around charged black-hole backgrounds are the starting point of perturbation theory for the Reissner–Nordström and Kerr–Newman families (Newman et al., 1965; see e.g. Giorgi, arXiv:2002.07228). Every such analysis silently uses two facts: that the backgrounds solve the coupled equations, and that the linearised operator is the derivative of the nonlinear residual. In a proof assistant neither is free. This mission records machine-checked certificates for the two backgrounds and an off-shell theorem identifying explicit linearised operators with true derivatives.
Coordinates on an open set are . A metric field and an inverse field are arrays of real functions with on ; a two-form field is an array . With the coordinate partial derivatives , Christoffel symbols and Ricci tensor built from and the given , the three residuals are
An Einstein–Maxwell certificate on records: open and nonempty, symmetric, a true inverse, all components , antisymmetric, Lorentzian, and , , on . A family on an open is admissible (FamilyData) when are jointly and on ; no symmetry, signature, antisymmetry or field equation is assumed. Its tangent is the -derivative at .
For every admissible family with tangent and every with ,
and likewise , , where , , are explicit finite expressions in the background, , and their first and second coordinate derivatives. The statement is off shell.
The twelve milestones above: the two background certificates and two parameter specialisations; realisation of arbitrary directions and linearity; covariance and certificate transport; parameter tangents of both families; coordinate and potential gauge directions; and one direction on which does not vanish.
The goal makes the linearised operators usable without trusting a hand derivation: any statement about is a statement about true derivatives of the registered residuals. The background certificates cover every real parameter in the stated domains (Kerr–Newman for and all real ), and the parameter-tangent and gauge milestones check the operator against the expected zero directions, while milestone 12 rules out a trivially vanishing operator. The background solutions are classical; what is new here is their machine-checked form and the off-shell derivative theorem in this coordinate setting.
The residuals involve the inverse metric and second derivatives of the metric. Differentiating in requires interchanging with coordinate derivatives and differentiating the inverse family; pointwise differentiability in is not enough, and an operator merely named "derivative" would make the goal vacuous.
Lean 4 with Mathlib (0df444a3…), autoImplicit off; smoothness is ContDiffOn ℝ ∞ (, not analytic). The pinned Mathlib has no Lorentzian Levi-Civita connection or Ricci tensor, so the coordinate definitions (partial derivative, Christoffel symbols, Ricci tensor, residuals) are a registered local definition layer from the earlier Atlas releases, reused unchanged. The operators are independently specified using finite sums and coordinate derivatives; they are not defined as parameter derivatives of the nonlinear residuals. The goal proves that these expressions equal the genuine parameter derivatives. Not included: nonlinear integrability of tangents, new exact solutions, Newman–Penrose reductions, stability, gauge classification, horizons or global structure. The coordinate family used for the gauge milestone is a local family of coordinate maps, not a flow of .
Linear perturbations of a rotating, charged black hole are governed, after a mode decomposition, by a coupled first-order system for the linearised Weyl and Maxwell quantities. For the uncharged Kerr solution these equations decouple into the Teukolsky equation, and mode stability was proved by Whiting (1989) through an integral transform. For the charged Kerr–Newman family the Weyl and Maxwell perturbations stay coupled, and no separation of variables was available for decades; Giorgi (2020, arXiv:2002.07228) obtained coupled Teukolsky-type and Regge–Wheeler-type systems but not a separated form. Hintz (2026, arXiv:2609.33661) found a matrix integrating factor that removes the same-chirality coefficient A from the first-order derivatives and makes the remaining coefficient matrix split into a radial and an angular part; from this he derives separation of variables and mode stability for subextremal Kerr–Newman black holes. The algebraic core of that derivation is a chain of explicit, local, coordinate-level transformations between first-order systems on the exterior region. This mission formalises that chain.
Prior formalised material on this platform: the Boyer–Lindquist Kerr vacuum certificate and the Exact Vacuum Atlas I/II coordinate certificates and transports (same author, same environment). None of them touch perturbation theory; this mission starts a new, independent layer and does not depend on them.
Fix subextremal Kerr–Newman parameters , , with (Lean: Hintz2026.SubextremalKN). Put , , and work on the open set
(Lean: U p, with x 0 = r, x 1 = θ). Write , . Fix a frequency and an azimuthal number (kept real in Lean; integrality is not used by any statement here), and put , .
The first-order operators of the Newman–Penrose formalism in these coordinates are, for a label ,
with daggers obtained by , . Partial derivatives are coordinate-slice derivatives (Lean: cpd), and all fields are complex-valued functions on that are on .
System (1) (positive spin) is the system (1a)–(1d) of Hintz for the four rescaled mode quantities ; the negative-spin system is obtained from it by the replacement rules stated in the paper (Lean: res1a–res1d, res1aN–res1dN, each the difference "left side minus right side"). The chiral variables (3) are
System (4) is with the explicit matrices , and scalar of the paper (Lean: A, Bmat, cscalar; is the spin label). The integrating factor is the matrix of equation (5), with , and system (7) is
for , and . The paper's separation statement is that with four explicit coefficient functions .
for both spins (Lean: Hintz2026.main_pos, Hintz2026.main_neg, with the on- forms main_pos_on_U, main_neg_on_U). The composite transformation is explicitly invertible on : first recover and , then apply the inverse chiral map invPos or invNeg. The goal leaves the frequency and azimuthal parameters free, assumes nothing beyond subextremality and regularity on , and does not assert anything at the horizon or at infinity.
Dminus_X_eq_AX, Dplus_XstarInv_eq).Dm_Xv_sub_AXv, Dp_Yv_add_AYv, Dm_zero_iff_Xv_residual_zero_on_U, …).Cmat_eq_Csep), and .system4_iff_system7).ident_*, identN_*), and the equivalence (1) ⟺ (4) (sys1_iff_sys4_pos, sys1_iff_sys4_neg).The chain (1)→(4)→(7) is the step on which the rest of Hintz's argument rests: once is known to separate, the angular operator can be diagonalised and the radial problem reduces to a scalar second-order equation, which is where the mode-stability argument lives. The transformations are algebraic but far from trivial to check by hand — each entry of is a rational-trigonometric expression in , , , and the three parameters, and the cancellation of all mixed terms is the content of the separation claim.
Everything in this mission is already proved in the paper. What the mission adds is a machine-checked verification of the explicit coefficient data and of the transformation identities for arbitrary fields, with the regularity and domain hypotheses made explicit. All targets listed here already carry accepted proofs on this platform; the mission records them as a public, reviewable dependency tree. Not formalised here: the derivation of (1) from the Einstein–Maxwell equations, the angular eigenvalue problem, the radial reduction, the Whiting-type transform, and mode stability itself.
The naive approach — substituting the chiral variables into (4) and comparing with (1) term by term — produces hundreds of rational terms with half-integer powers of and of . The first-order terms match by construction; the difficulty is that the zeroth-order terms only match after using , and the specific values of , , . A second trap is in the negative-spin system: the replacement rules put sign changes inside the operators, and an identity proved for a "simplified" version of the rules would be an identity about a different system. The formalisation keeps the rules literally and derives linearity separately.
Coordinates are with , ; no manifold, tetrad or spacetime object is defined. Derivatives are coordinate-slice derivatives (deriv along one coordinate), and the final unknown-field interfaces use ContDiffOn ℝ ∞ _ (U p); auxiliary statements may require only coordinate-slice differentiability, and explicit coefficient statements retain the stronger analytic order ω. Real exponents , are Real.rpow; is Real.sqrt. All coefficient matrices are explicit Matrix (Fin 2) (Fin 2) ℂ; the separated form is an independent explicit definition, not derived from , so Cmat_eq_Csep is a genuine check. The spin label is a real parameter in the definitions of and ; the two spins are the instances , each proved separately with its own chiral variables.
Nothing here is vacuous: the systems are Props about arbitrary fields, the residuals are explicit, and the domain is nonempty and open. A reader can check that the Lean definitions reproduce the paper's formulas from the transcript of the paper's equations included with the source.
Reusable beyond this mission: the slice-derivative calculus (cpd, Dm, Dp, product and sum rules), the integrating-factor layer (X, A, invertibility, residual identities) and the prefactor calculus for .
A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. For the sequence space c₀, Leo (2022) proved plasticity of the unit ball under the extra hypothesis that the inverse map is continuous; the project's earlier results, all unpublished, covered c₀(Γ) itself without that hypothesis (the earlier c0 mission), smooth strictly convex blocks of any finite dimension and strictly convex planes, with scalars beside them, ℓ¹ₙ blocks of bounded dimension, and polygonal planes, also beside discs. This mission formalizes a proof that the closed unit ball of every c₀ sum of real spaces of dimension at most two is plastic, for arbitrary index sets and arbitrary norms on the blocks, together with the two-space statement that every nonexpansive bijection between the balls of two such sums is an isometry. The results come from an unpublished research project on the plasticity problem.
For a family of real normed spaces, the sum consists of the families with and along the cofinite filter, with the norm . Its closed unit ball is . The blocks here have dimension at most two: zero, the real line, or a real plane with any norm, whose unit ball may be a parallelogram, a polygon, a disc, or have flat edges and curved arcs in any combination, with no uniformity over .
For finite index sets the balls are finite-dimensional, and both statements are covered by Zavarzina's theorem for finite-dimensional targets (Ann. Funct. Anal. 9 (2018), Theorem 3.8); the content is the infinite case.
The result. It settles plasticity for all c₀ sums of blocks of dimension at most two. It gives the first infinite c₀ sums in which scalar coordinates sit beside polygons or other planes that are not strictly convex, and the first non-polygonal planes that are not strictly convex (a curved ball with two edges meeting at a corner, or with countably many extreme points). Its proof shows that nonexpansive bijections between such balls are block-diagonal linear isometries, with scalar blocks going to scalar blocks after each parallelogram plane is split into two scalar coordinates.
Formalizing it. The proofs exist only in the project's notes and were checked by AI referees; a machine-checked proof is the independent confirmation sought. Known inputs available in this environment through earlier missions are invariance of domain, the Freudenthal–Hurewicz theorem and Brouwer's fixed-point theorem; Baire's theorem, Krein–Milman and Mazur–Ulam are in Mathlib.
For infinite index sets the ball is not compact, its unit sphere has large flat faces, and no regularity of the inverse map is assumed. The planar geometry is the bulk: covers of a planar ball by three translates near corners where two edges meet, an extreme lens and a far-comparison estimate at extreme points where the norm is curved, and the linearization of an extreme-point correspondence between two different planes from a single radial inequality. The c₀ part must match blocks, exclude scalar coordinates that feed planar blocks, and exclude the collapse of a block by a two-lift argument.
Real scalars, arbitrary index sets (no countability or nonemptiness assumed), arbitrary norms on the blocks.
The sum is Mathlib's lp E ⊤; the c₀ sum is the submodule c0Sum E of it (definition Plasticity_C0Sum), with its subspace norm.
"Dimension at most two" is Module.rank ℝ (E i) ≤ 2, which excludes infinite-dimensional blocks.
The goal uses HasPlasticUnitBall (definitions Plasticity_Basic); the two-space theorem is stated for functions between the subtypes Metric.closedBall (0 : c0Sum E) 1, with LipschitzWith 1 and Function.Bijective.
Extremal graph counterexamples, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
Write for the maximum number of edges in an -vertex simple graph containing no subgraph copy of , with value if there is no eligible graph; a copy is an injective edge-preserving map and need not be induced. For a finite family of finite simple graphs, each encoded on for its own , let be the maximum edge count over simple graphs on containing no copy of any member of , again taking for an empty collection. There exist a nonempty such family and real constants such that every member is connected, bipartite, and not acyclic; for each , for all sufficiently large natural , with a threshold that may depend on ; for every and every simple graph on containing no copy of any member, ; and for every , . These last two bounds use the same and include . The conclusions also include and , as equalities and inequalities of real numbers. No member and real constant satisfy for all sufficiently large . Moreover, the assertion that every nonempty finite family of finite simple graphs whose members each contain a cycle admits such a member and constant is false.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, J_CompactnessConjecture.json, J_TwoDegenerateGraphs.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Multicolor triangle Ramsey numbers, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For each , let be the infimum in of the integers such that every labeling of the edges of the complete simple graph on by colors has a monochromatic triangle; equivalently, no such labeling has every color graph free of a three-vertex clique. This is the least such when the set is nonempty, with infimum for an empty set. Both of the following hold: for every integer , , where all quantities in the inequality are real; and as , meaning that for each real there is such that whenever . The root sequence is defined also at using real division , so that term equals and does not affect the limit.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, I_MulticolorTriangleRamsey.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Ehrhart volume inequality, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
Let be any positive natural number and any convex compact set with nonempty interior. Write for its Lebesgue measure converted from to a real number, and define its barycenter as . The conversion sends infinite measure to zero and real inversion is total, but these hypotheses make finite and positive. If this barycenter is the zero vector and , then . The lattice condition says both that the origin lies in the interior and that no other integer vector does. The volume in this inequality is the real Lebesgue volume itself.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, F_EhrhartVolumeInequality.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Hardness of the closest vector problem, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For every Boolean language of finite bit strings for which there exist a polynomial and a deterministic polynomial-time Boolean verifier satisfying if and only if there is a bit-string certificate with and , there exists a total deterministic polynomial-time map on bit strings sending every with into the following YES set and every with into the following NO set. An instance consists of a natural dimension , an integer matrix with , a target all of whose coordinates are integers, and a rational radius . It is in YES exactly when some satisfies , and in NO exactly when every satisfies . The sets consist of the exact encoded instance strings, formed by concatenating the encodings of , , the target coordinates in order, and the matrix entries in row-major order. Each scalar is encoded by taking its library natural-number code, applying the library's natural-number-to-bit-string encoding to get a word , and prefixing with true bits followed by one false bit. Strings without such a valid encoded instance, and instances satisfying neither distance condition, are outside both sets; dimension one is included. Polynomial time is witnessed in the library's TM2 machine model, using its product encoding of Boolean lists for verifier input, its Boolean output encoding for the verifier, and identity encodings for the reduction's input and output.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, H_GapCVP.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Arithmetic formula lower bounds for the permanent, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For every natural number and every finite arithmetic formula whose leaves are variables , , or arbitrary complex constants and whose binary operations are addition, subtraction, multiplication, and division, assume that every divisor subformula evaluates to a nonzero element of the fraction field of and that the value of in this fraction field equals the polynomial under the canonical inclusion. Then the number of variable-leaf occurrences satisfies , with both sides viewed as real numbers. Repeated occurrences are counted separately, constants contribute zero, and the leaves of both operands of each operation, including division, are counted. Nonzero divisors are required as rational functions, not at every numerical substitution.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, C_PermanentFormulaLowerBound.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Counterexamples to Connes rigidity, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
There exist a countable group and a sequence of countable groups , indexed also at , such that all of them are finitely generated and infinite, every conjugacy class of a nonidentity element in each such group is infinite, and every such group has property T. For every , is isomorphic to as specified below, and for every , including , is isomorphic to in the same sense. If , there is no group isomorphism , and for every there is no group isomorphism . For each group concerned, property T means that, for every complete complex inner-product space and every homomorphism , if for every finite and every real there is a vector with and for all , then there is a nonzero vector fixed by every . Here is the double commutant, inside the bounded complex-linear operators on , of the left translations , and . An asserted isomorphism of these tracial algebras is a complex -algebra equivalence preserving such that both it and its inverse preserve every existing supremum of any set of self-adjoint idempotents, with projection order defined by .
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, E_ConnesRigidity.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
A finitely presented non-sofic group, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
There exist a set and a group structure on such that has a finite presentation and is not sofic in the following precise sense: there are a finite subset and a real number for which no positive integer and map with simultaneously satisfy for every and for every with . Here is normalized Hamming distance; is defined on all of and is not assumed to be a homomorphism. The finite subsets in the defining sofic approximation property include the empty subset, and the permutation sets are required to be nonempty.
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, D_NonSoficGroup.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
Binary and spherical codes, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For every real with , the following strict inequality holds. Write , with the total-real logarithm convention . Let be the maximum cardinality of a finite subset of in which every two distinct words differ in at least coordinates, and put . Empty codes are permitted in the maximum; the sequence term is zero by total real division. Define and , a real infimum. Then .
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, B_BinaryCodes.json, B_SphericalCodes.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
High-dimensional sphere packing, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.
For each natural number , let consist of complex-valued Schwartz functions on Euclidean whose values and Fourier-transform values are real, with for every , , and whenever ; radiality is not required. Put , , and , where the infimum is taken in . Put , , and . The assertion is the conjunction of the following ten claims: ; there exists a real sequence such that for every ; ; ; there exists a real sequence such that for all sufficiently large ; there exists a real sequence , nonnegative for every natural , such that for all sufficiently large and every , ; ; ; ; and there exists a real sequence such that for all sufficiently large . Each limit is along natural dimensions tending to infinity, and the four existentially quantified error sequences need not coincide. The sequences are defined also at using total real operations, in particular and division by zero equal to zero; the displayed powers denote those real powers.
Additional targets:
The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.
Sources: Lean formalization, A_SpherePacking.json.
Planned collection: OAI Ten Proofs (oai-ten-proofs).
The Angel problem asks whether bounded movement can overcome an adversary that destroys one square per turn on an infinite chessboard. It is a question about strategies for arbitrarily long play, rather than about finding a path through one fixed configuration. The Devil may act anywhere on the board, including far ahead of the Angel. The movement range therefore has to be compared with a changing obstacle set and with an opponent that observes earlier moves.
This mission collects the complete classification for natural-number powers in one formal development. The power-one loss is the known Berlekamp king-capture result described in Kutz's 2004 thesis, Section 1.1. The power-two win is Mathe's Theorem 4.6 (2007). Higher powers and the exact threshold are consequences of these published results and the movement rules. This is formalization of known mathematics; it does not propose a new solution to an open problem.
A square is a point of the integer lattice . The Angel starts at the origin. Its power is a natural number , including zero. A legal jump changes each coordinate by at most in absolute value. Intermediate squares impose no restriction, and zero-length moves are allowed. Thus power one has the movement range of a chess king, while power zero cannot change position.
The ordinary Devil moves first in every round. It chooses at most one square to burn, or passes. A burned square remains burned. Repeated choices are allowed and do not destroy additional squares. Naming the Angel's currently occupied square is permitted; the loss condition is checked at the Angel's subsequent landing. The Angel loses if its destination is burned or its displacement exceeds its power.
A strategy uses only the finite history available at the time of the move. A Devil strategy receives the visited positions. An Angel strategy receives these positions and the Devil actions, including the action just taken in the current round. Every pair of strategies defines a play by recursion. Write when all rounds of this play have legal, unburned landings, and define
The mission's main theorem is the exact classification
Its two principal outcomes are
and
The first statement supplies one Devil strategy defeating every power-one Angel, rather than an opponent chosen separately after seeing a complete Angel play. Likewise, the Angel's winning strategy is chosen before the opposing Devil strategy. All these statements use the same game definition.
The source milestones retain the original Nice Devil reduction and escape theorem, add Mathe's power-two theorem explicitly, and include the king-capture result from Kutz Section 1.1. A Nice Devil protects the origin and every square within movement range of any visited position other than the most recent position. The corresponding Angel objective includes leaving every finite box. This restricted opponent is an intermediate target; the headline classification concerns the ordinary, unrestricted Devil. Monotonicity and the higher-power corollary are available in the linked theorem dependency graph without attributing invented theorem numbers to either source.
The classification identifies the exact integer threshold: one square of movement in each coordinate is insufficient, whereas two suffice. It distinguishes unlimited survival from success for a fixed number of rounds. The lower endpoint is covered as well, because the formal parameter is a natural number rather than a strictly positive integer.
The formal development makes the quantifier order, observation rules, and geometric assumptions inspectable. The classification and both principal outcomes already have machine-checked proofs. The repository audit records 228 checked local theorems and six accepted extension submissions. Its classification dependency graph contains 37 nodes, 66 edges, and zero open leaves. These are verification results, not independent peer review or a new mathematical publication. The mission now presents this completed body of work as one navigable result.
A finite simulation cannot establish survival against every opponent forever. Conversely, failure of several candidate Angel strategies does not establish a uniform winning Devil strategy. Finite and infinite play must be related without reversing the strategic quantifiers. The geometric statements also have to constrain the evolving play, rather than describe only a static drawing. For the king-capture result, local boundary restrictions must remain valid after every legal move; for the power-two result, the source's confinement and escape assertions must refer to the same operational game.
The implementation uses integer pairs, finite histories, optional Devil actions, finite sets, and recursion on natural numbers. Lean 4.33.1 and the pinned Mathlib revision match the platform environment. The closed local entry point is Solutions.PowerClassification; Solutions.Completed retains the original Mathe assembly. The definitions do not assume a winning strategy or restrict the headline game to a finite board.
The king-capture implementation uses deliberately loose radius-100 constants for an internal confinement argument. It does not claim an optimal capture time or a formalization of the smallest board illustrated by the source. Fractional speeds and Devils burning multiple squares per turn are outside this mission. Reusable material includes finite-game determinacy, finite-survival compactness, journey reduction, connected-square boundary estimates, and strategy monotonicity. Independent reproduction and documentation improvements are welcome; there is no remaining open proof obligation for the stated classification. Platform reference mirrors containing sorry are kept separate from the closed local proof library, whose audited dependencies contain only the standard Lean axioms.
A graph homomorphism sends vertices of one graph to another while preserving adjacency. Requiring this map to be continuous makes graph coloring sensitive to topology: each color must occupy an open and closed region. For integer lattice actions, the resulting questions connect finite graph structure with continuous dynamics. The results considered here give an algebraic sufficient condition on a finite target graph that works in every finite lattice dimension. They are Theorem 1.4 and Proposition 7.1 of Ruijun Wang's Continuous graph homomorphisms of higher dimensional abelian group actions, a 2026 research preprint.
Fix an integer . The integer lattice is , with standard generators . Each generator has one coordinate equal to one and all other coordinates zero. An action of on a space assigns maps satisfying and . A continuous action uses the discrete topology on . It is free when implies .
A Polish space has a topology induced by a complete separable metric. It is zero-dimensional when its topology has a basis of clopen sets, meaning sets that are both open and closed. The standard Schreier graph on joins to for each generator, with adjacency understood symmetrically.
Let be a finite simple graph on a vertex set , equipped with the discrete topology. A continuous homomorphism is a continuous function such that
Write when such a map exists for every free continuous lattice action on every zero-dimensional Polish space.
A closed walk starts and ends at the same vertex, and its length counts edges. Repetitions are allowed. The reduced homotopy group identifies based closed walks under cancellation of a spur and cancellation of a closed four-walk, with these relations compatible with concatenation. Its identity is the constant walk. These conventions agree with Section 2.
Theorem 1.4 assumes an odd closed walk whose reduced class has trivial square:
The source statement appears in Section 1.
The main target, Proposition 7.1, permits any finite order:
Here is a positive integer; it need not be the least exponent. The square-trivial case follows by taking . The stronger statement is given in Section 7.1.
These results turn one finite algebraic witness into a conclusion covering all the spaces, actions, and positive dimensions specified above. Once a graph satisfies the hypothesis, an individual action requires no additional dynamical condition beyond the stated assumptions. The conclusion concerns finite discrete targets and the standard generating set.
Both results are established in the cited paper. Complete local Lean proofs now cover their full universal statements. The local project build and kernel audit have passed, and the final declarations use only Lean's standard logical axioms. Prove2Me has accepted the complete uploaded proof dependency graph. Both original headline theorem identities now have status Proved.
The completed development supplies reusable statements and checked infrastructure for lattice actions, reduced graph walks, finite probability distributions, and continuous graph homomorphisms. These components support inspection and reuse beyond the two headline results.
Choosing a homomorphism separately on each orbit does not ensure continuity across nearby points of the space. Freeness identifies each orbit with a lattice once an origin has been chosen, but does not supply continuously chosen origins across all orbits. A proof must therefore establish continuity of the resulting vertex map itself. Restricting attention to one action, one dimension, or an orbitwise map would leave the stated universal conclusion unresolved.
The lattice is represented by , actions use additive notation, and standard adjacency includes both orientations of each generator edge. Reduced homotopy is an inductively generated relation on genuine Mathlib graph walks; powers are repeated concatenations. The target vertex type is arbitrary and finite, with its discrete topology.
Source spaces and target vertex types have independent universe parameters. Empty source spaces are allowed. No connectivity assumption is imposed on the target, and no separate nonemptiness hypothesis is added. The odd-walk witness already forces target nonemptiness. Neither a carrier-construction assumption nor an approximation condition appears in either final theorem.
Finite order refers to the class of the walk, rather than its length. An odd walk can revisit vertices and traverse edges repeatedly, so the hypothesis does not require an embedded cycle. All four-walk relations are included, including those with repeated vertices. The conclusion asserts existence of a continuous adjacency-preserving function; it asserts neither uniqueness nor injectivity. These distinctions matter when comparing a formal declaration with the source: replacing arbitrary closed walks by simple cycles or adding connectedness would change the objects quantified over. The recorded statements retain the wider walk convention used in the paper.
Further contributions can reuse the infrastructure or establish related variants while preserving these conventions. Any changed statement should distinguish its additional hypotheses and its altered conclusion from the two results recorded here.
Ruijun Wang, Continuous graph homomorphisms of higher dimensional abelian group actions, arXiv preprint arXiv:2609.39824v1, 2026. Version and source; Theorem 1.4; definitions; Proposition 7.1.