2-Coloring Cycles in One Round to Sharp list-scheduling and…
Theorem2-Coloring Cycles in One Round#
Formalizes certified upper and lower bounds for one-round randomized algorithms that 2-color cycles.
Quoted from the card LeanPool/projects/2-coloring-1-round.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Distributed2Coloring.pStar_ge_23879(theorem; a main declaration), declared in LeanPool/TwoColoringOneRound/MainResults.lean, line 70: “Proves that every one-round classical algorithm has monochromatic-edge probability at least 0.23879.”Distributed2Coloring.pStar_lt_24118(theorem; a main declaration), declared in LeanPool/TwoColoringOneRound/MainResults.lean, line 79: “Proves that an explicit one-round algorithm attains monochromatic-edge probability strictly below 0.24118.”
Project
- Authors: Jukka Suomela.
- Source: arXiv:2603.04235.
- Project repository: suomela/2-coloring-1-round.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0, keeping its copyright line: “Copyright (c) 2026 Jukka Suomela”.
- MSC2020: 68W15, 05C15.
- In Lean Pool: LeanPool/TwoColoringOneRound, from the card LeanPool/projects/2-coloring-1-round.yaml.
Sources
TheoremThe Aaronson–Ambainis influence conjecture#
Proves that a real polynomial of degree at most d, bounded between zero and one on the Boolean cube and with variance at least epsilon > 0, has a coordinate of squared-difference influence at least (epsilon/d)^7. Also proves explicit bounds with epsilon^(5/2)/d^6, together with determinant pairings, fractional-certificate inequalities and coordinate averaging. The internal packing-cover duality supports the proof; generic finite LP duality is already pooled as StandardLP.strongDuality. The sharper constant is conditional on the stated Agarwal–Ben-David fractional block-sensitivity bound. Quantum simulation consequences are outside this formalization.
Quoted from the card LeanPool/projects/aaronson-ambainis.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
AaronsonAmbainis.aaronson_ambainis(theorem; a main declaration), declared in LeanPool/AaronsonAmbainis/Main.lean, line 44: “For every real polynomial in N variables of total degree at most d, bounded between zero and one on the Boolean cube, positive variance at least epsilon guarantees a coordinate whose uniform mean squared change under a bit flip is at least (epsilon/d)^7.”AaronsonAmbainis.aaronson_ambainis_explicit(theorem; a main declaration), declared in LeanPool/AaronsonAmbainis/Main.lean, line 49: “Under the same hypotheses, a coordinate has squared-difference influence at least 8 sqrt(15) epsilon^(5/2) / (125 pi^4 d^6).”AaronsonAmbainis.aaronson_ambainis_pm(theorem; a main declaration), declared in LeanPool/AaronsonAmbainis/Main.lean, line 54: “For a real polynomial of degree at most d bounded in absolute value by one on the sign cube, positive variance at least epsilon guarantees a coordinate whose uniform mean squared half-difference under a bit flip is at least sqrt(15) epsilon^(5/2) / (500 pi^4 d^6).”AaronsonAmbainis.aaronson_ambainis_of_fbsDegreeBound(theorem), declared in LeanPool/AaronsonAmbainis/Main.lean, line 59: “Assuming the explicitly stated Agarwal–Ben-David fractional block-sensitivity bound, the zero-one cube influence bound improves to 32 sqrt(15) epsilon^(5/2) / (125 pi^4 d^6).”
Project
- Authors: David Turturean.
- Source: A proof of the Aaronson–Ambainis conjecture.
- Project repository: physical-superintelligence/aaronson-ambainis, at commit 2a6ceaef.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 68Q12, 60C05, 05D40.
- In Lean Pool: LeanPool/AaronsonAmbainis, from the card LeanPool/projects/aaronson-ambainis.yaml.
Sources
TheoremAdversary bounds and the polynomial method for quantum queries#
Develops finite quantum query algorithms, real adversary primal and dual programs, strong duality, exact Boolean block composition, explicit constant-factor bounded-error query characterizations, and degree bounds for output-probability polynomials. Query models include idle and blank sectors; bounds count queries, not gate complexity or running time. Uniform algorithm extraction assumes a supplied dual certificate.
Quoted from the card LeanPool/projects/quantum-query-foundations.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
QuantumQueryComplexity.advDual_eq_advPM(theorem), declared in LeanPool/QuantumQuery/Adversary.lean, line 6567: “For every total Boolean function on a finite Boolean input cube, the all-pairs real adversary dual infimum equals the real symmetric primal supremum.”QuantumQueryComplexity.advPM_composeFun_eq(theorem), declared in LeanPool/QuantumQuery/Adversary.lean, line 6587: “The negative-weight adversary value of total Boolean functions composed on disjoint blocks equals the product of their adversary values, including constant functions and empty index types.”QuantumQueryComplexity.boundedErrorQQuery_characterized_by_advPM(theorem; a main declaration), declared in LeanPool/QuantumQuery/QueryBounds.lean, line 1806: “For a total Boolean function at error one third, quantum value-query complexity lies between ADV±/36 and 2^14 ADV±. The value oracle swaps a blank answer with the queried letter and includes an idle query index.”QuantumQueryComplexity.xorQQuery_characterized_by_advPM(theorem), declared in LeanPool/QuantumQuery/QueryBounds.lean, line 1818: “For the Boolean XOR oracle with idle and blank sectors, query complexity at error one third lies between ADV±/72 and 2^15 ADV±.”QuantumQueryComplexity.qQueryOn_third_le_of_hasDualOn_uniform(theorem), declared in LeanPool/QuantumQuery/StateConversion.lean, line 5494: “A supplied all-pairs real dual certificate of nonnegative cost c gives a finite quantum algorithm using at most 8192(1+c) value queries at error one third, for any finite promise domain and nonempty decidable output type.”QuantumQueryComplexity.QAlg.exists_probability_polynomial(theorem), declared in LeanPool/QuantumQuery/Polynomial.lean, line 388: “Each output probability of a q-query value-oracle algorithm on Boolean inputs agrees on the Boolean cube with a real polynomial of total degree at most 2q.”QuantumQueryComplexity.exists_xor_probability_polynomial(theorem), declared in LeanPool/QuantumQuery/Polynomial.lean, line 516: “Each output probability of a q-query Boolean XOR algorithm agrees on the Boolean cube with a real polynomial of total degree at most 2q.”
Project
- Authors: Troy Lee.
- Source: arXiv:1011.3020v2.
- Project repository: troyjlee/quantum-query-complexity, at commit 517ba85e.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 68Q12, 81P68.
- In Lean Pool: LeanPool/QuantumQuery, from the card LeanPool/projects/quantum-query-foundations.yaml.
Sources
TheoremBeyond the Bethe approximation of the permanent#
Constructs a deterministic polynomial-time approximation algorithm for the permanent of every nonnegative rational matrix, with exponential base strictly smaller than the square root of two. The development includes stable-polynomial inequalities, rational convex optimization, finite-precision arithmetic, and a Turing-machine complexity proof.
Quoted from the card LeanPool/projects/formalization-beyond-bethe.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
BeyondBethe.theoremOne(theorem; a main declaration), declared in LeanPool/BeyondBethe/BeyondBethe/Main.lean, line 255: “There is a fixed rational algorithm approximating the permanent of every nonnegative rational n-by-n matrix within c^n for an absolute c below sqrt(2), with a deterministic polynomial-time Turing-machine implementation.”
Project
- Authors: Nima Anari, Samuel Schlesinger, Bolton Bailey, Christian Reitwiessner.
- Project repository: nimaanari/formalization-beyond-bethe, at commit 325cda6d.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 68W25, 15A15.
- In Lean Pool: LeanPool/BeyondBethe, from the card LeanPool/projects/formalization-beyond-bethe.yaml.
Sources
TheoremBlock sensitivity can exceed spectral sensitivity squared#
Constructs a total Boolean function on 14011 blocks of 144 bits with block sensitivity at least 14011 and squared spectral sensitivity at most U = 7149 + 2 sqrt(150108). Proves the strict separation lambda(f)^2.12 < bs(f), multiplicativity of spectral sensitivity under arbitrary block composition, and an exponential lower bound with factor 14011/U > 1.768 for the self-composed family. Includes reusable finite product probability, an asymmetric Lovasz local lemma, partial Boolean assignments, certificate-family spectral bounds, and a Paley doubly regular tournament. The formalized explicit exponent is 2.12; the exact logarithmic exponent is also retained.
Quoted from the card LeanPool/projects/block-spectral-sensitivity.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
BSLambda.Final.exists_bs_gt_lam_rpow(theorem; a main declaration), declared in LeanPool/BlockSpectralSensitivity/Main.lean, line 297: “There exists a total Boolean function on ZMod 14011 times Fin 144 whose block sensitivity strictly exceeds its spectral sensitivity raised to the real exponent 2.12.” Its source, as the card gives it: “Upstream Main.lean; bs_lambda.txt Sections 5-12 and 14.”BSLambda.Final.exists_counterexample(theorem), declared in LeanPool/BlockSpectralSensitivity/Main.lean, line 305: “There exists a gate labelling whose certificate-union indicator f has bs(f) at least 14011, lambda(f)^2 at most U = 7149 + 2 sqrt(150108), and lambda(f)^alpha at most bs(f), where alpha = 2 log(14011)/log(U) > 2.” Its source, as the card gives it: “Upstream Main.lean; bs_lambda.txt Sections 5-12 and 14.”BSLambda.Final.exists_ratio_blowup(theorem), declared in LeanPool/BlockSpectralSensitivity/Main.lean, line 316: “A single gate labelling yields, for every natural m, an m-fold self-composition F_m satisfying (14011/U)^m * lambda(F_m)^2 <= bs(F_m). The auxiliary theorem ratio_gt proves 14011/U > 1.768.” Its source, as the card gives it: “Upstream Main.lean; bs_lambda.txt Section 14, division-free bound.”BSLambda.lam_comp(theorem), declared in LeanPool/BlockSpectralSensitivity/Spectral/Multiplicative.lean, line 512: “For any Boolean functions on finite coordinate types, spectral sensitivity of their block composition equals the product of their spectral sensitivities, including the degenerate cases.” Its source, as the card gives it: “Upstream Spectral/Multiplicative.lean; composition theorem used in Section 14.”BSLambda.LLL.pr_avoid_pos(theorem), declared in LeanPool/BlockSpectralSensitivity/LLL/Asymmetric.lean, line 228: “In a finite uniform product of nonempty alphabets, events supported on specified coordinate sets have positive probability of all being avoided if each event probability is at most its weight times the product of one minus the weights of its dependent neighbours, with every weight strictly between zero and one.” Its source, as the card gives it: “Upstream LLL/Asymmetric.lean; asymmetric local lemma in Section 10.”
Project
- Authors: Alex Meiburg.
- Source: Block Sensitivity can exceed Spectral Sensitivity Squared, arXiv:2608.00851.
- Project repository: Timeroot/BS_Lam, at commit 7bd39a8d.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 68Q17, 05D40, 05C50.
- In Lean Pool: LeanPool/BlockSpectralSensitivity, from the card LeanPool/projects/block-spectral-sensitivity.yaml.
Sources
TheoremCircuit Complexity in Lean 4#
A Lean 4 formalization of classical Boolean circuit complexity, including the Shannon counting lower bound, Schnorr's XOR gate lower bound, a gate-elimination lower bound, CNF/DNF lower bounds for parity, and nondeterministic quantification complexity bounds.
Quoted from the card LeanPool/projects/circuit-complexity.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
CircuitComplexity.shannon_lower_bound_circuit(theorem; a main declaration), declared in LeanPool/CircuitComplexity/Internal/Bridge.lean, line 217: “For N at least 6, there exists a Boolean function on N inputs that cannot be computed by any fan-in-2 AND/OR circuit of size at most 2^N / (5N).”CircuitComplexity.schnorr_lower_bound_circuit(theorem), declared in LeanPool/CircuitComplexity/Internal/Bridge.lean, line 235: “Any fan-in-2 AND/OR circuit computing the N-input XOR function (or its complement) has at least 2(N-1) internal gates.”CircuitComplexity.Circuit.gate_elimination_lower_bound(theorem), declared in LeanPool/CircuitComplexity/Internal/LowerBound.lean, line 167: “Any circuit over bounded fan-in k AND/OR computing a function with n' essential inputs has size at least n' / k.”CircuitComplexity.DNF.xorBool_complexity_lb(theorem), declared in LeanPool/CircuitComplexity/NF.lean, line 42: “Any DNF formula computing the N-input XOR function requires at least 2^(N-1) terms.”CircuitComplexity.CNF.xorBool_complexity_lb(theorem), declared in LeanPool/CircuitComplexity/NF.lean, line 49: “Any CNF formula computing the N-input XOR function requires at least 2^(N-1) clauses.”CircuitComplexity.existQuantify_complexity_le(theorem), declared in LeanPool/CircuitComplexity/Nondeterminism.lean, line 160: “If a function f has circuit complexity s, then the existential quantification of f over a k-bit block has circuit complexity at most 2^k * (s + 1).”
Project
- Authors: Samuel Schlesinger.
- Project repository: SamuelSchlesinger/circuit-complexity.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 68Q06, 94C11.
- In Lean Pool: LeanPool/CircuitComplexity, from the card LeanPool/projects/circuit-complexity.yaml.
Sources
DefinitionCoinductive Interaction Trees using QPFs#
Formalizes coinductive interaction trees as the M-type of a polynomial functor (via Mathlib QPFs), proving the lawful functor and monad structure, a bisimulation equality coinciding with propositional equality, and iteration and effect-handler interpretation combinators, supported by a vendored parameterized-coinduction (Paco) library.
Quoted from the card LeanPool/projects/lean4-itree.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Lean4Itree.ITree(def; a main declaration), declared in LeanPool/Lean4Itree/ITree/Basic.lean, line 56: “Defines the coinductive interaction tree as the final coalgebra (M-type) of the interaction-tree polynomial functor.”Lean4Itree.ITree.IEq(def), declared in LeanPool/Lean4Itree/ITree/Basic.lean, line 286: “Defines bisimulation equality between interaction trees as a coinductive fixed point.”Lean4Itree.ITree.ieq_iff_eq(theorem; a main declaration), declared in LeanPool/Lean4Itree/ITree/Basic.lean, line 291: “Proves that bisimulation equality of interaction trees coincides with propositional equality.”Lean4Itree.ITree.bind_assoc(theorem), declared in LeanPool/Lean4Itree/ITree/Monad.lean, line 182: “Proves associativity of monadic bind for interaction trees, part of the LawfulMonad instance.”Lean4Itree.ITree.iter(def), declared in LeanPool/Lean4Itree/ITree/EffectAlgebra.lean, line 90: “Defines the iteration combinator producing an interaction tree from a step function.”Lean4Itree.ITree.interp(def), declared in LeanPool/Lean4Itree/ITree/EffectAlgebra.lean, line 110: “Defines interpretation of an interaction tree against an effect handler into an arbitrary iterable monad.”Lean4Itree.plfp_acc(theorem; a main declaration), declared in LeanPool/Lean4Itree/Paco/PacoDefs.lean, line 185: “Proves the accumulation principle for the parameterized least fixed point underlying the Paco coinduction library.” Its source, as the card gives it: “C.-K. Hur, G. Neis, D. Dreyer, V. Vafeiadis, The Power of Parameterization in Coinductive Proof, POPL 2013, doi:10.1145/2429069.2429093.”
Project
- Authors: Paul Mure, Joonhyup Lee.
- Source: doi:10.1145/3371119, arXiv:1906.00046.
- Project repository: mit-plv/lean4-itree.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0, keeping its copyright line: “Copyright (c) 2025 the choice-tree authors (see the AUTHORS file)”.
- MSC2020: 68Q55, 18C50, 68N18.
- In Lean Pool: LeanPool/Lean4Itree, from the card LeanPool/projects/lean4-itree.yaml.
Sources
StructureEvent Structures and Causal-Consistent Reversibility#
Formalizes event structures with binary conflict, their configurations, computations, the trace monoid, and causal-consistent reversibility, proving correctness and causal-safety of rollback, uniqueness of minimal and maximal replays, and conditional replay-existence characterizations.
Quoted from the card LeanPool/projects/event-structures.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
EventStructures.EventStructure(structure; a main declaration), declared in LeanPool/EventStructures/Basic.lean, line 25: “Defines an event structure as a partially ordered set of events with an irreflexive symmetric conflict relation.” Its source, as the card gives it: “M. Nielsen, G. Plotkin, G. Winskel, Petri nets, event structures and domains, part I, Theoretical Computer Science 13 (1981), 85-108, doi:10.1016/0304-3975(81)90112-2.”EventStructures.Conf(def; a main declaration), declared in LeanPool/EventStructures/Configuration.lean, line 33: “Defines a configuration as a conflict-free, downward-closed set of events.” Its source, as the card gives it: “G. Winskel, Event structures, Advances in Petri Nets 1986, LNCS 255, Springer, 1987, 325-392, doi:10.1007/3-540-17906-2_31.”EventStructures.Rollback.rollback_correctness_finite(lemma), declared in LeanPool/EventStructures/Rollback.lean, line 232: “Proves that the original configuration is reachable from the rollback of an event when the configuration is finitely representable.” Its source, as the card gives it: “Causal-consistent reversibility in the sense of V. Danos, J. Krivine, Reversible communicating systems, CONCUR 2004, LNCS 3170, Springer, 2004, 292-307, doi:10.1007/978-3-540-28644-8_19.”EventStructures.Rollback.rollback_causal_safety(lemma), declared in LeanPool/EventStructures/Rollback.lean, line 104: “Proves causal safety of rollback - events causally after the rolled-back event are removed.” Its source, as the card gives it: “Causal-consistent reversibility in the sense of V. Danos, J. Krivine, Reversible communicating systems, CONCUR 2004, LNCS 3170, Springer, 2004, 292-307, doi:10.1007/978-3-540-28644-8_19.”EventStructures.Replay.minReplay_unique(lemma), declared in LeanPool/EventStructures/Replay.lean, line 186: “Proves uniqueness of the minimal replay of a log - any two minimal replays compatible with the log reach the same configuration.”EventStructures.Trace.TraceMonoid(def), declared in LeanPool/EventStructures/Trace.lean, line 108: “Defines the trace monoid as lists of events quotiented by the congruence generated by swapping adjacent concurrent events; paths in the configuration graph are quotiented by the same trace equivalence to form asynchronous paths.” Its source, as the card gives it: “A. Mazurkiewicz, Trace theory, Advances in Petri Nets 1986, LNCS 255, Springer, 1987, 278-324, doi:10.1007/3-540-17906-2_30.”
Project
- Authors: Vikraman Choudhury.
- Source: doi:10.1007/3-540-17906-2_31.
- Project repository: vikraman/event-structures.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 68Q85, 06A06.
- In Lean Pool: LeanPool/EventStructures, from the card LeanPool/projects/event-structures.yaml.
Sources
TheoremExact Boolean multiplicative complexity of four-term polynomial multiplication#
Proves that multiplying two binary polynomials with n coefficients needs exactly 0, 1, 3, 6, and 9 AND gates for n = 0, 1, 2, 3, and 4, with XOR and constants free and arbitrary reuse of earlier nonlinear wires. The main lower bound excludes every eight-gate circuit for n = 4. Develops Boolean algebraic normal forms equivalent to all Boolean functions, a general circuit model, dimension bounds, circuit rewiring, a Reed-Muller minimum-weight theorem, and exterior-algebra and jet arguments controlling nonlinear feedback.
Quoted from the card LeanPool/projects/boolean-multiplication.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
UnrestrictedBooleanMul.mc_mul_zero(theorem), declared in LeanPool/BooleanMultiplication/SmallCases.lean, line 367: “The empty polynomial multiplication map needs zero AND gates.” Its source, as the card gives it: “Proposition 2.3; the n = 0 target has no output coordinates.”UnrestrictedBooleanMul.mc_mul_one(theorem), declared in LeanPool/BooleanMultiplication/SmallCases.lean, line 370: “Multiplying two one-coefficient binary polynomials needs exactly one AND gate.” Its source, as the card gives it: “Proposition 2.3.”UnrestrictedBooleanMul.mc_mul_two(theorem), declared in LeanPool/BooleanMultiplication/SmallCases.lean, line 373: “Multiplying two two-coefficient binary polynomials needs exactly three AND gates.” Its source, as the card gives it: “Proposition 2.3.”UnrestrictedBooleanMul.mc_mul_three(theorem), declared in LeanPool/BooleanMultiplication/N3.lean, line 494: “Multiplying two three-coefficient binary polynomials needs exactly six AND gates.” Its source, as the card gives it: “Proposition 2.4; the lower bound is proved internally.”UnrestrictedBooleanMul.N4.mc_mul_four(theorem; a main declaration), declared in LeanPool/BooleanMultiplication/N4/Main.lean, line 62: “Multiplying two four-coefficient binary polynomials needs exactly nine AND gates, allowing free XOR, constants, and unrestricted nonlinear reuse.” Its source, as the card gives it: “Theorem 9.1.”UnrestrictedBooleanMul.N4.no_eight_gate_circuit(theorem), declared in LeanPool/BooleanMultiplication/N4/Main.lean, line 33: “No eight-AND circuit with free XOR, constants, and arbitrary nonlinear reuse computes all seven output coefficients of the product of two four-coefficient binary polynomials.” Its source, as the card gives it: “Theorem 9.1, lower bound.”
Project
- Authors: Gregory Morse.
- Source: Unrestricted Boolean Multiplicative Complexity of Four-Term Binary Polynomial Multiplication: Rational Places, Hasse Jets, and the Failure of Nonlinear Feedback, arXiv:2608.30238v1.
- The card's note on its source: “The complete Lean release predates the arXiv v1 submission of 2026-08-31T04:45:12Z. The selected September 22 commit corrects release metadata; eligibility rests on the complete August 31 Lean release at 2ebc0cf42039e4b5de84cb7f9d97cad4791c669d. The August 29 release contained computational artifacts, not the Lean formalization. The author discloses GPT-5.6 Sol for original research and proof development, Opus 5 as a critical referee, and Codex for release preparation. Gregory Morse directed and reviewed the work and assumes responsibility. AI provenance records the proof-producing agent workflow; human direction alone is not classified as mixed formalization. The complete upstream MIT notice is retained in LeanPool/BooleanMultiplication.lean. Only the published n <= 4 dependency closure is imported; no n = 5 or n = 6 claim is made.”
- Project repository: GregoryMorse/unrestricted-boolean-mul, at commit 79a80176.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
- MSC2020: 68Q06, 68Q17, 68W30, 15A75, 94D10.
- In Lean Pool: LeanPool/BooleanMultiplication, from the card LeanPool/projects/boolean-multiplication.yaml.
Sources
TheoremFinite witnesses and the width hierarchy for language generation#
Characterizes generation in the limit for arbitrary families of infinite languages over any countably infinite universe by finite positive witnesses. Ordered-history generators admit a single set-driven normalization, chosen before the target language. The separation-width invariant takes every value 0, 1, 2, ..., omega, omega+1; generation is equivalent to width at most omega. Reusable infrastructure includes locking witnesses, positive separation, bounded diagonal capture over arbitrary universes, transport under equivalences, and finite-query normalization on natural numbers. The formalized scope is the semantic characterization and hierarchy, not the paper's additional density-one or Turing-computability results in Appendices D and E.
Quoted from the card LeanPool/projects/language-generation-characterization.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
GenLimit.FiniteWitness.Simplified.ordinary_iff_finiteWitnesses(theorem; a main declaration), declared in LeanPool/LanguageGeneration/FiniteWitness/Simplified/Normalization.lean, line 172: “For any family H of infinite languages over a countably infinite universe, there exists one ordered-history generator that eventually outputs an unseen target element on every exact presentation of every target in H if and only if H admits a finite positive witness assignment whose nonempty active subfamilies always have infinite common intersection.”GenLimit.FiniteWitness.Simplified.universal_normalization(theorem), declared in LeanPool/LanguageGeneration/FiniteWitness/Simplified/Normalization.lean, line 153: “Every ordered-history generator over a countably infinite universe has one set-driven normalization that locks on every infinite target on which the original generator succeeds on all exact presentations. The normalization is chosen before the target.”GenLimit.FiniteWitness.ordinary_iff_width(theorem), declared in LeanPool/LanguageGeneration/FiniteWitness/Width/Value.lean, line 76: “A family of infinite languages over a countably infinite universe is generatable in the limit exactly when its separation width is at most omega.”GenLimit.FiniteWitness.full_range(theorem), declared in LeanPool/LanguageGeneration/FiniteWitness/Width/Endpoints.lean, line 101: “Over every countably infinite universe, every value in WithTop (WithTop Nat), representing 0, 1, 2, ..., omega, omega+1, is the separation width of some family of infinite languages.”GenLimit.FiniteWitness.bounded_capture(theorem), declared in LeanPool/LanguageGeneration/FiniteWitness/Width/Capture.lean, line 27: “Over an arbitrary universe, every sequence of uniformly bounded finite sets has infinitely many terms contained in one set D such that D contains none of a prescribed countable list of infinite cores.”GenLimit.FiniteWitness.executable_universal_normalization(theorem), declared in LeanPool/LanguageGeneration/FiniteWitness/Width/Executable.lean, line 155: “The finite-search normalization on natural numbers locks on every infinite language on which the supplied generator eventually succeeds on every exact presentation. This is a semantic correctness theorem for the defined procedure, without a formal Turing-computability claim.”
Project
- Authors: Xiaoyu Li, Andi Han, Jiaojiao Jiang, Junbin Gao, Shuangping Li, Peng Zhang.
- Source: Characterizing Language Generation in the Limit: Finite Witnesses and a Separation-Width Hierarchy by Xiaoyu Li, Andi Han, Jiaojiao Jiang, Junbin Gao, arXiv:2609.10525.
- Project repository: xiaoyulics/language-generation-characterization, at commit 4f7d3f21.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 68Q32, 68Q45.
- In Lean Pool: LeanPool/LanguageGeneration, from the card LeanPool/projects/language-generation-characterization.yaml.
Sources
TheoremFormal Learning Theory Kernel#
Formalizes major equivalences and separations in PAC, VC, Gold-style, and online learning theory.
Quoted from the card LeanPool/projects/formal-learning-theory.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 8 main results, each with its informal statement quoted from the card. The scan finds 8 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
vc_characterization(theorem), declared in LeanPool/FormalLearningTheory/Theorem/PAC.lean, line 125: “Characterizes PAC learnability by finite VC dimension.”fundamental_theorem(theorem; a main declaration), declared in LeanPool/FormalLearningTheory/Theorem/PAC.lean, line 284: “Bundles the central PAC, VC, compression, Rademacher, and sample-complexity equivalences.”fundamental_vc_compression(theorem), declared in LeanPool/FormalLearningTheory/Theorem/PAC.lean, line 242: “Relates finite VC dimension to compression with side information.”gold_theorem(theorem), declared in LeanPool/FormalLearningTheory/Theorem/Gold.lean, line 24: “States the Gold-style characterization for identification in the limit.”mind_change_characterization(theorem), declared in LeanPool/FormalLearningTheory/Theorem/Gold.lean, line 213: “Characterizes learnability by a bounded mind-change ordinal.”littlestone_characterization(theorem; a main declaration), declared in LeanPool/FormalLearningTheory/Theorem/Online.lean, line 415: “Characterizes online learnability by finite Littlestone dimension.”pac_not_implies_online(theorem; a main declaration), declared in LeanPool/FormalLearningTheory/Theorem/Separation.lean, line 1083: “Separates PAC learnability from online learnability.”ex_not_implies_pac(theorem), declared in LeanPool/FormalLearningTheory/Theorem/Separation.lean, line 1122: “Separates explanatory learnability from PAC learnability.”
Project
- Authors: Dhruv Gupta.
- Project repository: Zetetic-Dhruv/formal-learning-theory-kernel.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 68Q32, 68T05.
- In Lean Pool: LeanPool/FormalLearningTheory, from the card LeanPool/projects/formal-learning-theory.yaml.
Sources
TheoremFormalizations of theorems related to model checking#
Proves that every linear temporal logic formula has an equivalent finite-state nondeterministic Büchi automaton (via negation normal form, alternating Büchi automata, and the Miyano-Hayashi breakpoint construction), and that every linear-time property decomposes as the intersection of a safety property and a liveness property.
Quoted from the card LeanPool/projects/lean-model-checking.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanModelChecking.for_any_LTL_formula_exists_an_equivalent_NBW(theorem; a main declaration), declared in LeanPool/LeanModelChecking/LTLNBWResult.lean, line 35: “For any linear temporal logic formula there exists an equivalent finite-state nondeterministic Büchi automaton, i.e. one whose state type is finite, accepting the same language.” Its source, as the card gives it: “M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification, LICS 1986, 332-344; C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press, 2008, ISBN 978-0-262-02649-9, https://mitpress.mit.edu/9780262026499/principles-of-model-checking/”LeanModelChecking.LTL(inductive), declared in LeanPool/LeanModelChecking/LTLNBWStatement.lean, line 25: “The syntax of linear temporal logic formulas over a set of atomic propositions.”LeanModelChecking.NBW(structure), declared in LeanPool/LeanModelChecking/LTLNBWStatement.lean, line 48: “A nondeterministic Büchi automaton over a given alphabet of letters.”LeanModelChecking.ABW.toNBW.lang_eq(theorem), declared in LeanPool/LeanModelChecking/ABWNBW.lean, line 323: “The Miyano-Hayashi breakpoint construction turns any alternating Büchi automaton over a finite state space into a nondeterministic Büchi automaton accepting the same language.” Its source, as the card gives it: “S. Miyano and T. Hayashi, Alternating finite automata on omega-words, Theoretical Computer Science 32 (1984), 321-330, doi:10.1016/0304-3975(84)90049-5”SafetyLivenessDecomposition.safety_liveness_decomposition(theorem), declared in LeanPool/LeanModelChecking/SafetyLivenessDecomposition.lean, line 99: “Every linear-time property is the intersection of a safety property and a liveness property.” Its source, as the card gives it: “B. Alpern and F. B. Schneider, Defining liveness, Information Processing Letters 21 (1985), 181-185, doi:10.1016/0020-0190(85)90056-0”
Project
- Authors: György Kurucz.
- Source: An Automata-Theoretic Approach to Linear Temporal Logic by Moshe Y. Vardi, doi:10.1007/3-540-60915-6_6.
- Project repository: kuruczgy/lean-model-checking.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 68Q60, 03B44, 68Q45.
- In Lean Pool: LeanPool/LeanModelChecking, from the card LeanPool/projects/lean-model-checking.yaml.
Sources
TheoremThe Johnson–Lindenstrauss Lemma and Quantized JL#
Formalizes the Johnson–Lindenstrauss lemma end to end — a Gaussian random projection preserves pairwise distances of a finite point set up to a (1 ± ε) factor, so a distortion-ε embedding of any m-point set exists once k is logarithmic in m — together with the quantized JL (QJL) one-bit sign sketch: unbiasedness of the asymmetric 1-bit estimator and its sub-Gaussian distortion bound.
Quoted from the card LeanPool/projects/johnson-lindenstrauss-lean.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
JL.johnson_lindenstrauss(theorem; a main declaration), declared in LeanPool/JohnsonLindenstraussLean/Lemma.lean, line 62: “The abstract probabilistic-method union bound — if the summed per-pair distortion-failure probability is below one, a distortion-preserving map exists.”JL.johnson_lindenstrauss_pointset(theorem; a main declaration), declared in LeanPool/JohnsonLindenstraussLean/EndToEnd.lean, line 65: “The end-to-end Johnson–Lindenstrauss lemma — a Gaussian random projection into k dimensions embeds any m-point set with (1 ± ε) distortion once k is logarithmic in m.” Its source, as the card gives it: “S. Dasgupta, A. Gupta, An elementary proof of a theorem of Johnson and Lindenstrauss, Random Structures and Algorithms 22 (2003), 60-65, doi:10.1002/rsa.10073.”JL.qjlEstimator_unbiased(theorem), declared in LeanPool/JohnsonLindenstraussLean/QJL.lean, line 257: “The QJL asymmetric 1-bit estimator is unbiased for the normalized inner product between key and query.” Its source, as the card gives it: “A. Zandieh, M. Daliri, I. Han, QJL: 1-Bit Quantized JL Transform for KV Cache Quantization with Zero Overhead, AAAI 2025, arXiv:2406.03482.”JL.qjlEstimator_concentration_exp(theorem), declared in LeanPool/JohnsonLindenstraussLean/QJLDistortion.lean, line 594: “Sub-Gaussian distortion bound for the QJL 1-bit estimator: deviation at least ε has probability at most 2·exp(-m·ε²/(π·‖q‖²)).” Its source, as the card gives it: “A. Zandieh, M. Daliri, I. Han, QJL: 1-Bit Quantized JL Transform for KV Cache Quantization with Zero Overhead, AAAI 2025, arXiv:2406.03482.”
Project
- Authors: claytomode.
- Source: Extensions of Lipschitz mappings into a Hilbert space by William B. Johnson, Joram Lindenstrauss, doi:10.1090/conm/026/737400.
- Project repository: claytomode/johnson-lindenstrauss-lean.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 68W20, 60G15, 68P05.
- In Lean Pool: LeanPool/JohnsonLindenstraussLean, from the card LeanPool/projects/johnson-lindenstrauss-lean.yaml.
Sources
TheoremMatrix multiplication exponent at most 9/4 over every field#
The arithmetic exponent of square matrix multiplication is at most 9/4 over every field. The proof preserves a general tensor-rank and arithmetic-program library, extends Fourier separation to positive characteristic, and descends finite tensor decompositions through algebraic extensions. For every positive epsilon it constructs correct division-free programs of cost at most C n^(9/4 + epsilon), with C uniform in the matrix size.
Quoted from the card LeanPool/projects/matrix-multiplication-all-fields.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
MatrixMultiplicationAllFields.omega_le_nine_quarters_all_fields(theorem; a main declaration), declared in LeanPool/MatrixMultiplicationAllFields.lean, line 117: “For every field F, the infimum of admissible arithmetic matrix multiplication exponents is at most 9/4.”MatrixMultiplicationAllFields.MatrixMultiplication.admissibleExponent_nine_quarters_all_fields(theorem), declared in LeanPool/MatrixMultiplicationAllFields/LinearAlgebra/MatrixMultiplication/AllFields/Main.lean, line 109: “Over every field F and for every epsilon > 0, a positive constant C bounds the cost of a correct division-free straight-line program for n by n matrix multiplication by C n^(9/4 + epsilon) for every n >= 1.”MatrixMultiplicationAllFields.MatrixMultiplication.matrix_multiplication_cost_le_all_fields(theorem), declared in LeanPool/MatrixMultiplicationAllFields/LinearAlgebra/MatrixMultiplication/AllFields/Main.lean, line 114: “The bound is realized by correct arithmetic programs at every positive matrix size, with a constant depending on the field and epsilon but not the size.”MatrixMultiplicationAllFields.MatrixMultiplication.AllFields.rankAtMost_of_map(theorem), declared in LeanPool/MatrixMultiplicationAllFields/LinearAlgebra/MatrixMultiplication/AllFields/Descent.lean, line 110: “A rank-R decomposition over a finite extension E/P of degree m descends to a rank at most m^3 R decomposition over P.”
Project
- Authors: OpenAI, Jeroen Zuiddam.
- Source: paper.
- Project repository: jzuiddam/omega-nine-quarters-all-fields, at commit 615b591c.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 68Q17, 15A69, 68Q25.
- In Lean Pool: LeanPool/MatrixMultiplicationAllFields, from the card LeanPool/projects/matrix-multiplication-all-fields.yaml.
Sources
DefinitionMRiscX#
A Hoare logic for verifying unstructured RISC-V-like assembly in Lean, following Lundberg et al. (SEFM 2020), with a certified interpreter, proved structural Hoare rules, per-instruction specifications, custom elaborators and tactics, and a complete One-Time-Pad correctness proof.
Quoted from the card LeanPool/projects/mriscx.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
hoareTripleUp(def; a main declaration), declared in LeanPool/MRiscX/Hoare/HoareCore.lean, line 91: “Defines the MRiscX Hoare triple, asserting that from any state satisfying the precondition the code reaches a successor state satisfying the postcondition while respecting the line whitelist and blacklist.” Its source, as the card gives it: “D. Lundberg, R. Guanciale, A. Lindner, M. Dam, Hoare-Style Logic for Unstructured Programs, SEFM 2020, doi:10.1007/978-3-030-58768-0_11.”S_SEQ(theorem; a main declaration), declared in LeanPool/MRiscX/Hoare/HoareRules.lean, line 134: “Proves the sequencing Hoare rule, peeling off the last instruction of a code block.” Its source, as the card gives it: “D. Lundberg, R. Guanciale, A. Lindner, M. Dam, Hoare-Style Logic for Unstructured Programs, SEFM 2020, doi:10.1007/978-3-030-58768-0_11.”PRE_STR(theorem), declared in LeanPool/MRiscX/Hoare/HoareRules.lean, line 207: “Proves the precondition-strengthening rule for MRiscX Hoare triples.”POST_WEAK(theorem), declared in LeanPool/MRiscX/Hoare/HoareRules.lean, line 224: “Proves the postcondition-weakening rule for MRiscX Hoare triples.”specification_LoadImmediate(theorem), declared in LeanPool/MRiscX/Semantics/Specification.lean, line 66: “Proves the per-instruction Hoare specification of the load-immediate instruction.”proof_otp(theorem; a main declaration), declared in LeanPool/MRiscX/Examples/OtpProof.lean, line 393: “Proves the full correctness of a One-Time-Pad implementation written in MRiscX assembly.”
Project
- Authors: Julius Marx.
- Source: doi:10.1007/978-3-030-58768-0_11.
- Project repository: JulsDE/MRiscX.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 68Q60.
- In Lean Pool: LeanPool/MRiscX, from the card LeanPool/projects/mriscx.yaml.
Sources
TheoremPolynomial-factor hardness of the closest vector problem#
Formalizes polynomial-factor NP-hardness of the closest vector problem through an explicit reduction from 3-SAT. The development also derives NP-hardness of binary nearest codeword, binary syndrome decoding, and finite p-norm variants of GapCVP. It includes machine-level polynomial-time bounds, binary encodings, affine systems, Reed--Solomon-style interpolation, and the lattice and coding-theory reductions needed by the final results.
Quoted from the card LeanPool/projects/gap-cvp.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
GapCVP.Comparator.gapCVP400IsNPHard(theorem; a main declaration), declared in LeanPool/GapCVP/Part18.lean, line 746: “GapCVP in the Euclidean norm with approximation factor n^(1/400), where n is the lattice dimension, is NP-hard as a promise problem: every NP language reduces in polynomial time to the promise problem on encoded well-formed instances (positive dimension, nonsingular integer basis, positive rational radius) with an integer target, whose YES instances have a lattice vector within the radius of the target and whose NO instances have every lattice vector at distance greater than n^(1/400) times the radius.”GapCVP.Comparator.binaryNearestCodewordIsNPHard(theorem), declared in LeanPool/GapCVP/Part18.lean, line 750: “Binary nearest codeword is NP-hard as a promise problem.”GapCVP.Comparator.binarySyndromeDecodingIsNPHard(theorem), declared in LeanPool/GapCVP/Part18.lean, line 757: “Binary syndrome decoding is NP-hard as a promise problem.”GapCVP.Comparator.finitePNormGapCVPIsNPHard(theorem), declared in LeanPool/GapCVP/Part18.lean, line 764: “For every rational p at least one, the finite p-norm version of GapCVP is NP-hard as a promise problem.”
Project
- Authors: OpenAI, Dean Cureton.
- Source: Ten Advances in Mathematics and Theoretical Computer Science by OpenAI.
- Project repository: openai/ten-proofs, at commit 94bc0feb.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 68Q17, 68Q25, 11H06, 94B35.
- In Lean Pool: LeanPool/GapCVP, from the card LeanPool/projects/gap-cvp.yaml.
Sources
TheoremPumping Lemma for Context-Free Grammars#
Formalizes the pumping lemma for context-free languages via parse trees of Chomsky-normal-form grammars and a pigeonhole argument.
Quoted from the card LeanPool/projects/pumping-cfg.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Language.IsContextFree.pumping(theorem; a main declaration), declared in LeanPool/PumpingCfg/Pumping.lean, line 343: “Every context-free language admits a pumping length p such that any word of length at least p decomposes as u v x y z with vy nonempty, vxy of length at most p, and u vⁱ x yⁱ z in the language for every i.”ChomskyNormalFormGrammar.pumping(lemma; a main declaration), declared in LeanPool/PumpingCfg/Pumping.lean, line 314: “The pumping lemma at the level of a Chomsky-normal-form grammar, obtained from a sufficiently tall parse tree with a repeated nonterminal.”
Project
- Authors: Alexander Loitzl, Martin Dvorak.
- Project repository: AlexLoitzl/pumping_cfg.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 68Q45.
- In Lean Pool: LeanPool/PumpingCfg, from the card LeanPool/projects/pumping-cfg.yaml.
Sources
TheoremPure Nock semantics, trace certificates, and polynomial fingerprints#
Formalizes Pure Nock nouns with natural-number leaves, operational semantics, evaluator soundness and completeness, verifiable crash behavior, modular evaluation and guarded natural-number bridges, execution trace certificates, and polynomial fingerprints over arbitrary finite fields. Distinct field-valued noun data have bounded fingerprint collision probability, with a union bound for tables sharing one random evaluation point. A computable Horner evaluator agrees with the polynomial fingerprint. The language and fingerprint closure excludes the framework's zkVM, AIR, RAP, table security theorem, and concrete Goldilocks field. Manuscript line references concern the upstream bundled draft v0.1.6, rather than the posted ePrint revision.
Quoted from the card LeanPool/projects/pure-nock.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Nock.Verb.runProgram_adequate_complete(theorem; a main declaration), declared in LeanPool/PureNock/PureComplete.lean, line 1156: “A subject and formula evaluate to a result under the small-step program machine with some finite fuel if and only if the derived paper evaluator produces that result with some finite fuel.”Nock.Verb.runTraceProgram_certificate(theorem), declared in LeanPool/PureNock/TraceCertificate.lean, line 225: “Every successfully emitted program trace is consistent and complete, every adjacent transition passes the Nock checker, and the final state is either terminal or has a crash edge accepted by the checker.”Nock.paper_field_bridge(theorem), declared in LeanPool/PureNock/PaperFieldBridge.lean, line 253: “For a modulus greater than one and inputs whose atoms are below the modulus, successful guarded evaluation produces the same bounded result under natural-number paper evaluation, modular paper evaluation, the full modular evaluator, the natural-number reference evaluator, and the small-step program machine with some finite fuel.”Nock.NPR.collision_prob_le(theorem; a main declaration), declared in LeanPool/PureNock/NPR.lean, line 521: “For nouns with at most Lambda leaves and distinct field-valued coefficient data or tree shapes, a uniformly selected point of a finite field makes their polynomial fingerprints coincide with probability at most 2 times (2 Lambda minus 1) divided by the field cardinality.”Nock.NPR.fnHorner_eq_fn(theorem), declared in LeanPool/PureNock/Fingerprint.lean, line 57: “The computable Horner fingerprint of every noun at every field evaluation point equals its polynomial fingerprint.”Nock.Verb.eval_crash_iff_invalid(theorem), declared in LeanPool/PureNock/Trace.lean, line 513: “The three-valued evaluator reports a crash at some finite fuel exactly when the initial verb has a complete trace ending at a stuck nonterminal state.”Nock.NPR.collision_table_prob_le(theorem), declared in LeanPool/PureNock/NPR.lean, line 641: “For a finite table of bounded-length nouns evaluated at one shared random field point, the probability that some pair with distinct field-valued data collides is at most the single-pair error times k times (k minus 1) divided by 2.”
Project
- Authors: Pure Nock formalization contributors.
- Contributors: Assimakis A. Kattis.
- Source: A Generic Compilation Framework for Efficiently Verifiable Virtual Machine Architectures (draft v0.1.6) by Assimakis A. Kattis, Brian Klatt, Philip Quirk, Logan Allen, manuscript.
- Project repository: nockchain/pure-nock-lean, at commit 4838863b.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 68Q55, 68Q60, 11T71.
- In Lean Pool: LeanPool/PureNock, from the card LeanPool/projects/pure-nock.yaml.
Sources
TheoremQuartic-over-logarithmic lower bound for rational permanent formulas#
Proves that every valid rational arithmetic formula over the complex numbers computing the n-by-n permanent, for n at least 32, has at least n^4 / (192 log_2 n) variable leaves. The development derives the bound through coefficient-field transcendence degree, Jacobian minors, matching-polynomial identities, and a cyclic block decomposition.
Quoted from the card LeanPool/projects/permanent-formula-lower-bound.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
PermanentFormulaLowerBound.permanent_rational_formula_logarithmic_lower_bound(theorem; a main declaration), declared in LeanPool/PermanentFormulaLowerBound.lean, line 6243: “For n at least 32, every valid rational formula over the complex numbers that computes the n-by-n permanent has at least n^4 / (192 log_2 n) variable leaves.”PermanentFormulaLowerBound.permanent_rational_formula_lower_bound(theorem), declared in LeanPool/PermanentFormulaLowerBound.lean, line 6222: “The same quartic-over-logarithmic lower bound controls variable leaves, total leaves, and vertices, and half that bound controls internal gates.”
Project
- Authors: OpenAI, Dean Cureton.
- Source: Ten Advances in Mathematics and Theoretical Computer Science by OpenAI.
- Project repository: openai/ten-proofs, at commit 94bc0feb.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 68Q17, 68Q25, 15A15.
- In Lean Pool: LeanPool/PermanentFormulaLowerBound, from the card LeanPool/projects/permanent-formula-lower-bound.yaml.
Sources
TheoremSharp list-scheduling and longest-processing-time bounds#
Formalizes identical-machine scheduling for arbitrary finite job sets with real processing times. Proves Graham's sharp list-scheduling and LPT approximation bounds, constructs their tight instances, characterizes all positive instances attaining the LPT bound, and establishes the supremum for every sufficiently large fixed job count.
Quoted from the card LeanPool/projects/graham-lpt.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
GrahamLPT.listSchedule_le_optMakespan(theorem), declared in LeanPool/GrahamLPT/ListBound.lean, line 60: “For nonnegative processing times on m nonzero identical machines, every list schedule has makespan at most (2 - 1/m) times the optimal makespan.”GrahamLPT.lpt_le_optMakespan(theorem; a main declaration), declared in LeanPool/GrahamLPT/LPTBound.lean, line 69: “For nonnegative processing times on m nonzero identical machines, every longest-processing-time-first schedule has makespan at most (4/3 - 1/(3m)) times the optimal makespan.”GrahamLPT.isLeast_lpt_ratio(theorem), declared in LeanPool/GrahamLPT/Ratio.lean, line 53: “For each nonzero machine count, 4/3 - 1/(3m) is the least universal approximation factor for LPT, over all finite nonnegative real job sets.”GrahamLPT.lpt_eq_bound_iff_graham(theorem; a main declaration), declared in LeanPool/GrahamLPT/LPTForm.lean, line 58: “For at least two machines and a nonempty set of positive-length jobs, an LPT schedule attains Graham's bound exactly if the instance is a positive scalar multiple and permutation of Graham's 2m + 1 jobs.”GrahamLPT.isLUB_lpt_ratio_of_card(theorem), declared in LeanPool/GrahamLPT/FixedCount.lean, line 247: “For a nonzero machine count and every fixed job count n at least 2m + 1, the supremum of LPT-to-optimum makespan ratios over positive instances with n jobs remains 4/3 - 1/(3m).”GrahamLPT.exists_isLPTSchedule(theorem), declared in LeanPool/GrahamLPT/Basic.lean, line 319: “Every finite real job-length vector on a nonzero number of machines admits an LPT schedule.”GrahamLPT.exists_listSchedule_le(theorem), declared in LeanPool/GrahamLPT/ListOptimum.lean, line 160: “Every assignment of nonnegative-length jobs is matched or improved by a list schedule in some ordering of the jobs.”
Project
- Authors: JD Jones.
- Source: Graham's bounds for list scheduling and LPT on identical machines by JD Jones.
- Project repository: JD-Jones-ASES/graham-lpt-lean, at commit c8ed035b.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
- MSC2020: 68M20, 90B35, 68W25.
- In Lean Pool: LeanPool/GrahamLPT, from the card LeanPool/projects/graham-lpt.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.