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.
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?
An o-minimal structure is a setting in which every definable subset of the line is tame: a finite union of points and open intervals. This single axiom rules out oscillation, space-filling behavior, and other pathologies, and it makes one-variable definable functions tractable. The central consequence is the Monotonicity Theorem: every definable function on an interval is piecewise constant or strictly monotone and continuous, with only finitely many pieces.
The result originates in the work of Pillay and Steinhorn on o-minimality and is presented systematically in Lou van den Dries, Tame Topology and O-minimal Structures, Chapter 3 (Cambridge University Press, 1998). A concise expository account is given in Mário Edmundo, O-minimal structures (arXiv:math/0012051). This mission formalizes the one-dimensional monotonicity theorem and its supporting lemmas in Lean 4 against Mathlib, as a verified entry point to o-minimal geometry.
Let be a type equipped with a dense linear order without endpoints : an irreflexive, transitive, trichotomous relation in which every strict inequality admits an interpolant and every element has strict predecessors and successors. Finite Cartesian powers are represented as coordinate tuples , with coordinate projections, deletion, and append operations defined explicitly.
An o-minimal structure over is a family of collections of subsets of , closed under finite unions and intersections, containing diagonals and the order relation, closed under products, coordinate reindexing, and existential projection, and satisfying the o-minimality axiom: every member of is a finite union of points and open intervals. A definable function with domain and codomain is a dependent function on the corresponding subtypes whose domain, codomain, and graph are all members of .
For in , the open interval is the set of coordinate tuples whose single coordinate lies strictly between the two endpoint values, with endpoint variants allowing and . A function is strictly increasing (respectively strictly decreasing) on when implies (respectively ) in the first output coordinate. Continuity at a domain point is the graph-based epsilon-delta predicate: belongs to exactly when the graph meets every sufficiently small box around in the graph of a locally oscillation-free correspondence. Finiteness and infinitude of one-dimensional sets are expressed through first-coordinate listings.
An open cell is good when restricted to is constant, or strictly increasing and continuous there, or strictly decreasing and continuous there. The number of cut points is finite and depends on , , and ; no bound on is asserted.
The result itself. The Monotonicity Theorem is the foundation of one-dimensional o-minimal geometry. It implies that definable sets have finitely many connected components, that definable functions have finite limits at endpoints, and that higher-dimensional cell decomposition can proceed by induction on dimension. Without it, the correspondence between definability and geometric tameness remains unestablished.
Formalizing it. The classical proofs are known and appear in the references above; what is missing is a machine-checked version with explicit definability bookkeeping. This mission produces Lean 4 declarations for the order, interval, monotonicity, graph, and continuity predicates together with the theorem and its lemmas, all verified against the pinned Mathlib revision. The definability infrastructure (products, projections, fiber extraction) is reusable for subsequent cell-decomposition missions. Status honesty: the one-dimensional interval-extraction lemmas are machine-checked; the local constancy-or-injectivity lemma, the injective-to-monotone lemma, the finite-partition assembly, and the goal theorem itself remain open targets.
The naive argument fixes a point and inspects nearby values, but definability does not by itself provide any neighborhood on which behavior is uniform. The fiber dichotomy illustrates the obstruction: knowing that each fiber is definable does not decide whether some fiber contains an interval or every fiber is finite, and the two cases require different constructions (a constancy interval versus an injective-selection interval). Similarly, injectivity alone does not yield monotonicity without partitioning the domain by local sign patterns and applying o-minimality to select a uniform pattern on a subinterval. Each step fails until the relevant definable set is exhibited and the one-dimensional interval lemma is applied to it.
Lean represents one-dimensional points as functions , with order, intervals, and finiteness stated through the first coordinate. Definability is always the structure membership predicate , never an informal attribute. Continuity is the graph-based predicate applied to ; a submission that discharges a continuity goal from the domain inclusion alone, or that replaces the continuity predicate by the domain set, does not satisfy the statement. The goal quantifies over cut points with , , and strict increase at each step; the intervening sets are the open intervals determined by consecutive finite endpoints.
Contributions welcome: direct proofs of the open leaves (fiber definability, the finite-fiber injective-interval construction, the injective-to-monotone step, the finite-partition assembly), sharper statements with explicit endpoint bounds, and reusable o-minimal infrastructure beyond this mission. Out of scope: higher-dimensional cell decomposition, differentiability, and integration of definable functions.
The fundamental lemma is a family of identities between orbital integrals on a reductive group and stable orbital integrals on a smaller group attached to it, its endoscopic group. Langlands isolated these identities in the 1970s as the last missing ingredient in the comparison of trace formulas, and Langlands and Shelstad formulated them precisely in 1987; Waldspurger reformulated the statement for Lie algebras and proved that the Lie algebra form implies the group form. The Lie algebra statement was proved in equal characteristic by Bao Chau Ngo in Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), by a global geometric argument built on the Hitchin fibration; Waldspurger's earlier work transfers the result to mixed characteristic. The identity is the engine behind the stabilization of the trace formula and behind the computation of the cohomology of Shimura varieties.
Both sides of the identity carry a normalizing factor built from the discriminant, and the exact power of relating the two normalizations is fixed by a purely root-theoretic computation carried out in Ngo's §1.10-§1.11. That computation is the subject of this mission. It is self-contained, it uses no geometry, and it is the first piece of the paper that can be stated in Lean today.
Let be a split reductive group over a field with maximal torus , character lattice , cocharacter lattice , root system and Weyl group . Write for the Cartan subalgebra, so that each root has a differential , a linear form on . Ngô's discriminant is the product
a -invariant polynomial function on and hence a function on the space of characteristic polynomials.
An endoscopic datum is an element of the dual torus . The endoscopic group attached to it is the group whose root system is
with Weyl group and its own discriminant . Choose a subset containing exactly one root out of each pair of opposite roots outside , and set
Finally let be a non-archimedean local field with valuation and residue cardinality , and recall Ngô's normalizing factors and .
for a point of the endoscopic Cartan with image . Equivalently with : this is exactly what lets one pass between the two forms of the fundamental lemma, and .
The identity above is the image under of the divisor identity of 1.10.3, which in turn rests on the fact that — which depends on a choice of — is nevertheless -invariant, and on the fact that really is a root subsystem. The milestone list follows that order.
Theorem 1 of Ngô's paper, the Langlands-Shelstad conjecture for Lie algebras, is the identity for corresponding regular semisimple stable classes, under the hypothesis that twice the Coxeter number of is smaller than the residue characteristic. Nothing in that statement can be written in Lean today: reductive group schemes over a discrete valuation ring, endoscopic data, Kostant sections, orbital integrals and affine Springer fibers are all absent from Mathlib. What can be written, faithfully and without any placeholder, is the root-theoretic layer that fixes the transfer factor, and that is what this mission asks for. It is a genuine prerequisite: the two displayed forms of Theorem 1 differ precisely by the identity above.
The mission also produces reusable infrastructure — the discriminant of a root system, the notion of a closed subsystem and its Weyl group, the endoscopic subsystem cut out by an element of the dual torus — none of which currently exists in Mathlib, and all of which any future formalization of endoscopy will need.
Only one of the four milestones is a routine manipulation. Splitting into pairs and collecting squares is bookkeeping; that is -invariant is immediate because permutes . The content is in Lemma 1.10.2: is not stable under , so carries to , where counts the roots of sent into ; the claim is that is always even. The naive attempt — check it on the generating reflections of — is exactly where a careless argument goes wrong, since it is false for reflections in roots outside . Ngô's argument identifies the sign with , the ratio of the sign characters of and , and observes that both compute the determinant of acting on the same reflection representation.
Root systems are modelled with Mathlib's RootPairing ι R M N: the module plays the role
of , the module the role of and of the Cartan on which the differentials
are evaluated, and is the linear form . The endoscopic
subsystem is cut out by an element of the dual torus, taken as a group homomorphism
from the cocharacter lattice to an arbitrary commutative group, and is expressed over
coefficients as in the definition of a root datum. Products over and are
finite products over a Fintype index, and a choice is a Finset satisfying an
exclusive-or condition, which automatically rules out the degenerate case .
The identity 1.10.3 is stated as an identity of functions on the Cartan rather than as an identity of divisors, so the unit is carried explicitly rather than discarded. Lemma 1.10.2 is stated over for an honest root system, since the sign argument uses the reflection representation. The goal 1.11.3 is stated for an additive valuation with values in , which is what makes the two sides comparable when a discriminant vanishes.
There is no trivializing formalization here: the hypotheses of every item are satisfiable — any root system with any closed subsystem and any choice of gives an instance — so none of the statements is vacuous, and none of them is an identity between two occurrences of the same expression.
Contributions of the surrounding theory are welcome: a positive system compatible with a subsystem, the sign character of a Weyl group, and the reducedness of the discriminant divisor (the remaining half of Lemme 1.10.1) are all natural next steps.
A coset partition of a group is a finite family of left cosets that are pairwise disjoint and cover . In 1974 Herzog and Schönheim asked whether the indices of such a partition, with , can be pairwise distinct. They cannot when — there a coset partition is an exact covering system of the integers, and Davenport–Rado and Mirsky–Newman showed the largest modulus must repeat — but for general groups the question is still open, even for finite solvable groups.
Progress has come in two styles. Structural: Berger, Felzenbaum and Fraenkel settled finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333 and finite pyramidal groups in Fund. Math. 128 (1987) 139–144. Order-bounded: Ginosar and Schnabel (2011) settled every whose order has at most two prime divisors, and Margolis and Schnabel (2019) verified all .
The paper formalized here, Z.-W. Sun, J. Algebra 273 (2004) 153–175, takes a third route: it constrains the subgroups rather than the group, and simultaneously weakens "partition" to "uniform cover". Its hypothesis — that the be subnormal — costs nothing in the nilpotent case (every subgroup of a nilpotent group is subnormal) yet applies to arbitrary, possibly infinite, ambient groups . It also answers negatively an open question of the same paper, generalizing one of Erdős: the indices of such a cover cannot all be large if each occurs only boundedly often.
Let be a group, written multiplicatively. For a finite system
of left cosets, the covering function counts memberships,
If is constant, say , then is a uniform cover of of weight ; the case is exactly a coset partition. A uniform cover is trivial when for every , and this is the only degenerate case that must be excluded. Uniform covers are genuinely more general than partitions: one may have no disjoint subcover at all.
A subgroup is subnormal if some finite chain reaches , each term normal in the next. Normal subgroups are subnormal; in a nilpotent group every subgroup is; and shows a subgroup of a solvable group need not be.
Write for the indices, always assumed finite, and
for their least common multiple, whose prime divisors are exactly those of . Let and denote the least and greatest prime divisors of , let be Euler's totient, and let
be the largest multiplicity with which an index is repeated. The Herzog–Schönheim conjecture says .
The goal theorem is Theorem 4.3(i) of the source: for a nontrivial uniform cover of any group by cosets of subnormal subgroups of finite index, some index divisible by the largest prime is repeated at least times,
In particular . Two weaker consequences are separate targets. Since , this gives the Herzog–Schönheim conjecture for subnormal uniform covers,
and the quantitative step behind it is a Burshtein-type inequality, which after clearing denominators reads
The result itself. It is the widest structural class in which Herzog–Schönheim is known, and the only one that does not require to be finite: subnormality of the is a condition on the subgroups, so itself is arbitrary. It strictly contains the nilpotent case of Berger–Felzenbaum–Fraenkel, and being quantitative it also yields the Burshtein conjecture in this setting — a bound no purely qualitative statement gives. Because the conclusion is a lower bound on growing with , it answers the paper's open question: one cannot make all the indices of a uniform cover large while keeping every multiplicity bounded.
Formalizing it. Nothing here is open, and the mission is the machine-checked version of a known
proof. What it adds is a formal vocabulary for uniform covers — Mathlib has
Mathlib/GroupTheory/CosetCover.lean (B. H. Neumann's theorems, ) but no
notion of covering multiplicity — and the arithmetic of subnormality, in particular that
divides when the are subnormal. Mathlib has
Subgroup.IsSubnormal with the basic closure properties but nothing about indices of subnormal
subgroups, and that divisibility is the whole reason subnormal covers behave. The totient measure
this proof runs on is already formalized: Sun's Lemma 3.1 is Berger–Felzenbaum–Fraenkel's equation
(14), already proved on the platform as BFFPyramidal.muMeasure_divisorClosure_image_mul, and
this mission reuses that definition file rather than duplicating it.
Status disclosure. Complete Lean proofs of the goal and of every milestone below already exist and will be submitted at launch, so this mission is not an open frontier: its value is the verified artifact, the reusable vocabulary, and the fact that the development turned up two places where the published argument needs repair or can be simplified (see Formalization scope). Alternative proofs, sharper variants, and the analytic parts excluded below remain genuinely open contributions.
The reciprocal identity is the first thing anyone writes down and it is not enough: a uniform cover of weight satisfies , and pairwise distinct can do that.
The real obstruction is that a cover does not descend to a quotient. A part need not lie in one coset of a chosen normal subgroup, so the induction that proves the finite nilpotent case has nothing to induct along once may be infinite and the are merely subnormal. Sun's replacement is a lower bound for the size of a union of cosets, Theorem 3.1: if for all and , then the number of cosets of inside is at least the number of divisible by some . The union is compared not with the but with a purely numerical shadow of itself in , and it is here that subnormality enters, through the divisibility (Lemma 2.1) — for arbitrary finite-index subgroups Poincaré gives only the inequality , which is too weak.
The second difficulty is arithmetic and is where the source spends its effort. Turning Theorem 3.1 into a bound on multiplicities (Theorem 3.2) requires computing the density of a union , and the identity the paper uses (Lemma 3.4) expresses that density as times an infinite sum of reciprocals over -smooth elements of the union. Along that route the full series is needed: truncating it loses precisely the geometric factors that produce the divisor sum in the conclusion.
It is worth saying, though, that this analytic detour is avoidable — a solver need not take it. Theorem 3.2 can also be reached by a purely finite argument: bound the density from below by injecting each index into the divisor , which is sharp in the same cases as the series argument. Lemma 3.4 remains a faithful and separately interesting milestone of the paper, but it is not on the critical path to the goal. The naive version of the finite estimate — bounding the density below by — is genuinely false, as shows, so the injection is the content, not a one-liner.
The development commits to the following conventions, worth stating because the prose leaves them implicit.
Covers are indexed families rather than sets of cosets: IsUniformCover K a w asserts that for
every the number of indices with is exactly w, counted as
Nat.card of a subtype so that no decidability hypothesis is needed. Indexing by Fin k keeps
multiplicities visible, which matters because every conclusion counts indices, not distinct
subgroups. Nontriviality is never folded into the definition; it appears as the explicit
hypothesis ∃ i, K i ≠ ⊤, and without it every statement here is false (take , ).
is an arbitrary group — not assumed finite. Finiteness enters only through
Subgroup.FiniteIndex on each , which the source assumes implicitly when it writes "the
(finite) indices". Indices are Subgroup.index and is H.relIndex (K i). For a
subgroup that is not assumed normal, G ⧸ H is still the type of left cosets and
Nat.card (G ⧸ H) = H.index; Theorem 3.1 is stated with that type, since the it is applied
to is not normal.
Densities are never limits. The density of a union is taken as the
finite ratio for an explicit common multiple ,
which is exactly equal to the asymptotic density and keeps Lemma 3.4 free of any analysis on the
left-hand side; the right-hand side genuinely is an infinite sum and is stated with HasSum over
.
Inequalities are cleared of denominators and stated in wherever possible, so that appears as . Readers should check the direction: subtraction truncates, so is only the intended quantity because every here is prime, hence .
⚠️ Parts (ii)–(iv) of the source's Theorem 4.3 are out of scope. Those bound the primes
dividing the indices, their number, and by and similar, and they rest on Mertens' third theorem,
, which Mathlib does not have. It is worth
being precise about what Mathlib does have, since the gap is narrower than it looks: the prime
counting function Nat.primeCounting, Chebyshev's and with the machinery around
them (Mathlib/NumberTheory/Chebyshev.lean), Euler products
(Mathlib/NumberTheory/EulerProduct/), and the constant itself
(Real.eulerMascheroniConstant) are all present — what is missing is Mertens' asymptotic tying
them together, and the asymptotics. Supplying that is a substantial number-theory
project in its own right, so this mission stops at the arithmetic core, part (i), which is what
implies Herzog–Schönheim. Contributions adding the analytic parts are welcome and would complete
Theorem 4.3.
Two things the development established that the paper does not state. First, Lemma 2.1 is true in a stronger form: needs only subnormal, not both, and needs no finiteness hypothesis at all (with Mathlib's convention that an infinite index is ). Second, Theorem 4.1's passage from the largest prime to the smallest can be isolated as a self-contained arithmetic inequality, , which is tight at prime powers; it is listed as its own milestone for that reason.
Reusable beyond this mission: the uniform-cover vocabulary, the subnormal index divisibility of Lemma 2.1, and Theorem 3.1's union bound, which applies to any attack on Herzog–Schönheim including the still-open solvable case. The source also leaves Conjecture 4.1 open — that for a nontrivial uniform cover by subnormal subgroups the largest index is repeated at least times, its least prime factor — which would be a natural follow-on target.
This mission curates the formalized output of Alethean — an Autonomous Logic Engine for Theorem Hunting, Exploration, And Navigation (alethean.org). Alethean autonomously generates research directions, develops them into research papers, and formalizes their results in Lean 4 — an "ever-expanding registry of absolute mathematical truths," built with the Aristotle reasoning engine. "The unconcealed truth between conjecture and proof."
The corpus's public home is the Alethean Lean 4 Catalog — the central registry of formalized theorems across the ecosystem, browsable as research packages (each with its article, research paper, interactive view, future directions, and Lean 4 proof files). This mission is the platform-side mirror of that registry: 2,799 definition bundles and 7,517 theorems compiled and verified against the pinned toolchain (Lean v4.30.0, Mathlib c5ea003), spanning analytic number theory, combinatorics, probability, information theory, quantum information, tropical algebra, and machine-learning theory.
The corpus arrives fully proved. The goal theorem is the corpus's universal error-detection bound for random checksums — the capstone of the Almost-Lossless compression thread (Compression Beyond the Pigeonhole Bound): appending an independent random checksum makes the probability of silent corruption at most , uniformly over all source strings and all inner decoders. The milestones are capstone theorems from across the corpus: sphere-packing and VC-dimension bounds, second moments of central -values, tropical Arrow-type impossibility, sums-of-three-cubes obstructions, and more.
Every milestone is a verified platform theorem: study the proofs, reuse them as imported lemmas, or rebuild them from first principles. The interesting open work is extension: the corpus's research-direction papers (browsable at alethean.org under Future Directions) state quantitative sharpenings — explicit constants, wider parameter ranges — that are not yet formalized. Pick a direction, formalize its statement, and the verification pipeline does the rest.
53c2925a02)c5ea00351c28e24afc9f0f84379aa41082b1188faether-catalog.A coset partition of a group is a finite family of left cosets of subgroups that are pairwise disjoint and cover . Asking which multisets of indices can occur is a question with two independent origins. For the cosets are arithmetic progressions and a coset partition is an exact covering system of the integers; Erdős asked whether the moduli of such a system can be pairwise distinct, and Davenport and Rado, and independently Mirsky and Newman, showed they cannot — the largest modulus must repeat. For general groups, Herzog and Schönheim (1974) asked the same question: in any coset partition with , must two of the indices coincide? That question is still open.
Progress has come by restricting the group. Berger, Felzenbaum and Fraenkel proved the conjecture for finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333, and the paper formalized here extends it to a wider class defined by a chain condition. Later work bounds the order instead of the structure: Ginosar and Schnabel (2011) settle every whose order has at most two prime divisors, and three prime divisors when , while Margolis and Schnabel (2019) verify all . The conjecture remains open even for finite solvable groups.
Let denote the least prime factor of and the greatest, and let be Euler's totient function.
A finite group is pyramidal if it admits a chain of subgroups
in which every step has index equal to the least prime factor of the order of the preceding term:
A subgroup whose index is the smallest prime dividing the order is automatically normal, so the chain is a composition series; consequently every pyramidal group is solvable, and every supersolvable group is pyramidal. Pyramidality is therefore a chain condition sitting between supersolvability and solvability.
Given a coset partition of , write
The goal theorem is the multiplicity lower bound of Berger–Felzenbaum–Fraenkel. If is pyramidal and the cosets , , partition with , then at least
of the subgroups have the same order.
Two consequences are separate targets. Since whenever , the bound yields the Herzog–Schönheim conjecture for pyramidal groups:
and it likewise settles Burshtein's conjecture in this setting, which concerns the case and bounds the primes dividing in terms of the largest multiplicity.
The bound is quantitative where the Herzog–Schönheim conjecture is qualitative: it does not merely assert that a repetition exists but forces a repetition of prescribed multiplicity, growing with the largest prime factor of . That is what makes it strong enough to also imply Burshtein's conjecture, which no purely qualitative statement does.
The class it covers is also of independent interest. Nilpotent groups are pyramidal, so the result subsumes the authors' earlier theorem, and it reaches groups that are solvable but far from nilpotent. It remains, more than three decades later, among the structural (as opposed to order-bounded) cases in which the conjecture is known.
No part of this development is currently formalized: Mathlib has the ingredients — Sylow theory, Hall subgroups of solvable groups, Euler's totient with Gauss's identity — but neither coset partitions as a structure, nor pyramidality, nor any case of Herzog–Schönheim. The mission produces the first machine-checked proof of a structural case of the conjecture, together with a reusable formal vocabulary for coset partitions.
The reciprocal identity is immediate and useless on its own: distinct indices can satisfy it, so no counting argument over the indices alone can succeed.
The natural attack — induct along the chain, quotienting by — fails because a coset partition does not descend to a quotient. A part need not lie inside a single coset of : if then it meets every coset of , and the induced family on is a cover with multiplicity rather than a partition. Controlling that dichotomy is the first obstacle, and it is precisely where the definition of pyramidality is used, the index being the least prime factor of rather than an arbitrary one.
The second obstacle is that the conclusion counts subgroups of equal order, so the induction must carry a lower bound on the size of a union of cosets that is sensitive to the orders and not merely to their number. The paper's device is a measure on the naturals with , evaluated on the divisor closure of the set of orders; Gauss's identity makes interact correctly with divisibility, and the required inequality is genuinely a statement about the group, not about the multiset of orders. The final step splits off the Sylow -subgroup against a Hall complement, which exists only because pyramidal groups are solvable.
The development commits to the following conventions, all fixed in Lean and worth stating because the prose leaves them implicit.
Coset partitions are indexed families rather than sets of cosets: IsCosetPartition K a asserts
that for every there is a unique index with . Indexing by Fin t
keeps multiplicities visible, which matters since the conclusion counts indices, not distinct
subgroups; and uniqueness encodes disjointness and covering simultaneously. Groups are finite via
[Finite G], and orders and indices are Nat.card and Subgroup.index.
Pyramidality is stated as the existence of a length and a chain c : ℕ → Subgroup G with
c 0 = ⊤, c n = ⊥, and Subgroup.relIndex (c (k+1)) (c k) = Nat.minFac (Nat.card (c k)) for
k < n. Normality of each step is a consequence, not a hypothesis, and is deliberately not assumed.
The greatest prime factor is maxPrimeFac m = m.primeFactors.sup id, which is for
; the floor in is natural-number division, so the goal statement is
(maxPrimeFac l * Nat.totient l) / l + 1 ≤ …. Note that the bound is vacuous at — there
and — so is a necessary hypothesis and is present in every
statement that needs it; a formalization omitting it would be trivially true and is ruled out.
A complete development needs, beyond the goal: the coset intersection lemma; the least-prime-index dichotomy; uniqueness of the Sylow -subgroup of a pyramidal group; the scaling law for the divisor-closure measure; the union lower bound; and solvability of pyramidal groups. The coset-partition vocabulary and the union bound are reusable for any other case of Herzog–Schönheim, including the still-open solvable case, and contributions of alternative proofs or sharper variants are welcome.
A unit fraction is the reciprocal of a positive integer. The number can be written as a sum of distinct unit fractions in infinitely many ways — , , and so on — and the combinatorics of such representations is one of the oldest recurring themes in Erdős's problem lists. Most questions in the area concern size: how many terms are needed, how small the largest denominator can be, how large the smallest one must be. Erdős Problem 287 asks instead about the shape of a representation: how tightly can the denominators be packed?
Order the denominators increasingly and look at their consecutive differences. For the differences are and . The question is whether a difference of at least must always occur, in every representation of , no matter how many terms it has. The problem is recorded in Erdős and Graham's 1980 problem book (ErGr80, p. 33) and was selected for the booklet of favourite problems prepared for the 1999 Budapest conference on Erdős's mathematics ([Va99, 1.15]). It remains open.
Timeline. The weaker statement that some difference must be at least — equivalently, that is never the sum of the reciprocals of a block of consecutive integers — is classical. Theisinger (1915) proved that the harmonic number is not an integer for , using Bertrand's postulate. Kürschák (1918) introduced the -adic argument that proves the general block statement: for , the difference is not an integer. Erdős's 1932 paper [Er32], whose title translates as "A generalisation of an elementary number-theoretic theorem of Kürschák", extends the result from blocks of consecutive integers to arithmetic progressions; the erdosproblems.com entry for Problem 287 cites it for the difference- bound. Nothing stronger appears to be known: the passage from to is the open part, and no partial result is recorded in the entry beyond a conditional one, namely that the conjecture would follow for all but finitely many exceptions if it were known that for every large there is a prime with also prime.
Fix an integer and integers
with
the sum taken in . Call such a tuple a representation of length . The denominators are strictly increasing, hence distinct, and all exceed : the value is excluded because already exhausts the total. The gaps of the representation are the consecutive differences for , and its maximal gap is .
Representations exist for every , and for only the excluded ; no representation of length exists. Examples: with gaps ; with gaps ; with gaps .
This is the open conjecture, stated with no bound on and no restriction on the denominators beyond those in Setting. It is the weakest form that captures the question: asserting a bound for one particular , or for denominators in some range, would be a different and strictly easier statement.
Equivalently: no block of two or more consecutive integers has reciprocals summing to . This is closed mathematics and the natural first target.
The gap-two bound is an immediate consequence, since a representation all of whose gaps equal is exactly a block of consecutive integers.
So the constant in the goal is optimal and cannot be replaced by .
The result itself. A positive answer would say that a representation of by unit fractions can never have all its denominators within distance of each other — a structural constraint of a kind that the size-based results in this area do not provide. The conditional route recorded on the problem page is instructive about where the difficulty sits: it reduces the conjecture, up to finitely many exceptions, to the existence of primes in with prime, a statement of Bertrand-with-extra-structure type that is itself out of reach of current technology. A direct proof would therefore either bypass that route or resolve the conjecture for the remaining cases by different means.
Formalizing it. The gap-two bound and the block theorem behind it are closed mathematics, so the honest description of that part of this mission is formalization, not research. It is nevertheless not already available: Mathlib proves Theisinger's case harmonic_not_int, that for , but not Kürschák's block version , which is the form Problem 287 needs. Supplying it is a genuine strengthening of the library's existing development and is reusable for any question about reciprocal sums over intervals. The goal itself is open, and this mission does not claim otherwise: it is registered with an open proof, and the milestones are what a solver can realistically close today.
The obvious first idea — bound the number of terms, then check finitely many cases — fails immediately, because is unbounded: representations of exist with arbitrarily many terms, so no finite computation can settle the conjecture. The second idea, extending the -adic argument that gives the gap-two bound, also fails, and instructively. That argument works because a block of consecutive integers contains exactly one element of maximal -adic valuation, which leaves the total with negative valuation. Once gaps of size are permitted the denominators may be chosen to avoid that configuration — for instance all even, as in — and the valuation obstruction disappears. There is no evident replacement prime or weighting that rules out all gap- configurations simultaneously, and the conditional result quoted above suggests why: the known routes pass through the distribution of primes in short intervals with a multiplicative side condition, rather than through a congruence obstruction.
A representation is encoded as a function together with the hypotheses ∀ i < k, 1 < f i and ∀ i j, i < j → j < k → f i < f j, and the requirement ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1. Only the values of below are constrained; the function is not required to be monotone or bounded elsewhere, and nothing outside the window is used. The conclusion is ∃ i, i + 1 < k ∧ 3 ≤ f (i + 1) - f i, the existential form of "the maximal gap is at least "; the subtraction is natural-number subtraction, which is harmless because is increasing on the window, so no truncation can occur. The sum is a rational equality, not an approximation.
The statement admits no trivializing reading. The hypothesis 1 < f i is essential and is not vacuous — dropping it would admit , ; the strict monotonicity is what makes the gaps well defined and the denominators distinct; and k ≥ 2 guarantees that at least one gap exists, so the conclusion is not an empty existential. Asserting exactly rather than at least would be false, as has a gap of .
Infrastructure: the block theorem is proved from Mathlib's padicNorm and padicValNat API — padicNorm.add_eq_max_of_ne, padicNorm.sum_lt', padicNorm.not_int_of_not_padic_int, pow_padicValNat_dvd and pow_succ_padicValNat_not_dvd — and needs no new definitions. That development is reusable beyond this mission and is a candidate for upstreaming to Mathlib alongside harmonic_not_int. Contributions are welcome on any milestone independently; a formalization of the conditional reduction to primes with prime would also be a valuable addition, and is not included as a milestone here only because the problem page states it too briefly to formalize faithfully without consulting a primary source.
Quantum algorithms for stochastic optimization are usually presented one paper at a time: a schedule is fixed, a quantum mean estimator is substituted for a classical minibatch, and a new rate is derived from scratch. The derivations are near-identical, and the step that actually differs — the price of one gradient query — is buried inside each proof rather than exposed as a parameter.
This mission publishes a Lean 4 development in which the oracle is a parameter, not an assumption. One rate theorem, instantiated at different oracle contracts and cost models, yields the classical rate, the inexact-gradient rate, and the quantum rate. All constants are explicit; nothing is asymptotic.
The published results it reproduces or corrects:
Let be a real inner-product space, an objective, and a map supplied as a parameter in place of the gradient. The smoothness hypothesis is the descent-lemma inequality
written ; this is exactly what rate proofs consume, and it is implied by a Lipschitz gradient. Write for the initial gap, for the target accuracy, for the gradient-noise scale, for the mean-squared smoothness constant, and for the ambient dimension.
A cost model converts a target accuracy into a query count as a power law with exponent . Its member is the classical minibatch bill, scaling as ; its member is the quantum mean-estimation bill, scaling as . That single exponent is where classical and quantum part company.
The goal theorem is the exact crossover between the two SPIDER bills. Writing and for the dominant terms of the quantum and classical query totals,
the target asserts, for and ,
Every supporting rate is also published and proved: the two SPIDER query totals, SPIDER's correctness, the SGD and PL rates, the exact and inexact gradient-descent rates, the two variance-purchase bills, and the two query counts.
The results. The crossover makes the dimension-versus-accuracy trade-off of quantum stochastic optimization quantitative rather than folkloric. Two readings follow directly: at fixed the quantum advantage disappears as , so the speedup lives at moderate accuracy, not asymptotically; and at fixed the advantage requires . Note what cancels — , and the -exponent all drop out, leaving only against .
The formalization. Because the oracle and the cost exponent are parameters, the classical and quantum rates are one theorem evaluated twice rather than two proofs. This mission is unusual in that its frontier is already closed: every node arrives with a machine-checked proof, transplanted from a green build. What it offers the platform is a reusable, fully-proved layer for first-order convergence analysis — function classes, cost models, a one-step descent recursion, accumulation laws including a stopped-time version, and the SPIDER schedule — on which further rates can be built by instantiation.
The apparent difficulty is not where a newcomer expects. Deriving a rate from the one-step recursion is routine telescoping. What is delicate is keeping the constants honest while the oracle varies: a rate proof that quietly assumes an exact gradient, or a global lower bound on , will produce the right-looking exponent from the wrong hypotheses.
Two specific places carry real content. Evaluating an error recursion at a random return time breaks the unconditional variance bound, because conditioning on destroys independence; the stopped-time accumulation law is what repairs it. And reproducing a published constant exactly — rather than up to — is what certifies that the parametrized machinery has not silently degraded the bound it generalizes.
Smoothness is QuadUpper on an explicitly supplied g; no differentiability or convexity is assumed anywhere, and the only lower-bound hypothesis is at the terminal iterate rather than globally. Cost models are an inductive family with a power-law member, so the classical and quantum instances are and of one definition. Half-integer powers are written with Real.sqrt, so no real exponentiation appears in any statement. Stochastic results use a genuine Filtration and a conditional oracle contract; the tower property is derived, not assumed.
Two honesty notes. Several statements carry hypotheses that Lean marks unused; these are recorded as such in the individual nodes rather than presented as load-bearing. And the library records a discrepancy in Sidford--Zhang's Algorithm 7 parameter block, documented in its own STATUS notes; the formalization follows the corrected parameters.
lean-optrates, github.com/shiy1022/lean-optrates at commit 4c0b8498, Apache-2.0, by Yueheng Shi. The platform copy renames the root namespace OptRates to ShiOptRates; no statement or proof is otherwise altered.Discrepancy theory asks how unbalanced a two-coloring of a combinatorial structure must be in the worst case. Concretely: given sets over an -element ground set, color each element or so that every set is as close to balanced as possible. The question is classical (Beck–Fiala 1981; Spencer 1985) and the answer for general (dense) set systems is one of the sharpest gaps between a naive probabilistic bound and the truth known in combinatorics: assigning colors uniformly at random only guarantees discrepancy , yet a coloring with discrepancy always exists — the logarithmic factor is an artifact of the naive argument, not of the problem. This mission formalizes that removal, following T. Rothvoß's lecture-note exposition of J. Spencer's entropy method (MIT 18.095, "Discrepancy theory"), the standard modern presentation of the technique (see also Matoušek, Geometric Discrepancy, Ch. 4). The entropy method is the ancestor of the whole "partial coloring" family of arguments used throughout discrepancy theory and combinatorial algorithm design, so a machine-checked account of its base case is reusable well beyond this one theorem.
Fix and an matrix with entries in , thought of as the incidence matrix of sets over an -element ground set: iff element lies in set . A coloring is a map , and the discrepancy of row under is , the signed imbalance of set . The discrepancy of the matrix is the value achieved by the best coloring, minimizing the worst row.
The entropy method bounds this via the partial coloring lemma: rather than coloring all elements at once, one repeatedly colors a constant fraction of the currently uncolored elements while keeping every row's contribution small, then recurses on what remains. Each round is itself produced by an entropy/pigeonhole argument: quantize each row's signed sum (under a uniformly random coloring) into "shells" of width (where is the number of active elements); a short computation shows this quantization carries very little Shannon entropy once the shell width exceeds a threshold; subadditivity of entropy across the rows then bounds the joint quantization entropy, which by pigeonhole forces an exponentially large set of colorings landing in the same joint shell; Kleitman's theorem on the diameter of a large subset of the Hamming cube then extracts two such colorings that are far apart in Hamming distance, and their difference is the sought partial coloring.
Goal.
This is the qualitative, constant-suppressed form of Spencer's theorem: it asserts discrepancy with a single universal constant, and deliberately leaves that constant unspecified. This is the right goal for this mission because it is the weakest statement that is still stable: any future improvement to the constant (down to Spencer's sharp , or beyond) refines this theorem rather than invalidating it.
The removal of the factor is the entire content of Spencer's theorem: it is what separates discrepancy theory from a corollary of concentration inequalities, and the partial-coloring/entropy method it introduced underlies later results throughout the field (Beck–Fiala-type bounds, the Komlós conjecture literature, and constructive/algorithmic discrepancy minimization). Formalizing it is formalizing the base case that every later partial-coloring argument specializes.
This mission's goal theorem, spencer_discrepancy_sqrt_n_bound, is already proved (zero sorrys), by a from-scratch entropy-method development: the per-row shell-entropy bound, the joint pigeonhole-and-Kleitman assembly for one round, and the outer geometric iteration and induction combining rounds into a full coloring. What remains open in this mission is shannonEntropy_shellFin_le (Lemma 9 in Rothvoß's notes) — the per-row entropy bound is currently imported as an assumption by the one-round lemma lemma8_partial_coloring_round, which is therefore only conditionally proved pending it. A separate, harder mission on this platform (Komlos.spencer_six_deviations) targets Spencer's sharp constant via a tighter, non-standard numeric derivation; that is a distinct, substantially harder target and this mission does not duplicate it.
The obvious argument is: fix a target bound , use a Chernoff/Hoeffding bound to show each row fails with probability at most , union-bound over the rows, and take a coloring outside the bad event. This works to prove a single good coloring exists — but it is not strong enough to survive being iterated to remove the entire uncolored set, because a per-row union bound loses a factor of that a fixed cannot always absorb once the active column count is close to : for the scaling family where the row count and the active set shrink together, the naive union bound's failure probability grows linearly in , not exponentially, exactly canceling the exponential decay one is trying to exploit. The fix is to bound the joint entropy of all rows' quantizations at once (subadditivity of Shannon entropy), rather than union-bounding row-by-row failure events; this is genuinely a different technique, not a tightening of the same one, and it is the reason the entropy method is presented as its own tool rather than a Chernoff-bound corollary.
Matrices are Fin n → Fin n → ℝ with an explicit ∀ i j, A i j = 0 ∨ A i j = 1 hypothesis; colorings are represented two ways in this development — Fin m → Bool internally (via the platform definition RSign converting to ) during the entropy/Kleitman argument, and directly as Fin n → ℝ constrained to pointwise in the goal theorem's statement, matching the usual -coloring convention. The row-sum shell quantization is the platform definitions rowSumB, shellIdx, shellFin (an integer-valued "round to nearest shell" construction, packaged into a fixed Fin (2m+3) type for entropy purposes). The active column set during the outer iteration is tracked as a shrinking Finset (Fin n) of the original index type throughout, rather than moving between different Fin m types round to round, which keeps the induction free of type-level bookkeeping.
Reusable, already-Proved infrastructure this development builds on: shannonEntropy_pi_le (subadditivity across independent rows), shannonEntropy_pigeonhole, choose_sum_le_exp_mul_binEntropy, and kleitman_diameter, all already Proved on the platform independent of this mission. The one genuinely open piece — and the mission's standing invitation — is shannonEntropy_shellFin_le (Lemma 9): a self-contained Shannon-entropy computation about the shellFin quantization that does not depend on anything else in this mission and can be attempted independently.
Quantum low-density parity-check codes encode quantum information using sparse parity constraints. A standard way to construct them is to translate binary chain complexes into Calderbank--Shor--Steane codes and to combine complexes by tensor product. Homology identifies the logical operators of the resulting code, while the smallest Hamming weight of a nontrivial homology class controls one of its distances. Determining how this distance behaves under a tensor product is therefore a basic structural question, not merely a parameter calculation.
Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an arbitrary finite binary chain complex and the other is the one-complex induced by a binary matrix. Their paper was published as “Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,” Physical Review Letters 122, 230501 (2019). Its main distance result is Eq. (13) in the arXiv version: for this particular tensor factor, the usual product upper bound is always exact. The result extends the familiar two-complex setting of quantum hypergraph-product codes to the local structure occurring in complexes of any dimension.
A based binary chain complex consists of finite-dimensional vector spaces over , each equipped with a specified coordinate basis, and linear boundary maps
such that . Its degree- homology is . The homological distance is measured in the chosen basis:
Following the paper, the minimum of an empty set is . Thus when is trivial.
The endpoint convention is also the one stated explicitly after Eq. (1). For an -complex, is the zero matrix and is the zero matrix. Consequently
and
For an binary matrix , the one-complex has in degree one, in degree zero, and boundary . Its two distances are
and
In particular, unless has full row rank, in which case . The degree- chain group of is
with the standard tensor-product boundary. Over the usual sign in that boundary has no effect.
The first milestone is Eq. (11) for two arbitrary finite-length based binary chain complexes:
Let and . The second milestone is Theorem 1, including both of its cases:
and
The goal is Eq. (13):
No full-rank hypothesis is imposed on .
The equality determines the product distance exactly from four component distances. General tensor-product arguments immediately provide the upper bound, but an exact formula requires ruling out lower-weight homology classes that mix the two direct-sum blocks. Once established, the formula can be applied repeatedly to tensor products of one-complexes, which is the step used in the paper to obtain higher-dimensional quantum hypergraph-product code families and to compute their distances.
For formalization, the mission contributes reusable definitions of finite based binary chain data, homological distance valued in , the one-complex of a binary matrix, and the relevant tensor-product boundary maps. Mathlib contains Hamming weight and general homological-algebra infrastructure, while QECLean contains a closely related based length-three homological-code interface. Neither the selected Mathlib environment nor the inspected QECLean development currently supplies this rank-sensitive exact distance theorem.
The central issue is that Hamming weight depends on the chosen bases and is not preserved by arbitrary homological isomorphisms. A Künneth isomorphism describes the product homology and readily produces low-weight representatives, which is enough for the upper bound, but it does not by itself exclude a still lighter representative obtained by cancellation between the two tensor blocks. The lower bound must also remain valid at the endpoints of the complex and in singular cases where one or more homology groups vanish and the relevant distance is .
The theorem cannot be reduced to a dimension calculation. It must reason about supports and Hamming weights of based representatives while respecting the quotient by boundaries, and it must cover both and .
The Lean development works over ZMod 2. A finite basis in degree is
represented by Fin (dimension i), and a chain group is the function space
from that coordinate type to ZMod 2. BasedBinaryChainComplex stores the
dimension and boundary in every nonnegative degree, the chain condition, and a
finite length above which all dimensions are zero. Thus the first milestone
quantifies over genuinely arbitrary finite lengths for both and
, rather than over a local window or a one-complex specialization.
If the stored length is , the zero-dimensional source in degree
makes the unique zero map, just as the
zero-dimensional target below degree zero makes
the unique zero map. Hence both singular endpoint
cases in Eqs. (1) and (4) are represented directly.
Distances use WithTop ℕ. Their definitions are actual minima of Hamming
weights of nontrivial representatives, with ⊤ produced by the empty-set
case; infinite distance is not an extra hypothesis or a separately hard-coded
branch. Coordinate types may be empty, which covers missing endpoint blocks.
The binary matrix is represented as a linear map between two finite based
function spaces. Its row and column coordinate types need not be nonempty,
and no injectivity or surjectivity assumption is added.
The degree- product group is indexed by the disjoint union of all coordinate products for . Consequently its Hamming norm is the sum of the weights of all tensor-degree blocks. The product boundary is the standard signed tensor boundary; its sign disappears over . A formal proof verifies that every pair of consecutive product boundaries composes to zero; the cancellation of the two mixed terms uses characteristic two. Thus the product distance is taken from an actual chain complex, rather than from unrelated adjacent linear maps. A basis-free tensor product or an abstract homology group alone is insufficient for the target, because either would discard the weight data on which the statement depends. The mission does not formalize the asymptotic code-family construction later in the paper, the transposed cohomological distance, or the CSS-code parameter translation. Those are natural downstream missions; they should reuse rather than alter the present based-chain definitions.
Computability theory studies which questions admit algorithms and how the unsolvable questions compare with one another. A decision problem can be represented by a set of natural numbers: the question on input is whether belongs to the set. Even when there is no algorithm that always answers this question, there may be an algorithm that eventually recognizes every positive instance. Understanding the relative difficulty of such problems is the setting of the Friedberg–Muchnik theorem.
The original paper by Richard M. Friedberg appeared in 1957 under the title Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944). It supplies the historical paper source for this formalization. A. A. Muchnik's independent contribution appeared in Russian in 1956. Friedberg, PNAS 43(2), 236–238; Muchnik, Math-Net bibliography, 1956 entry.
A set is computably enumerable, abbreviated c.e., if membership has a semidecision procedure: on input , the procedure halts exactly when . The older terminology is recursively enumerable, abbreviated r.e. The Lean predicate CEnumerable A uses Mathlib's REPred for this property. A computable set has a decision procedure that terminates on every input and answers membership correctly; this is expressed separately by ComputableSet A using ComputablePred.
For each set , define its characteristic function by
An oracle for answers requests for this function's values. It always supplies an answer, even if membership in cannot be computed without an oracle. The declaration setOracle A represents this total function inside Mathlib's type of partial functions from natural numbers to natural numbers.
Write when an algorithm with access to the membership oracle for computes on every input. This is Turing reducibility, expressed by SetTuringReducible A B. The algorithm may make several queries, with later queries depending on earlier answers. Incomparability requires both and ; it is stronger than saying the two sets merely have different degrees. These conventions specify the mathematical reading of the supplied Lean definitions.
The goal is the following unconditional existence statement:
Its Lean name is Computability.friedberg_muchnik. No enumeration, pair of sets, or oracle program is supplied as a hypothesis. Both sets must be obtained as witnesses to the conclusion. The statement matches Theorem 26.2 in Arnold W. Miller's Lecture notes in Recursion Theory, Section 26, with the theorem on page 51 and its proof on pages 51–54. Miller, December 3, 2008 version.
The target establishes that the c.e. problems have incomparable levels of computational difficulty. Its witnesses cannot be computable: a computable membership procedure would also work in the presence of any other oracle simply by making no queries, contradicting the required nonreducibility. The stronger historical consequence is a positive solution of Post's problem: a c.e. degree can lie strictly between the computable degree and the halting degree. Miller records this consequence separately as Corollary 26.3 on page 54. Miller, Section 26.
The mathematical theorem is established; the work requested here is its Lean 4 formalization. A completed development must construct witnesses, prove their computable enumerability, and exclude oracle computations in each direction using Mathlib's actual reducibility relation. The provided goal currently ends in sorry. Successful compilation of this statement checks its formulation and imports; it does not constitute a proof of the existence result.
The main obstacle is preserving decisions about oracle computations while both sets are still being enumerated. An additional element in one set can change an oracle answer used by an earlier computation, undermining the attempt to separate the other set from it. There are infinitely many candidate programs in both directions. Thus a formal treatment has to justify the eventual stability of the relevant computations as well as the effectiveness of the enumeration. This is the setting of the finite injury argument developed in Miller's proof of Theorem 26.2. Miller, pages 51–54.
The sets are arbitrary Set ℕ, including the natural number zero in their ambient domain. The oracle answers use natural numbers, with one for membership and zero for nonmembership. Classical reasoning is used to define the oracle for an arbitrary set; it supplies no assertion that this function is computable. Each oracle is nevertheless total. Replacing it with a partial membership recognizer would change the meaning of the target.
The foundation consists of Mathlib.Computability.RE and Mathlib.Computability.TuringDegree, together with the supplied definitions in namespace Computability. SetTuringEquivalent records reducibility in both directions. degreeOfSet maps a characteristic-function oracle to its Turing degree, and CEnumerableDegree says that a degree has a c.e. representative. These additional definitions are retained as useful interfaces, while the root theorem itself is expressed directly with sets and TuringIncomparable.
A complete proof will need representations of effective finite stages and oracle computations, and lemmas relating those representations to the imported predicates. Such infrastructure can support later formalizations involving oracle use, computable enumerations, and priority constructions. Contributions should establish these connections with Mathlib's definitions and finish the unconditional target. The theorem must not be replaced by mere degree inequality, weakened reducibility, or a conditional assertion that assumes the required incomparable sets already exist.
The Kerr metric (Kerr, 1963) is the exact solution of the vacuum Einstein equations that describes the exterior gravitational field of a rotating mass. It is the working model for astrophysical black holes: gravitational-wave templates, black-hole imaging and the classification results of the uniqueness theorems all take it as their starting point. Its form in the coordinates of Boyer and Lindquist (1967) is the one found in every textbook, and the statement that this line element has vanishing Ricci tensor is the single most-cited computation of the subject. That computation is long, it is almost never printed, and in practice it is trusted because computer-algebra systems agree on it. The parent project of this mission builds a certified-discovery pipeline for exact solutions of Einstein's equations in which a symbolic verifier is the oracle; this mission asks for the Kerr instance of that oracle's verdict to be re-established inside a proof assistant, so that the pipeline's benchmark result rests on a kernel-checked proof rather than on a simplification routine.
Timeline: Kerr (1963) found the metric in Kerr-Schild and in his original coordinates; Boyer and Lindquist (1967) introduced the coordinates in which the metric below is written and described its maximal analytic extension; Carter (1968) established the separability structure that underlies the closed-form inverse. None of these results has, to the authors' knowledge, a machine-checked proof.
Fix real parameters and . A point of is written ; in Lean it is a function Pt := Fin 4 → ℝ. Write , and
The Boyer-Lindquist Kerr metric is the symmetric matrix of functions
with all other entries zero (signature , ). Its closed-form inverse has , and a block with denominator . The regular coordinate domain is
For any matrix of functions with candidate inverse , the coordinate partial derivative is the one-variable derivative at of the slice , and the coordinate Christoffel symbols and coordinate Ricci tensor are
These four definitions (pd, christoffel, ricci, ricciOf) form the definition bundle KerrBL_CoordGeometry; the metric, its inverse and the regular domain form KerrBL_Kerr_Metric.
KerrBL.vacuum_Kerr)For all real and every with :
The goal deliberately bundles the inverse identity and the two differentiability clauses with Ricci-flatness. Without the first, ricciOf g ĝ with a wrong could vanish trivially; without the other two, the derivative in the definition of could be Mathlib's default value at a non-differentiable slice. With them, the last clause is a statement about the genuine coordinate Ricci tensor.
The milestones follow the three layers of the proof: (I) the inverse identity; (II) the bridge from the generic definitions to explicit closed forms, through derivative certification of the metric, the Christoffel bridge, derivative certification of the generic Christoffel symbols, and the Ricci bridge ; (III) the vanishing of the explicit expression for each of the eight components that are not structurally zero, as rational identities in the seven variables under , , , and finally the vanishing of all sixteen generic components.
The result itself is classical: the Boyer-Lindquist Kerr family is a vacuum solution wherever the coordinates are regular. What the mission adds is a proof in which the trusted base is explicit and small: a 45-line generic layer defining , and , and the transcription of five metric components from a hash-locked source file, with source-lock lemmas proving that the compact definitions equal the transcriptions. Everything else, including roughly 120 kB of generated closed forms, is bridged by proof; a wrong closed form can make a bridge theorem unprovable but never a false theorem provable. The generic layer and the bridge pattern are reusable for any coordinate metric in four dimensions, and the pattern of certifying a computer-algebra derivation through polynomial witnesses checked by linear_combination is reusable for any rational-function identity.
Status: the theorem is proved in the classical sense since 1963 and verified by every computer-algebra system; the machine-checked coordinate proof is what this mission records. At launch every node of the mission carries an accepted proof.
The obvious argument is to compute. The difficulty is size and control, not ideas. The Ricci components of Kerr are rational functions whose numerators have up to a few hundred monomials in seven variables; a normalisation tactic applied to the raw expression does not terminate in practice, and a naive -based unfolding of the double sums over produces terms whose elaboration alone exceeds the server budget. The proof therefore has to be organised: opaque atoms for and so that denominators are monomials, per-term clearing lemmas over a common denominator, and a single polynomial identity per component certified by explicit quotient witnesses of the relations , , . Mathlib's derivative also needs care: deriv returns where a function is not differentiable, so every derivative used in the Ricci formula must be accompanied by a HasDerivAt witness, and the differentiability of the generic Christoffel symbols has to be transferred from their closed forms by a locality argument on the open regular domain.
The Lean representation commits to the following. Points are Fin 4 → ℝ with , , , ; there is no manifold, no chart, no periodicity of and no range restriction on . Derivatives are Mathlib's deriv of coordinate slices. The candidate inverse is data; its correctness is a theorem. The parameters are arbitrary reals: the mission proves Ricci-flatness of the Boyer-Lindquist Kerr family on the regular coordinate domain used by the formalization, not a global Lorentzian-manifold theorem and not a statement restricted to the black-hole regime , . The axis is excluded (the inverse carries ) although the metric is smooth there; the loci and are excluded. Nothing is asserted about signature, uniqueness, symmetry of (all sixteen components are proved separately) or any coordinate-independent curvature quantity. A trivialising formalization is ruled out by the goal's first clause: the Ricci tensor of the specification layer takes the inverse as an argument, and the goal certifies that argument.
Independent blind read-back of the definitions and main statements, performed by a separate agent that saw only the Lean text, returned the following honest statement, recorded here verbatim: "For every pair of real numbers , and every point at which , and , all sixteen numbers obtained by evaluating the explicit coordinate formula [...] vanish, where is the explicitly transcribed Boyer-Lindquist Kerr component matrix, is an explicitly transcribed matrix that (by ginv_mul_g_Kerr, under the same hypothesis) satisfies at that point, and is Mathlib's one-variable deriv of the coordinate slice." The two should-fix findings of that read-back (inverse coupling; junk derivative values) are addressed by the first three clauses of the goal.
Infrastructure: three definition bundles (KerrBL_CoordGeometry, hand-written; KerrBL_Kerr_Metric, generated from the source file and human-auditable; KerrBL_Kerr_ClosedForms, generated and untrusted). Reusable beyond the mission: the generic layer, the locality lemma, and the bridge pattern. Natural extensions welcome after release: the two-sided inverse, the reduction to Schwarzschild, and curvature invariants such as the Kretschmann scalar.
Classical Eilenberg correspondence theorems connect algebraic descriptions of finite-state behavior with language-theoretic closure principles. The version developed by Juan Climent Vidal and Enric Cosme Llópez replaces one-sorted monoids by many-sorted algebras, so that operations may accept arguments of several prescribed sorts and return a value of another sort. This is the natural algebraic setting for typed term languages: a signature records the permitted input and output sorts of each operation, and a language is a family of sets indexed by sorts. The paper proves that two ways of organizing finite-state behavior—through finite-index congruences and through regular languages—determine the same ordered structure. The source is the final section of Climent Vidal and Cosme Llópez, Eilenberg theorems for many-sorted formations, published in the Houston Journal of Mathematics 45(2), 2019.
The companion manuscript A Kleene theorem for free many-sorted algebras develops the free-term and recognizability infrastructure used by this formalization. It supplies a concrete Lean representation of sorted signatures, free algebras, homomorphisms, terms, and finite many-sorted carriers. The present mission begins from that reusable core and formalizes the formation-level theorem of the HJM paper, rather than repeating the already completed Kleene development.
Fix a finite type of sorts and an -sorted signature . For an -sorted set , write for the free -algebra on . A congruence on a many-sorted algebra is a family of equivalence relations , one on each carrier sort, compatible with every basic operation. Its index is finite when the entire sorted quotient family
is finite. A sorted language is -saturated when membership in is constant on every -class. The syntactic congruence is the greatest algebra congruence that saturates , and is regular when has finite index.
A finite-index congruence formation selects, for every variable family , a nonempty filter of finite-index congruences on . The selection is closed under intersections, upward inclusion, and pullback along homomorphisms whose composite with the relevant quotient projection is surjective at every sort.
A regular-language formation selects regular languages in each . It contains every language saturated by the universal congruence; whenever it contains every language saturated by ; and it satisfies the corresponding pullback-saturation condition for quotient-surjective homomorphisms.
The two constructions are
and
The capstone is the paper's final formation theorem: the ordered sets of finite-index congruence formations and regular-language formations are order-isomorphic, with the isomorphism fixed to be exactly the two displayed constructions.
The milestones establish the universal property of the syntactic congruence, closure of finite-index congruences under the filter operations, the well-definedness of each construction, and the two recovery identities
These identities determine the inverse maps and prevent the goal from being satisfied by an unrelated abstract order equivalence.
The theorem packages a family of finite quotients and a family of regular languages as interchangeable data. On the algebraic side, closure is expressed by filters of congruences and quotient-surjective pullbacks. On the language side, the same information is expressed through saturation by syntactic congruences. The result therefore gives a systematic translation between quotient-based and language-based classifications in a typed, many-sorted setting.
Formalizing the theorem adds congruence, quotient-index, saturation, syntactic-congruence, and formation interfaces to the existing free many-sorted algebra library. These components are reusable for future formalizations of recognizability, Myhill–Nerode principles, finite algebra formations, and varieties or pseudovarieties of typed algebras. The mathematical theorem is already proved in the cited 2019 paper; the remaining task is to produce machine-checked Lean proofs of the source-faithful statements.
The two maps are simple to write down but their inverse laws are not pointwise tautologies. A finite-index congruence must be reconstructed from the family of all languages it saturates, and a language formation must be reconstructed from all selected finite-index congruences. In the many-sorted case, finiteness applies to the entire quotient family, including its support across sorts, and intersections and pullbacks must preserve this global condition. The quotient-surjectivity premise is also essential: replacing it by ordinary surjectivity of the original homomorphism would change the formation axiom.
The syntactic congruence creates a second layer of care. It must be characterized as the greatest compatible sorted equivalence saturating a language, not merely as the kernel of the language's characteristic function, which need not itself respect the algebra operations. Thus an argument that treats saturation as an arbitrary set-theoretic equivalence misses the algebraic compatibility required by the theorem.
The Lean development uses the existing MSKleene representation of sorted sets, signatures, argument tuples, algebras, homomorphisms, terms, and free algebras. Congruences are sort-indexed setoids with explicit compatibility for every signature operation. Their order is inclusion of relations. Intersection and the universal congruence are concrete constructions, while pullback is defined along an algebra homomorphism.
Finite index is represented by finiteness of the sigma-type of all quotient carriers, matching the paper's finite sorted-set convention; it is not weakened to separate finiteness of each inhabited component. The sort type is assumed finite in the finite-index filter and formation correspondence theorems, as required in the final section of the source. Languages are arbitrary sorted subsets of free term algebras, including empty components. No nonemptiness assumption on variable carriers or algebra sorts is added.
The syntactic congruence is defined internally as the supremum-style least upper bound of all congruences saturating a language, rather than postulated together with its universal property. The formation structures contain only the source closure axioms. In particular, neither correspondence map nor either inverse identity is stored as a structure field; doing so would trivialize the capstone. Contributions are welcome on the foundational universal-property and finite-index lemmas, the two formation constructors, and the recovery identities that assemble into the final order isomorphism.
The third mission in the series formalizing Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; pi.math.cornell.edu/~hatcher/AT/AT.pdf) turns to the second main topic of Chapter 1, covering spaces (Section 1.3, pp. 56–78). The first mission used the covering to compute , and the second proved van Kampen's theorem. This mission develops the general theory of covering spaces of a fixed space : the lifting properties (pp. 60–62), the classification of connected covering spaces by subgroups of (pp. 63–68), and deck transformations and group actions (pp. 70–72). Its goal is the classification theorem (Theorem 1.38, p. 67), Hatcher's "Galois correspondence" between path-connected covering spaces of and subgroups of , together with its companions Proposition 1.39 (deck groups and normal covers) and Proposition 1.40 (covering space actions and orbit spaces).
All statements live in the Lean namespace Hatcher used by the earlier missions.
A covering space of (p. 56) is a space with a map such that every has an open neighborhood whose preimage is a disjoint union of open sets each mapped homeomorphically onto ; may be empty, so need not be surjective. This is Mathlib's IsCoveringMap. For a covering space with basepoints we write
for the induced homomorphism (Hatcher.coverHom) and its image (Hatcher.coverSubgroup).
is semilocally simply-connected (p. 63, Hatcher.IsSemilocallySimplyConnected) if each has a neighborhood such that every loop at contained in is null-homotopic in . The bundle Hatcher_Covering also fixes: the structure CoveringSpace X (a total space and a covering map ) and its pointed version PointedCover X x₀ (with and associated subgroup PointedCover.subgroup); isomorphism of covering spaces (p. 67), a homeomorphism with , with or without preservation of basepoints (IsIsomorphic, IsPointedIsomorphic); the deck transformation group (p. 70, deckGroup), the self-homeomorphisms of commuting with ; normal covering spaces (p. 70, IsNormalCover); Hatcher's condition for a covering space action of a group on (p. 72, IsCoveringSpaceAction); and the orbit space with its quotient map (OrbitSpace, orbitProj).
Let be path-connected, locally path-connected and semilocally simply-connected, with basepoint . Then:
Together these say that is a bijection from basepoint-preserving isomorphism classes of path-connected covering spaces to subgroups, inducing a bijection from isomorphism classes to conjugacy classes of subgroups.
The result itself. The classification theorem is the central structural fact about covering spaces: the connected coverings of are "the same as" the subgroups of , with the universal cover corresponding to the trivial subgroup and normal coverings to normal subgroups. Proposition 1.40 is the standard method for computing fundamental groups of orbit spaces (, , lens spaces) and is used throughout Hatcher's later chapters.
Formalizing it. Mathlib (at this environment's revision) already has the lifting theory for covering maps: path and homotopy lifting (IsCoveringMap.liftPath, liftHomotopy), the monodromy action (IsCoveringMap.monodromy), the injectivity of (injective_path_homotopic_map, cited there as Proposition 1.31), the unique-lifting statement (IsCoveringMap.eq_of_comp_eq), and the lifting criterion itself (existsUnique_continuousMap_lifts_of_range_le, cited as Proposition 1.33). For quotient maps by a free properly discontinuous action it has IsQuotientCoveringMap, with the homomorphism and its kernel and surjectivity. Milestones 1, 4, 5 and 16 are therefore expected to be short reductions to Mathlib, and Mathlib's quotient-covering theory should carry most of milestones 14–15. Mathlib has no notion of semilocal simple connectivity, no construction of the universal cover or of the coverings , no classification theorem, and no deck transformation groups or normal coverings; milestones 6–13 and the goal are new.
The heart of the mission is the construction of the universal cover (pp. 63–65): the points are homotopy classes of paths from , the topology is generated by the sets for in the basis of path-connected open sets on which dies, and one must verify that this is a topology basis, that is a covering map, and that the result is simply connected. Proposition 1.36 then passes to a quotient by and checks that the projection remains a covering map. Both are elementary but long, and formalizing them requires a systematic treatment of path homotopy classes as points of a space.
Propositions 1.37 and 1.39 follow from the lifting criterion and unique lifting; the deck-group homomorphism in 1.39(b) sends a loop in to the deck transformation produced by the lifting criterion, and its kernel is computed by Proposition 1.31. Proposition 1.40(a) needs the quotient topology on and the evenly covered neighborhoods from condition ; part (b) is the observation that a deck transformation of a path-connected cover is determined by one value. Milestone 3 is orbit–stabilizer for the monodromy action.
CoveringSpace X bundles a total space in the same universe as with a covering map; the classification quantifies over covering spaces in this sense. Since the universal cover and the coverings are constructed from paths in , they live in that universe, so nothing is lost.MulAut.conj; "number of sheets equals the index" is stated as a bijection with the coset space.Normal instance in the statement; the final clause of 1.39 and 1.40(b) are stated as the existence of group isomorphisms, the latter with its action on prescribed.MulAction.orbitRel.Quotient with the quotient topology.Contributions welcome: a reusable construction of the space of path classes with its topology, the covering , and the deck-group homomorphism; the short reductions to Mathlib for Propositions 1.31, 1.33 and 1.34 are good first contributions.
Mathlib/Topology/Covering/Basic.lean (covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Basic.leanMathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting, monodromy, the lifting criterion). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.leanMathlib/Topology/Covering/Quotient.lean (quotient covering maps for group actions). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.leanOnce is known, the next question in Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; pi.math.cornell.edu/~hatcher/AT/AT.pdf) is how to compute fundamental groups of spaces built from pieces. Section 1.2 answers this with van Kampen's theorem (Theorem 1.20, p. 43): if a space is covered by open sets with a common basepoint and path-connected intersections, its fundamental group is the free product of the fundamental groups of the pieces, modulo relations coming from the intersections. It is the main computational tool of Chapter 1: it gives the fundamental groups of wedges of circles, graphs, surfaces, and every CW complex from its 2-skeleton (Propositions 1.26–1.28), and it underlies the classification of covering spaces in Section 1.3.
This is the second mission in the series formalizing Hatcher's book. The first mission established the covering-space lifting properties and in the Lean namespace Hatcher; this one covers the subsection "The van Kampen Theorem" of Section 1.2 (pp. 41–47) together with its warm-up Lemma 1.15 and Proposition 1.14 from Section 1.1 (p. 35).
Let be a topological space with a basepoint . A path is a continuous map , a loop at is a path with both endpoints , and is the group of homotopy classes of loops at under concatenation. A continuous map with induces a homomorphism , .
Let be a family of subsets of , each containing , with the subspace topology; write for . The inclusions induce
which are Hatcher.inclHom, and the inclusions and induce
which are Hatcher.interHomLeft and Hatcher.interHomRight.
The free product of a family of groups is the group of reduced words in the (Hatcher, pp. 41–42); in Lean it is Mathlib's Monoid.CoprodI, here Hatcher.FreeProd. Its universal property extends the to a single homomorphism
Hatcher.vanKampenHom. Since (both are induced by ), the elements
lie in the kernel of . Let be the normal subgroup generated by all of them, Hatcher.vanKampenNormal.
If is the union of path-connected open sets each containing , each is path-connected, and each is path-connected, then
Hence induces an isomorphism .
The result itself. Van Kampen's theorem is the gluing law for . With it Hatcher computes of wedge sums (free products), of graphs (free groups), of the closed orientable surfaces (Example 1.26), and shows that attaching -cells kills exactly the attaching loops (Proposition 1.26), so that every group is a fundamental group (Corollary 1.28). The surjectivity half alone gives Proposition 1.14, that spheres of dimension at least two are simply connected, and hence that is not homeomorphic to for (Corollary 1.16).
Formalizing it. Mathlib has the fundamental groupoid and fundamental group, induced homomorphisms (FundamentalGroup.map), free products of groups (Monoid.CoprodI) with their universal property, normal closures, and quotient groups. It has no version of van Kampen's theorem for topological spaces (its CategoryTheory/Limits/VanKampen concerns colimits in categories, not fundamental groups), and no computation of for ; on the platform, however, the theorem SP4Mission.sphere_simplyConnected (already proved in this environment) states that the unit sphere of is simply connected for , which is Proposition 1.14 with shifted indexing, so that milestone can be closed by a one-line reduction. The mission supplies the statements in Hatcher's form, on Mathlib's , so that later missions (covering spaces, cell complexes) can use them directly.
Surjectivity is a compactness argument: subdivide so each piece of the loop lies in one , then use path-connectedness of the intersections to connect the subdivision points back to . The formal difficulty is bookkeeping: producing the subdivision from an open cover of (Mathlib's exists_monotone_Icc_subset_open_cover_unitInterval is the tool) and showing the reparametrised concatenation is homotopic to the original loop.
The kernel computation is the hard part. Hatcher's proof takes a homotopy between two factorizations, subdivides the square into rectangles each mapped into a single , perturbs the grid so at most three rectangles meet at a corner (this is where triple intersections enter), and then shows that moving the loop across one rectangle at a time changes the factorization only by the two elementary moves that hold in . Every step is elementary, but the induction over the grid is long, and each elementary move requires an explicit path-homotopy in a subspace. The naive idea of proving by an induction on word length does not work: the relation between two factorizations of the same loop is only visible through a homotopy in , not through the words.
Proposition 1.14 is easy given Lemma 1.15 but requires exhibiting the cover of by two complements of antipodal points, showing each is simply connected (homeomorphic to via stereographic projection, which Mathlib has as stereographic), and showing their intersection is path-connected when .
Set X with the subspace topology, and is Mathlib's FundamentalGroup ↥(A α) ⟨x₀, _⟩. Hypotheses are stated explicitly on each theorem: IsOpen, IsPathConnected, ⋃ α, A α = Set.univ, and path-connectedness of pairwise (and, where Hatcher requires it, triple) intersections.List of loops, each tagged with the index of the piece it lies in, concatenated right-to-left with the constant loop as empty product (Hatcher.loopProd). Any bracketing gives the same homotopy class.Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1, and "" is Mathlib's SimplyConnectedSpace (path-connected with trivial fundamental group), which is what Hatcher means since is path-connected.Contributions welcome: the subdivision lemma for loops in an open cover, a reusable treatment of factorizations and their elementary moves, and the two-set special case as a corollary.
Mathlib/GroupTheory/CoprodI.lean (free products of groups). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/GroupTheory/CoprodI.leanMathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (fundamental group and induced homomorphisms). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.leanReflection positivity and infrared bounds form a standard finite-volume route from the geometry of a lattice reflection to quantitative control of long wavelength fluctuations. In the classical argument, reflection positivity supplies a Cauchy--Schwarz inequality for reflected observables, while Fourier diagonalization of the lattice Laplacian identifies the free covariance used in the infrared comparison. These ingredients underlie rigorous results on continuous-symmetry lattice systems in Fröhlich, Simon, and Spencer's development of infrared bounds and spontaneous symmetry breaking (1976), and the general theory of reflection positivity developed by Fröhlich, Israel, Lieb, and Simon (1978). Related technology appears in Fröhlich and Spencer's treatment of the two-dimensional Abelian spin systems and Coulomb gas (1981).
The analytic and model-specific theorems are substantial, but their finite algebraic interface is sharply separable. This mission isolates that interface so later clock, XY, and Gaussian-domination developments can share one checked notion of reflection, one spectral covariance convention, and one treatment of the constant mode.
Let be a finite set of configurations on one side of a reflection plane. A full split configuration is a pair , and reflection exchanges its two entries. A plus-half observable is a function lifted to through the first coordinate. Its reflected copy therefore depends on the second coordinate.
A split weight is specified by a finite feature index , real coefficients , and features :
For a finite family of plus-half observables , the reflected kernel is
A real matrix is positive semidefinite here when it is symmetric and its quadratic form is nonnegative on every real coordinate vector.
The spectral side uses a finite mode set with a distinguished zero mode . An infrared spectrum consists of a function that is nonnegative and vanishes exactly at . For , the free mode covariance is diagonal, equals zero at the constant mode, and has entry
away from zero. Covariance domination is tested only on source vectors whose zero-mode coordinate vanishes. The concrete spectral fixture is the periodic square lattice, with tensor-product discrete Fourier modes and the nearest-neighbor graph Laplacian.
The first target identifies the split reflection pairing with the explicit double sum over the two halves. Under , the resulting reflected kernel must be positive semidefinite:
Every such kernel must satisfy the two-observable chessboard inequality
For every Torus-4 frequency and site , the registered Fourier mode must satisfy the pointwise eigenvalue equation
The eigenvalues must be nonnegative and vanish exactly at the constant mode, and these laws must be packaged as the same spectrum type consumed by the infrared definitions.
The diagonal free covariance must be positive semidefinite for . If an interacting covariance is quadratically dominated by on sources with , then every nonzero Fourier mode must satisfy
Two finite counterfixtures are part of the target. They assert that an arbitrary full-vertex reflected two-point matrix need not be positive semidefinite, and that domination restricted away from the zero mode need not extend to full-matrix domination.
The resulting interface prevents three substitutions that otherwise look
notational but change the theorem. Reflection positivity is tested on
observables supported on one half rather than on an arbitrary matrix indexed
by all vertices. The infrared comparison excludes the constant mode rather
than forcing a fluctuating zero mode below a covariance with zero diagonal.
The graph-Laplacian eigenvalue is connected to the Fourier mode by an explicit
pointwise theorem rather than by assigning a function the name
laplacianEigenvalue.
Several ingredients already have machine-checked Lean proofs in the LeanProofs repository: the finite matrix Cauchy--Schwarz theorem, the Torus-4 DFT diagonalization and zero-mode theorem, and the diagonal free-covariance calculation. This mission reorganizes those results around a corrected consumer boundary and adds the split-half and off-zero adapters. It does not present the finite statements as new mathematics.
The main difficulty is maintaining the correct domain at each interface. A reflection of lattice sites does not by itself imply positive semidefiniteness of a correlation matrix indexed by every site; the tested observables and their support are part of the assertion. Likewise, a free covariance whose constant-mode entry is defined to be zero cannot dominate an arbitrary covariance on all source vectors. Finally, a Fourier multiplier used for a pseudospectral derivative is not automatically the eigenvalue of the nearest-neighbor graph Laplacian. The formal statements must keep these three objects distinct.
All configuration, feature, observable, and mode types are finite. Kernels, weights, coefficients, source vectors, and quadratic forms are real. Complex numbers occur only in the explicit discrete Fourier modes. Reflected pairings are unnormalized finite sums; no partition function or probability measure is introduced. The inverse temperature satisfies . The distinguished zero mode is part of the spectrum interface, and infrared domination is restricted to source vectors that vanish at that coordinate.
The mission does not assert reflection positivity of a clock or XY Gibbs measure, nonnegative Fourier coefficients of a physical cross-bond weight, Gaussian domination, a thermodynamic limit, a Kosterlitz--Thouless transition, or a universal jump. It also does not identify the Torus-4 graph spectrum with the Grid3 pseudospectral multiplier from the Fourier--Hodge packet. Those are separate future missions requiring additional model and analytic input.
The reusable outputs are the split-weight RP interface, the finite positive-semidefinite kernel API, the typed spectrum object, and the zero-mode-restricted domination predicate. Contributions should preserve the explicit half support and zero-mode restrictions; a proof obtained by adding the desired conclusion as a hypothesis is outside scope.
ReflectionPositivityInfraredBound.lean, exact repository
snapshot dbf503b2909cc17787d40a21eb75a0c9354cc6ef.
https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.leanKleene's theorem (Kleene 1956; McNaughton–Yamada 1960) is a cornerstone of formal language theory: over a free monoid, the languages recognized by finite automata are exactly the regular ones — those built from finite languages by union, concatenation, and the Kleene star. Mezei and Wright (1967) lifted recognizability off strings, calling a subset of an arbitrary algebra recognizable when it is the preimage of a subset of a finite algebra under a homomorphism. Replacing strings by terms — finite trees labelled by operation symbols — gives the theory of recognizable tree languages and finite tree automata of Gécseg and Steinby (1984), where the Kleene correspondence reappears with a tree concatenation and an iteration operation in the role of the star.
Many computational structures are inherently many-sorted: typed lambda calculi, structured programming languages, process calculi, XML schemas — data and operations organized into distinct sorts. In the many-sorted setting a signature assigns to each operation symbol the sorts of its arguments and of its value, variables carry sorts, and a language is a sort-indexed family of term sets. The predecessor of this mission, Climent Vidal–Cosme Llópez 2020 (CVCL20), established that recognizability over free many-sorted algebras is preserved — and, where applicable, reflected — by substitution, iteration, quotient, inverse tree-homomorphic image, and direct linear image, via finite-index congruences. What CVCL20 left open is the regular side: whether a natural class of many-sorted regular expressions captures exactly the recognizable languages. This mission closes that gap.
Fix a finite set of sorts . An -sorted set is a family of sets; it is finite when is finite. An -sorted signature assigns to each pair a set of operation symbols of arity and coarity . A -algebra is an -sorted set together with, for each , an operation , where . A homomorphism commutes with all operations sortwise.
The free -algebra on an -sorted set of variables has as its sort- carrier the set of -terms; every -sorted map extends uniquely to a homomorphism . Following automata-theoretic tradition, subsets of are called languages. For a sort , a language is -recognizable when there are a finite -algebra , a homomorphism , and a subset with . Write for the set of all such .
Two operations on languages, both performed sortwise, generate the regular expressions. Given a variable and a language , -substitution replaces, in every term of an input language of sort , each occurrence of independently by a term of . The -iteration is , where and . For a finite -sorted set , the regular signature expands by an empty constant , a binary sum , a unary -iteration for each , and a -substitution operation for each . Its terms are the regular expressions over ; the power algebra carries a canonical -algebra structure, and interpreting a regular expression there yields a language . A language is -regular when for some finite and some regular expression of type ; write .
The statement fixes no automaton model and no normal form for regular expressions: it asserts only that the two classes of languages coincide, at every sort, for every finite , every finite -sorted signature , and every finite -sorted set . It splits into (Corollary 4.8) and (Proposition 4.10).
The result completes the Kleene–Myhill–Nerode correspondence on the side of universal algebra, uniformly over an arbitrary finite many-sorted signature: it names the exact operations — those of , plus empty language, union, sortwise substitution, and sortwise iteration — that generate precisely the finite-state behaviours. Over non-free structures the correspondence is known to fail (recognizable but non-rational subsets of a monoid, Eilenberg 1974), which is what makes the free many-sorted algebra the natural home for an exact statement. The forward direction organizes the regular languages into a -algebra and instantiates the closure properties of CVCL20; the converse gives a constructive, syntactic procedure — from a recognizing homomorphism it builds a regular expression denoting the language — generalizing Lemma 2.5.7 of Gécseg–Steinby, itself descended from McNaughton–Yamada.
The paper is new (June 2026) and has no machine-checked proof. This mission produces the first formalization: a reusable Lean development of finite many-sorted universal algebra — signatures, algebras, free term algebras and their universal property, the Artinian subterm order, power algebras, recognizability, and the substitution/iteration calculus — together with the two inclusions and the state-elimination argument. Everything below the §4 headline results is infrastructure of independent value for many-sorted formal language theory.
The converse inclusion is the substance. The single-sorted proof eliminates automaton states one at a time along a single axis; the naive port to the many-sorted case — fix a linear order on all states and eliminate — loses track of the sort at which each elimination happens and does not terminate cleanly. The argument instead carries a sortwise budget: an -sorted family recording, for each sort , the set of state values still admissible at internal subterms. The induction is on , and each step removes the top state of one chosen sort, so the recursion branches over the sorts whose budget is nonzero and the key identity (Equation (E)) is a union over those sorts. The inductive invariant — the family of auxiliary languages with its budget bookkeeping — is what separates the many-sorted argument from its ancestor; it is also the part Gécseg–Steinby declare "obvious from the construction" and this proof spells out in full (Claims C1–C6).
Proposed Lean representation: a type with [Fintype S]; an -sorted set as S → Type; a signature as a family List S → S → Type with finiteness where the theorems need it; the free algebra as an inductive term type; the power algebra with sort- carrier Set (T_Σ Z s); -recognizability as the existence of a finite -algebra, a homomorphism, and a subset whose sortwise preimage is the language. Committed conventions: finite throughout; finite and finite for the §4 results (so that only finitely many basic terms exist and the budget induction is well-founded); the regular operations are exactly together with the operations of — not an unrestricted Boolean or closure algebra, which would trivialize the statement.
A complete development needs: the many-sorted UA core (sorted sets and maps, signature, algebra, homomorphism, subalgebra, congruence); the free algebra with unique readability (Proposition 3.4) and universal property (Proposition 3.5); the Artinian subterm order (Proposition 3.6); the power algebra; recognizability and -recognizability with the CVCL20 closure results (Propositions 3.29, 3.30, 3.33); the substitution and iteration calculus (Lemmas 3.23, 3.25, 3.28, Corollary 3.17, Lemma 3.18); and the §4 regular-expression layer (Definition 4.1, Proposition 4.3, Corollary 4.4, Definition 4.6). The UA core and the substitution calculus are reusable beyond this mission. Contributions are welcome at every level — the definitions, the closure results, the auxiliary claims C1–C6, and either inclusion.
Searching an unsorted list of items for a single marked entry takes queries classically — there is no way to do better than checking items one at a time. Grover's algorithm (Grover 1996) shows that a quantum computer solves the same problem in queries, a quadratic speedup that applies to any problem expressible as unstructured search over a black-box oracle (this includes brute-forcing NP-complete problems and inverting one-way functions, which is why post-quantum cryptography doubles key lengths to compensate). Unlike Shor's algorithm, Grover's algorithm is provably optimal: Bennett–Bernstein–Brassard–Vazirani (1997) showed queries are necessary for any quantum algorithm solving unstructured search, so the quadratic speedup is the best any quantum algorithm can achieve on this problem.
Model an -item database as the standard basis of (EuclideanSpace ℂ (Fin N)),
with inner product . Fix a marked index
. The algorithm starts in the uniform superposition
a unit vector assigning equal amplitude to every item. Two reflections drive the search:
One Grover iterate is . The algorithm applies some number of times to and measures; a measurement outcome equal to counts as success.
and are each reflections about a unit vector, hence isometries; their composition is therefore norm-preserving on the whole space, not just at — the minimal fact needed for to be a legitimate quantum operation.
The geometric heart of the algorithm (Nielsen & Chuang, Quantum Computation and Quantum Information, Section 6.1.2): restricted to the real two-dimensional subspace spanned by and the component of orthogonal to it, acts as rotation by a fixed angle . Each iterate therefore advances the amplitude on the marked state along , exactly as claimed, with the rotation's initial offset (since at ).
Some number of iterations drives the probability of measuring the marked item above . The goal is stated existentially, without fixing to a specific rounded formula: the rotation angle can be made to land within of by an appropriate integer , and at that point . Pinning down to an explicit closed form (e.g. the nearest integer to ) is one valid strategy, but is not required by the statement — any correct choice of , and any correct proof it works, closes the goal.
Grover's algorithm is the second landmark quantum algorithm after Shor's, and the one with the
widest applicability: because it treats the search space as a black box, it accelerates any
brute-force search — SAT solving, collision finding, and generic key search among them — which is
the concrete reason NIST's post-quantum cryptography standards double symmetric key lengths rather
than replacing them outright. The mathematics itself has been fully settled since 1996, including
matching optimality lower bounds; nothing here is open. What this mission adds is a machine-
checked derivation of the amplitude formula and success bound directly from the definitions of
the oracle and diffusion operators as concrete linear operators on EuclideanSpace ℂ (Fin N) —
Mathlib has the finite-dimensional inner product space and rank-one operator machinery this needs
(InnerProductSpace.rankOne, EuclideanSpace.single), but no existing formalization of the
algorithm itself.
The obvious first attempt tries to track the full -dimensional state vector through iterations. This is intractable in general: 's action on an arbitrary basis vector depends on its overlap with both and . The move that makes the problem tractable is recognizing that preserves the two-dimensional real subspace — everything orthogonal to this plane is fixed by both and , and inside the plane is exactly a rotation matrix by angle . Establishing this invariance and then tracking only the rotation angle (rather than the full vector) is the standard reduction, and the one this mission's milestones are built around; skipping it and attempting a direct -dimensional induction does not scale.
Works over a general together with a marked index — no
assumption that is a power of two, since the rotation argument is agnostic to how the basis
states are physically encoded into qubits (that encoding is a separate, unrelated concern from the
search dynamics proved here). Supplying w0 : Fin N already forces ; no separate
nonemptiness hypothesis is added. The oracle and diffusion operators are built directly from
Mathlib's InnerProductSpace.rankOne rather than an ad-hoc pointwise definition, so their
reflection structure (and hence unitarity) is visible from the definition itself. A trivializing
formalization is ruled out explicitly: the goal is stated as an existential over rather than a
fixed closed-form iteration count, so a correct proof must still exhibit a genuine successful
and establish the bound — it cannot be discharged by an unrelated or degenerate choice. Contributions
extending this to multiple marked items, or proving the matching lower bound
(Bennett–Bernstein–Brassard–Vazirani 1997), are welcome as follow-up missions.
Finding the eigenvalues of a large matrix or linear operator by computing its characteristic polynomial is numerically unworkable: the roots of a degree- polynomial are exponentially sensitive to small coefficient perturbations, and no closed-form root formula exists once . The power method avoids the polynomial entirely. Introduced in essentially its modern form by Müntz (1913) and von Mises and Pollaczek-Geiringer (1929), and analyzed rigorously alongside its shifted and inverse variants throughout the mid-20th century (Wilkinson, The Algebraic Eigenvalue Problem, 1965), it remains, in the guise of one power iteration per step, the engine inside PageRank, spectral clustering, and the Lanczos/Arnoldi methods used to find eigenpairs of matrices too large to diagonalize directly.
Let be a finite-dimensional inner product space over , with inner product and norm , and let be a self-adjoint (symmetric) linear operator: for all . The spectral theorem for finite-dimensional self-adjoint operators gives an orthonormal basis of () consisting of eigenvectors of , with real eigenvalues satisfying .
Call dominant if for every — it is then the unique eigenvalue of largest magnitude. Given a starting vector with coordinates in the eigenbasis, the power iterates are for , and the Rayleigh quotient of at a nonzero vector is
which recovers exactly when is the eigenvector .
Rewriting the -th power iterate in the eigenbasis: applying times raises each coordinate's eigenvalue factor to the -th power, since acts diagonally on the eigenbasis. This is the algebraic core the rest of the argument rescales and takes limits of.
Given a dominant eigenvalue and , dividing the expansion above by leaves the -th term fixed at while every other term is multiplied by , since for . This is the precise sense in which the power iterates "align" with the dominant eigenvector.
The practical output of the power method: the Rayleigh quotient of the (unrescaled) iterates converges to the dominant eigenvalue itself, giving a numerically computable estimator that needs no knowledge of in advance. This is the weakest statement that captures "the power method converges to the dominant eigenvalue" without hard-coding a convergence rate, so it is the mission's goal.
The power method is the template every practical large-scale eigenvalue algorithm departs from:
shifted inverse iteration, Rayleigh quotient iteration (with locally cubic convergence), the
QR algorithm, and Krylov subspace methods (Lanczos, Arnoldi) all begin from the same
diagonal-power argument formalized here, then add a trick — a shift, a change of subspace, an
orthogonalization step — to accelerate or extend it. The result itself is classical and
completely settled mathematically; there is no open question in the convergence theory of the
basic power method under the dominant-eigenvalue hypothesis used here. What this mission
contributes is a machine-checked version of that classical argument built directly on
Mathlib's existing finite-dimensional spectral theorem
(LinearMap.IsSymmetric.eigenvalues/eigenvectorBasis) — as of this writing, Mathlib's
InnerProductSpace/Spectrum.lean and Rayleigh.lean files contain the spectral decomposition
itself, and a Rayleigh quotient for ContinuousLinearMap, but not this convergence statement.
The obvious first attempt is to bound by a naive
sum of norms and take limits termwise; this works for the rescaled sequence (Milestone 2) but
does not by itself give the Rayleigh-quotient limit, because is invariant only under
nonzero scalar rescaling, not under limits taken carelessly — one has to first establish that
the limit vector is nonzero (using ), then invoke continuity of
away from to transport the Tendsto from the rescaled sequence to
. Getting the degenerate case right is the
other trap: with only one eigenvalue, the dominance hypothesis is vacuous, and if that
eigenvalue is allowed to be the rescaling divides by zero and the
rescaled-convergence statement becomes false — the formalization must therefore assume
explicitly rather than deriving it from dominance alone.
The mission works with a general RCLike 𝕜 field (real or complex ), a LinearMap.IsSymmetric
operator on a FiniteDimensional inner product space, and Mathlib's own eigenvalues/
eigenvectorBasis (which already fixes the eigenbasis and a specific, decreasing-by-value
ordering of eigenvalues — the formalization does not re-derive the spectral theorem). Dominance
is stated by magnitude (|\lambda_j| < |\lambda_{i_0}|), not by position in Mathlib's ordering,
since the dominant eigenvalue need not be the largest by value (it could be the most negative).
The starting vector is arbitrary subject to ; no normalization ()
is imposed, since the Rayleigh quotient and the rescaled limit are both scale-invariant/
scale-equivariant. A trivializing formalization is ruled out explicitly: without both
and , the , counterexample above makes the
rescaled-convergence statement false, so these are load-bearing hypotheses, not decoration.
Contributions on the two milestones (the algebraic iterate expansion, and the rescaled-limit
argument) are especially welcome, since they are reusable building blocks for any future mission
on shifted/inverse power iteration or Rayleigh quotient iteration.
When replenishment takes several periods, an inventory decision commits stock before the demand that will consume it is known. Too much stock incurs holding costs; too little loses sales. An optimal decision can depend on the entire pipeline of outstanding orders. A rule with only two adjustable parameters is easier to implement, but its simplicity alone gives no guarantee on the cost it can incur.
Capped base-stock policies combine an inventory-position target with a maximum order quantity. The class was introduced and analyzed by Xin (2021). The present target is the finite-lead-time guarantee in Linwei Xin's Capped Base-Stock Policies: A 2.33-Approximation, specifically the author-supplied manuscript with source label thm-main. A public listing of the paper identifies the July 17, 2026 working paper; the supplied text is the authoritative version for this formalization.
Periods are discrete. Demand is a sequence of independent, identically distributed nonnegative real random variables with finite, strictly positive mean . The deterministic lead time is an integer . Holding and lost-sales rates are and .
At the beginning of period , is on-hand inventory and are outstanding orders, with due immediately. That arrival is received, an order is placed, demand is realized, and costs are charged. The new order arrives periods later. The equations are
Here . Unfilled demand is lost rather than backlogged. With , the period cost is . Initial inventory and every pipeline coordinate are zero. A nonanticipative policy chooses orders using only information available before the current demand; policies may depend on the entire observed past and on independent private randomization.
For a policy , its long-run expected average cost is
The capped rule is for finite . Write . Ordinary base stock is already included by taking ; no infinite order cap is required.
For and , set
Empty sums are zero. The lower certificate is
The pair is feasible. Both horizon constraints are retained. With
the goal is Theorem 1's complete assertion:
The exact rational constant is used; the title's 2.33 is a rounded description. Multiplicative inequalities also make sense when the optimal cost is zero.
Five supporting targets reproduce selected source statements: Proposition 1's lower-certificate bound; Proposition 2's finite-cap cost conclusion; Lemma 2's bound on a consecutive block in the greedy recursion; Proposition 3's ordinary-base-stock cost bound; and Proposition 4's two-branch inequality. The finite-cap and ordinary-base-stock parameters remain exactly and , respectively. Labels accompany the printed numbering so the supplied source is unambiguous.
The result gives a uniform cost guarantee for this policy class across all positive holding and penalty rates, every positive integer lead time, and arbitrary nonnegative demand laws with finite positive mean. It bounds the infimum of costs over the policy parameters; it does not by itself provide an algorithm for selecting parameters or assert that the infimum is attained. At the displayed coefficient is 2, while its uniform upper bound is .
The manuscript supplies mathematical proofs. This mission asks for checked proofs of their formal statements. Compiling the declarations confirms that they are well formed, not that the claims are proved. A completed development would provide reusable delayed-inventory dynamics, measurable history policies, average-cost optimization objects, finite-horizon demand envelopes, and policy-comparison results.
The pipeline carries consequences of past decisions across multiple demand periods. Nonanticipativity and independence must be stated precisely before expectation and convexity arguments can be used. Also, existence of a stationary distribution alone does not identify its expected cost with a long-run cost from an empty initial system. The manuscript invokes stationary results from prior inventory work, including Xin and Goldberg (2016), and uses stationary CBS quantities in intermediate arguments. Their needed hypotheses and connections to the original objective require proof within a complete development.
The two cost bounds depend on both coordinates of a feasible lower-certificate pair. Losing either horizon constraint changes that certificate. Replacing it with an arbitrary scalar lower bound or assuming the policy comparisons would remove substantive parts of the result.
Stock, orders, and demand take arbitrary nonnegative real values. Time is represented from zero in the operational model, corresponding to period one in the manuscript. The formal representation uses a canonical probability model with independent demand coordinates and an independent uniform private seed; measurable time-dependent decision functions use only preceding demands and that seed. Connecting arbitrary standard-Borel randomized controls to this canonical realization is a representation obligation. The zero-start optimum ranges over these general history policies, not only stationary or capped policies.
Expected nonnegative costs, their upper limits, and cost infima are represented in the extended nonnegative reals. Thus a policy with infinite expected cost does not acquire a fictitious zero value through a totalized real integral. The finite-horizon envelope expectations use the original integrable demand law. The greedy lemma uses integer-indexed sequences so subtraction of earlier times has no natural-number truncation; its blocks are nonempty, as required to define their maximum.
Definitions contain no unproved facts. In particular, stationarity, convergence from the empty initial state, lower bounds, and upper policy comparisons are not fields assumed by the model. Contributions to these intermediate obligations and to any of the five source targets support the central theorem.
thm-main), Proposition 1 (lemma-lb), Proposition 2 (prop-finite-cap-bound), Lemma 2 (lem-greedy-window), Proposition 3 (prop-base-stock-bound), Proposition 4 (lem-two-branch). Source SHA-256: f353793c255e1ebed5f3ec541037284bd926183e3e5b71941f13e79c2d67cb7a.Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.
The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly candidate_only: it is bounded search evidence, not a proof of the unrestricted theorem.
A tournament is an orientation of a finite complete simple graph. For each pair of distinct vertices , exactly one of and is present. Every directed arc receives one of three labeled colors.
A rainbow directed triangle is a cyclically oriented triangle
whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.
A vertex is a monochromatic source when, for every vertex , there is some color and a directed -to- path all of whose arcs have color . The chosen color may depend on ; the theorem does not demand one common color for all targets. Length-zero reachability handles .
The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.
For every nonempty finite tournament with a three-coloring of its arcs,
No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.
The first milestone freezes the exact bounded claim supported by the replay package:
The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.
The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.
The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc may encode that cannot reach ; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.
The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.
The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.
Lean represents the tournament as a binary relation D with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.
The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.
Every introductory number theory course opens with the same fact: the integers factor into primes in exactly one way. Euclid's Elements (Book IX, Proposition 14) already proves a form of it for the case of two factorizations sharing no further structure, but the theorem is not stated in full generality — with existence and uniqueness as a single package — until Gauss's Disquisitiones Arithmeticae (1801, Art. 16). Every standard modern treatment restates it as the opening theorem of the subject: Hardy & Wright, An Introduction to the Theory of Numbers (Theorem 2), and Apostol, Introduction to Analytic Number Theory (1976, Theorems 1.9–1.10), both prove it in the first chapter, before anything else is developed. The reason is structural, not pedagogical convenience: gcd, lcm, multiplicative functions, the notion of "the" prime factorization of an integer, and the entire multiplicative structure of depend on it being true. Mathlib itself packages the general statement as UniqueFactorizationMonoid, of which is one instance — this mission asks for the classical, elementary argument specific to , in the two-part shape every textbook gives it.
A prime is a natural number whose only divisors are and (Mathlib's Nat.Prime). A factorization of is represented here as a multiset of natural numbers — an unordered collection that tracks multiplicity but not order, so that two factorizations differing only by a reordering of their factors are already identified as the same multiset, with no separate permutation argument needed. Write for the product of the elements of with multiplicity, under the convention that the empty multiset has product . The theorem concerns multisets all of whose elements are prime.
For every nonzero there is exactly one multiset of primes whose product is . This is the capstone: existence and uniqueness combined into the single statement every textbook eventually asserts.
Every nonzero natural number is a product of primes (Apostol, Theorem 1.9). This alone says nothing about how many such multisets there might be.
Any two multisets of primes with the same product are equal (Apostol, Theorem 1.10). Combined with Milestone 1, this gives the Goal.
The result itself. Unique factorization is what makes "the prime factorization of " a well-defined object rather than a choice. Every downstream elementary and analytic number theory construction leans on it: and computed via shared prime exponents, multiplicative arithmetic functions (, , ) defined by their values on prime powers, the Euler product for , and -adic valuations. Without it, none of these constructions are canonical.
Formalizing it. The general statement is already machine-checked in Mathlib as an instance of UniqueFactorizationMonoid (and concretely realized for via Nat.factors/Nat.factors_unique), so this is not open mathematics. What this mission asks for is the specific, elementary two-lemma argument — strong induction for existence, Euclid's lemma plus strong induction for uniqueness — spelled out for with the Multiset representation used here, rather than a one-line appeal to the packaged Mathlib result. A solution that simply repackages Nat.factors_unique and its companions is a legitimate route (nothing here is designed to block it), but the more valuable contribution is the self-contained classical proof, since that is what a reader of Apostol or Hardy & Wright expects to see reconstructed.
For existence, ordinary induction on does not immediately work: if is composite, with , and the inductive hypothesis is needed for both and at once, neither of which is simply . The fix is strong (well-founded) induction on , splitting into the prime case (trivial single-element multiset) and the composite case (combine the two multisets for and ).
For uniqueness, the natural first attempt — "cancel a common prime factor from both sides and recurse" — silently assumes that the same prime appears in both multisets, which is exactly what needs to be proved. The step that actually does the work is Euclid's lemma: if a prime divides a product , it divides one of the factors of . This is not a restatement of primality (irreducibility, "no nontrivial divisors") but a genuinely separate fact about that requires either Bézout's identity or a well-ordering argument to establish; conflating "prime" with "has this divisibility property" is the standard trap for a first attempt at this proof.
The statement is specific to (not or a general UniqueFactorizationMonoid), and factorizations are represented as Multiset ℕ rather than List ℕ up to permutation — this is a deliberate choice that folds "unique up to reordering" directly into multiset equality. The hypothesis is , not : the case is included, and its unique witness is the empty multiset, since the empty product is and no nonempty multiset of primes (each ) can have product . is excluded because no multiset of natural numbers has product under this convention (every prime is , and the empty product is ), so no factorization of exists to be unique.
No auxiliary platform Definitions are required — the statement is expressed entirely in terms of Nat.Prime and Multiset.prod from Mathlib. Reusable contributions welcome beyond the two milestones: an explicit construction of the canonical sorted List ℕ factorization (Nat.factors-style) connecting this multiset formulation to the more computational list representation, or a generalization of the uniqueness argument to an explicit statement and proof of Euclid's lemma as a standalone milestone.
Mathlib.RingTheory.UniqueFactorizationDomain, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/UniqueFactorizationDomain.htmlDiophantine equations ask for integer solutions to arithmetic equations. One family of questions starts with a set of positive integers and imposes the same condition on every pair: their product, increased by one, must be a square. The question is how many distinct integers can satisfy all those conditions together. It connects a simple definition with a global restriction on simultaneous integer solutions.
The paper There is no Diophantine quintuple, by Bo He, Alain Togbé, and Volker Ziegler, resolves the nonexistence question for sets of five elements. This mission targets its headline result, Theorem 1 in Section 1. The mathematical theorem is proved in the paper; the remaining goal is a complete Lean proof of that result.
A perfect square is an integer of the form for a natural number . A Diophantine -tuple is a set of distinct positive integers such that the product of any two different members, plus one, is a perfect square. Here records the number of elements, not a bound on their sizes. A Diophantine quintuple would have exactly five members (definition in Section 1).
Write those five integers as . Positivity means for every index. Distinctness means whenever . The square condition requires a possibly different square root for each pair. There is no requirement that the ten square roots coincide, be distinct, or satisfy an additional ordering condition.
The theorem concerns positive integers. Replacing them by rational numbers changes the question. Likewise, allowing zero changes the admissible objects, and allowing repeated entries ceases to represent a five-element set. These domain choices are explicit in the formal target.
The single goal is the following nonexistence statement:
This is Theorem 1 of the paper. The mission's goal is the existing declaration no_diophantine_quintuple.
The integers are unrestricted in size. The target does not fix the smallest entry, require a particular triple among the entries, or assume that an entry falls below a numerical search threshold. A proof must cover every quintuple satisfying the stated domain conditions.
The result rules out an entire class of simultaneous square equations. As an immediate consequence, any set of distinct positive integers satisfying the same pairwise condition has at most four elements: a larger set would contain five distinct members that inherit the condition. This consequence explains why the five-element statement also constrains larger configurations.
A completed formalization would supply a reusable theorem that can be invoked whenever five distinct positive integers and their pairwise square witnesses arise. It would turn the informal nonexistence claim into a checked contradiction from precisely those hypotheses. The published statement is currently open for a Lean proof; its successful compilation verifies that the statement is well formed, not that the theorem has been proved.
Testing examples cannot establish this target by itself. Any computation with a fixed search limit addresses only a bounded collection, while the statement quantifies over all positive integers. A formal proof that uses a finite computation must also establish why the computation covers every possible case.
The conditions are simultaneous: each entry participates in four pairwise equations. Solving or excluding one isolated pair does not by itself settle whether all ten equations can hold together. The paper's proof overview in Section 2 describes the arithmetic estimates and computational components behind its result. Formalizing those components entails checking their hypotheses and connecting their conclusions to the unrestricted goal.
The Lean declaration represents the entries by a function a : Fin 5 → Nat. It places the existence of that function under a negation and includes three conditions: every value is positive, different indices have different values, and every pair of different indices has a natural-number square witness.
The square condition is written for all unequal indices. This is equivalent to the usual condition for increasing pairs because multiplication is commutative. No increasing ordering of the five values is imposed. A development using sorted entries must justify its connection to this unrestricted indexed representation.
The root statement needs only Lean's core natural numbers, finite index type, arithmetic, and logic. It introduces no custom predicate whose meaning could hide additional assumptions. A complete proof may use Mathlib and reusable supporting results about integer arithmetic, squares, and the arithmetic tools required by the chosen argument. Supporting declarations should state their hypotheses explicitly and ultimately connect to this exact root theorem. Contributions establishing the known result, including an alternative rigorous proof, are within scope.
Two-dimensional lattice models admit topological defects whose energetic cost competes with their configurational multiplicity. The later stages of a finite vortex argument therefore need a trustworthy bridge from a prescribed vorticity to the least quadratic energy of a compatible field. This mission isolates that bridge. It does not attempt a phase-transition theorem; it establishes only the finite-dimensional variational identity on which a later, model-specific energy estimate can rest.
The algebra belongs to finite discrete Hodge theory. A finite cochain complex supplies a differential from degree one to degree two and an adjoint codifferential in the reverse direction. A normalized Green operator inverts the degree-two Laplacian on realizable vorticities and annihilates the harmonic obstruction. Such finite-complex harmonic methods go back at least to Beno Eckmann's 1944 treatment of harmonic functions and boundary-value problems on complexes. The vortex motivation comes from the energy--entropy mechanism discussed by Kosterlitz and Thouless for two-dimensional systems, but no claim from their thermodynamic analysis is included here.
Let be finite-dimensional real inner-product spaces. A finite Hodge complex consists of linear maps
together with specified adjoints and , and the cochain relation . The degree-two Laplacian is
The vorticity space is . A normalized degree-two Green owner supplies a unique self-adjoint linear map satisfying both inverse identities with the orthogonal projector onto that range, taking values in the range, and vanishing on .
For a realizable source , define the canonical one-cochain
The physical vortex normalization scales the prescribed vorticity by , so the canonical physical field is . For a coupling , the quadratic energy of is
For every realizable and every field satisfying , establish
The equality is required for every real . Its unscaled components assert the exact Poisson equation, closedness and orthogonality of the residual, the Pythagorean norm decomposition, and the identity
For , conclude
Two controls are part of the target boundary: zero coupling must not identify a unique minimizer, and zero vorticity must not imply that the underlying field or its positive-coupling energy vanishes.
The result separates universal finite linear algebra from geometry that depends on a particular lattice. Once a periodic square torus is registered as a finite Hodge complex, a later theorem may specialize the Green quadratic form to dipole charges and investigate its dependence on separation. Entropy can then be compared with a genuine energy inequality without redefining energy through the desired conclusion.
Formalizing this layer provides reusable interfaces for Poisson solvability, orthogonal residuals, exact quadratic energy splitting, and the nonnegative-coupling lower bound. It also makes normalization errors visible: the factor in the source and the factor in the energy force the coefficient . The underlying Green-owner infrastructure already has a machine-checked implementation in LeanProofs; the propositions in this mission are new proof obligations derived from that interface.
The central issue is not an asymptotic estimate. It is maintaining the exact relationship among the Laplacian sign, the orthogonal projector, the Green normalization, adjointness, and the physical scaling. A proof that silently projects a non-realizable source changes the problem. A proof that divides by loses the case. A proof that treats zero vorticity as a zero-field assertion discards closed and harmonic residuals. Each of these shortcuts is ruled out by the formal target or its controls.
The Lean development uses arbitrary finite-dimensional real inner-product spaces rather than a concrete torus. All maps are continuous only through finite-dimensional linear structure; there is no measure theory, probability, or limiting process. A source is explicitly required to lie in . The exact decomposition permits every real , while the inequality requires . Existence of a Green owner is supplied as data; this mission neither constructs a second inverse nor changes the existing normalization.
The mission does not define integer charge, torus distance, plaquette winding, or a concrete lattice Laplacian. It proves no logarithmic Green estimate, cosine-energy comparison, entropy bound, Gibbs statement, vortex proliferation result, thermodynamic limit, BKT transition, or universal jump. In particular, the target cannot be satisfied by choosing a convenient torus size or hard-coding a Green kernel: it is group-generic finite-dimensional algebra conditional on the stated Hodge and Green structures.
Contributions are welcome on the independent Poisson, orthogonality, norm, scaling, and control nodes. A later mission can add the square-torus realization and the separate analytic capacity estimate needed for a sharp logarithmic lower bound.
dbf503b2909cc17787d40a21eb75a0c9354cc6ef. https://github.com/MonumentalSystems/LeanProofs/commit/dbf503b2909cc17787d40a21eb75a0c9354cc6efFor every integer
, there exists a prime p such that
An almost complex structure gives every tangent space of a smooth manifold the linear algebra of a complex vector space, but it need not come from complex-valued coordinate charts. The gap between these two notions is a global differential-geometric question, not a change of terminology. Granja and Milivojević describe the following as “a major open problem in differential geometry”: whether every closed almost complex manifold of dimension at least six admits an integrable complex structure (Introduction, p. 1). This mission records that question as an open conjecture, not as an established theorem.
Fix an integer . Let be a connected, compact, Hausdorff, second-countable smooth manifold without boundary and of real dimension . An almost complex structure on is a smooth field
of real-linear maps satisfying for every and . This condition forces even real dimension, but by itself supplies no complex coordinate charts.
A complex structure of complex dimension is an atlas with values in whose transition maps are complex differentiable. Such an atlas induces an integrable almost complex structure. The target concerns existence on the underlying smooth manifold: the complex structure obtained may induce a different almost complex structure from the supplied . It does not claim that every chosen almost complex structure is integrable.
Here “closed” means compact and without boundary. Connectedness is explicit because it is part of the standing manifold convention in the cited 2022 source. The lower bound is on real dimension: , equivalently .
For every and every closed connected smooth real -manifold ,
“Compatible” means that the underlying real smooth structure of the complex atlas is smoothly equivalent to the given smooth structure on the same topological space. No claim of uniqueness, equality with the original atlas, or integrability of the supplied is made.
The real six-dimensional case is essential. Since carries an almost complex structure, the conjecture would imply that its underlying smooth manifold carries some complex structure. That special case remains unresolved; restricted nonexistence results, such as results imposing compatibility with a particular metric, do not decide the unrestricted existence question.
A positive solution would replace a pointwise tangent-bundle reduction by genuine holomorphic coordinates for every manifold in the stated class. It would in particular settle the existence question for . A negative solution would identify additional global obstructions to complex atlases that are invisible to the existence of an almost complex structure.
The formalization isolates a reusable smooth almost complex structure on top of Mathlib’s tangent-bundle and manifold APIs, while making the desired complex atlas explicit. This prevents the central distinction from being hidden inside an unconstrained predicate named “integrable.” It also exposes the compatibility between the original real smooth atlas and the real atlas underlying the complex charts, which future work on characteristic classes, Nijenhuis tensors, and concrete six-manifolds can reuse.
The equation is fiberwise algebra. Integrability requires local complex coordinates whose overlaps are holomorphic, equivalently the vanishing condition identified by Newlander and Nirenberg. Smooth variation of does not make that differential condition automatic. Thus simply viewing each tangent space as a complex vector space does not construct a complex manifold.
The six-sphere shows why the dimension threshold cannot be treated as a routine stable-range simplification. Its known almost complex structure supplies the hypothesis in real dimension six, while no arbitrary complex atlas is known. Likewise, replacing the conclusion by a complex vector-space structure on each tangent fiber would merely repeat the hypothesis and would not address the open problem.
The namespace AlmostComplexToComplex uses Mathlib’s boundaryless Euclidean manifold model. AlmostComplexStructure n M contains a continuous real-linear map on every tangent space, the pointwise identity , and smoothness of the induced self-map of the total tangent bundle. It contains no integrability field.
The main theorem assumes the real atlas is modeled on and concludes the existence of charts modeled on . Mathlib’s IsManifold condition over at order one states complex differentiability of chart transitions. Two conditions on the identity map compare the original real atlas and the real manifold structure underlying the complex charts in both directions; an unrelated smooth structure therefore cannot satisfy the conclusion merely by being placed on the same carrier type.
This is a chart-level interface, not yet a development of analytic integrability theory. Mathlib at the pinned revision has no ready-made almost-complex/Nijenhuis package connecting the structure above to the Newlander–Nirenberg criterion. The target does not assert that the supplied is integrable or homotopic to the one induced by the resulting atlas. A dedicated milestone is also outside this minimal draft because faithfully constructing the standard sphere and its known almost complex structure would require additional sourced infrastructure; no surrogate special case is inserted.