Sum of sets in several… to Weierstrass models and singular…
TheoremSum of sets in several dimensions#
Proves Ruzsa's lower bound for sumsets in R^D. If A and B are finite with B nonempty, |B| ≤ |A| and A + B of affine dimension d, then |A + B| ≥ |A| + Σ_{t=1}^{|B|-1} min(d, |A| - t), and this bound is attained in R^d whenever d ≥ 1 and |A| ≥ d + 1, so it is the exact minimum. Derives the asymmetric form of Freiman's lemma, |A + B| ≥ |A| + d|B| - d(d+1)/2. Defines the Freiman dimension of a finite subset of a commutative monoid, transfers the bound to sets with a Freiman model in R^r, and shows that a set X with |X + X| ≤ κ|X| has Freiman dimension at most 2κ - 1 and at most κ - 1 + κ(2κ - 1)/|X|.
Quoted from the card LeanPool/projects/sum-of-sets-in-several-dimensions.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.
SumOfSetsInSeveralDimensions.card_add_sum_min_le_card_add_of_finrank_span_sub_eq(theorem; a main declaration), declared in LeanPool/SumOfSetsInSeveralDimensions/LowerBound.lean, line 107: “For finite A, B ⊆ R^D with B nonempty and |B| ≤ |A|, if the differences of A + B span a space of dimension d, then |A| + Σ_{t=1}^{|B|-1} min(d, |A| - t) ≤ |A + B|.” Its source, as the card gives it: “Theorem 1.”SumOfSetsInSeveralDimensions.card_add_mul_card_le_card_add_add_of_le_finrank_span_sub(theorem; a main declaration), declared in LeanPool/SumOfSetsInSeveralDimensions/ClosedForm.lean, line 88: “For finite A, B ⊆ R^D with B nonempty and |B| ≤ |A|, and every d at most the dimension of the span of the differences of A + B, |A| + d|B| ≤ |A + B| + d(d+1)/2.” Its source, as the card gives it: “Corollary 1.1.”SumOfSetsInSeveralDimensions.sInf_card_add_eq_add_sum_min(theorem; a main declaration), declared in LeanPool/SumOfSetsInSeveralDimensions/MinCardAdd.lean, line 94: “For d ≥ 1, 1 ≤ m ≤ n and n ≥ d + 1, the least size of A + B over A, B ⊆ R^d with |A| = m, |B| = n and A + B of affine dimension d is n + Σ_{j=1}^{m-1} min(d, n - j).” Its source, as the card gives it: “Theorem 2, F_d(m, n) = G_d(m, n).”SumOfSetsInSeveralDimensions.sInf_card_add_of_finrank_span_sub_right_eq_add_sum_min(theorem), declared in LeanPool/SumOfSetsInSeveralDimensions/MinCardAdd.lean, line 103: “The same minimum n + Σ_{j=1}^{m-1} min(d, n - j) holds when only B is required to have affine dimension d.” Its source, as the card gives it: “Theorem 2, F'_d(m, n) = G_d(m, n).”SumOfSetsInSeveralDimensions.freimanDim_le_two_mul_sub_one_of_card_add_le(theorem; a main declaration), declared in LeanPool/SumOfSetsInSeveralDimensions/FreimanDimensionSumsetBounds.lean, line 277: “A nonempty finite subset X of a cancellative commutative monoid with |X + X| ≤ κ|X|, for a real κ, has Freiman dimension at most 2κ - 1.”SumOfSetsInSeveralDimensions.freimanDim_le_sub_one_add_mul_div_card_of_card_add_le(theorem), declared in LeanPool/SumOfSetsInSeveralDimensions/FreimanDimensionSumsetBounds.lean, line 313: “Under the same hypotheses, the Freiman dimension of X is at most κ - 1 + κ(2κ - 1)/|X|.”SumOfSetsInSeveralDimensions.card_add_sum_min_le_of_freimanDim_union(theorem), declared in LeanPool/SumOfSetsInSeveralDimensions/FreimanDimensionSumsetBounds.lean, line 251: “Ruzsa's lower bound holds for finite A, B in a commutative monoid with B nonempty and |B| ≤ |A|, with d replaced by r - 1, where r ≥ 1 is the Freiman dimension of A ∪ B.”
Project
- Authors: Gabriel Dahia.
- Source: Sum of sets in several dimensions by Imre Z. Ruzsa, doi:10.1007/BF01302969.
- Project repository: gdahia/SumOfSetsInSeveralDimensions, at commit bd2694b8.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11P70, 11B13, 11B75.
- In Lean Pool: LeanPool/SumOfSetsInSeveralDimensions, from the card LeanPool/projects/sum-of-sets-in-several-dimensions.yaml.
Sources
TheoremSums of Distinct Factorials That Are Powers of Two (Erdos Problem 403)#
Reconstructs the finiteness theorem for Erdos Problem 403: only finitely many sums of distinct factorials are powers of two, and every such power is at most 2^7 = 128 (the extremal solution 2! + 3! + 5! = 128). The sharp bound is proved in the factorial number system via a single fixed modulus 12!, with all computations kernel-pure.
Quoted from the card LeanPool/projects/erdos403.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.
Erdos403.erdos_403_sharp(theorem; a main declaration), declared in LeanPool/Erdos403/Sharp.lean, line 420: “Every power of two that is a sum of distinct factorials is at most 2^7, with 128 the largest solution.”Erdos403.erdos_403_finite(theorem; a main declaration), declared in LeanPool/Erdos403/Sharp.lean, line 427: “Only finitely many sums of distinct factorials are powers of two.”
Project
- Authors: Trevor Morris.
- Source: Erdos Problem 403: sums of distinct factorials that are powers of two by Trevor Morris, https://www.erdosproblems.com/403.
- Project repository: gotrevor/erdos-403.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11B83.
- In Lean Pool: LeanPool/Erdos403, from the card LeanPool/projects/erdos403.yaml.
Sources
TheoremSums of Three Squares#
Formalizes a blueprint step in the three-squares theorem using quadratic forms and geometry of numbers.
Quoted from the card LeanPool/projects/sumsthreesquares.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.
LeanPool.SumsThreeSquares.blueprint_case_mod8_eq3(theorem; a main declaration), declared in LeanPool/SumsThreeSquares/SumThreeSquares.lean, line 979: “Proves the mod-8-equals-3 blueprint case for the three-squares theorem.” Its source, as the card gives it: “H. Davenport, The geometry of numbers, The Mathematical Gazette 31 (1947), 206-210, doi:10.2307/3608159.”
Project
- Authors: Bhavik Mehta, Pietro Monticone, Abel Donate Munoz.
- Source: doi:10.1090/S0002-9939-1957-0085275-8.
- Project repository: pitmonticone/SumsThreeSquares.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 11E25, 11H06.
- In Lean Pool: LeanPool/SumsThreeSquares, from the card LeanPool/projects/sumsthreesquares.yaml.
Sources
TheoremThakur's hypotheses on power sums of F_q[t]#
Formalizes four components of Thakur's hypotheses on power sums over finite polynomial rings, including uniqueness and monotonicity results for the carry-free digit optimization problems and the Laurent-series expansion of finite-field power sums.
Quoted from the card LeanPool/projects/zeta-h123.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.
ZetaH123.H1.main_theorem(theorem; a main declaration), declared in LeanPool/ZetaH123/H1.lean, line 2404: “Proves uniqueness of the admissible base-q decomposition maximizing the H1 power-sum weight functional.”ZetaH123.H2.main(theorem), declared in LeanPool/ZetaH123/H2.lean, line 2130: “Proves the H2 unique-minimizer statement for the recursive digit/carry-free optimization problem defining the values s_d(k).”ZetaH123.H3.main_theorem(theorem), declared in LeanPool/ZetaH123/H3.lean, line 273: “Proves the H3 monotonicity statement that s_d(k) is strictly less than s_d(k+1) when p does not divide k.”ZetaH123.Lem41.main(theorem; a main declaration), declared in LeanPool/ZetaH123/Lem41.lean, line 1159: “Proves the Lemma 4.1 Laurent-series expansion for S_d(k), with nonzero coefficients indexed by the carry-free tuples.”
Project
- Authors: Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang.
- Source: Thakur's hypotheses on power sums of F_q[t] by Evan Chen, Ken Ono, arXiv:2606.16239.
- Project repository: AxiomMath/zeta-h123.
- 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: 11M38, 11T55, 11G09.
- In Lean Pool: LeanPool/ZetaH123, from the card LeanPool/projects/zeta-h123.yaml.
Sources
TheoremThe Three-Gap (Steinhaus) Theorem#
Formalizes the three-gap (Steinhaus, three-distance) theorem: for every real
aand everyN, theN-point orbit{i·a mod 1 : i < N}partitions[0,1)into gaps taking at most three distinct lengths, and when exactly three occur the largest is the sum of the other two. The proof works in[0,1)viaInt.fract(notAddCircle) through the two first-return timesη⁺andη⁻, and is uniform in the rotation number, covering rational and irrationalawith no case split.
Quoted from the card LeanPool/projects/three-gap-theorem.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.
SteinhausThreeGap.three_gap_card_le_three(theorem; a main declaration), declared in LeanPool/SteinhausThreeGap/Basic.lean, line 1471: “For every realaand naturalN, the gaps of the orbit{i·a mod 1 : i < N}take at most three distinct lengths.”SteinhausThreeGap.three_gap_lengths_eq(theorem), declared in LeanPool/SteinhausThreeGap/Basic.lean, line 1485: “When the gaps take exactly three distinct lengths, those lengths are precisely the two first returnsη⁺,η⁻, and their sumη⁺ + η⁻; in particular the largest gap is the sum of the other two.”
Project
- Authors: Dirk Kunert.
- Source: The Three Gap Theorem (Steinhaus Conjecture) by Tony van Ravenstein, doi:10.1017/S1446788700031062.
- Project repository: dkunert/three-gap-theorem-lean.
- 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 Dirk Kunert”.
- MSC2020: 11K06.
- In Lean Pool: LeanPool/SteinhausThreeGap, from the card LeanPool/projects/three-gap-theorem.yaml.
Sources
TheoremThe transcendence of π#
Formalizes a self-contained proof, following Niven's 1939 argument, that the real and complex number π is transcendental over the rationals.
Quoted from the card LeanPool/projects/istranscendentalpi.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.
IsTranscendentalPi(theorem; a main declaration), declared in LeanPool/IsTranscendentalPi/Main.lean, line 50: “Proves that the complex number π is transcendental over ℚ.”IsTranscendentalPiReal(theorem; a main declaration), declared in LeanPool/IsTranscendentalPi/Main.lean, line 117: “Proves that the real number π is transcendental over ℚ.”isAlgebraic_I_mul_pi_of_isAlgebraic_pi(lemma), declared in LeanPool/IsTranscendentalPi/Main.lean, line 38: “Shows that if π is algebraic over ℚ then so is iπ.”exists_monic_rat_poly_aeval_Ipi_eq_zero(lemma), declared in LeanPool/IsTranscendentalPi/Main.lean, line 43: “Produces a monic rational polynomial vanishing at iπ when iπ is algebraic.”
Project
- Authors: James Huang, Samuël Borza.
- Project repository: samuelborza/IsTranscendentalPi.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 11A41.
- In Lean Pool: LeanPool/IsTranscendentalPi, from the card LeanPool/projects/istranscendentalpi.yaml.
Sources
StructureWeierstrass models and singular points for Tate's algorithm#
Formalizes Weierstrass models of elliptic curves over a commutative ring, their b- and c-invariants and discriminant, the change-of-coordinates group action, the discriminant's membership in the Jacobian ideal, and the construction of the singular point of a singular model over a perfect field, together with the Kronecker symbol and the Kodaira type enumeration.
Quoted from the card LeanPool/projects/ec-tate-lean.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 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.
Model(structure; a main declaration), declared in LeanPool/EcTateLean/Algebra/EllipticCurve/Model.lean, line 46: “Defines a Weierstrass model of a possibly singular elliptic curve by its five a-invariants.”Model.discr_identity(lemma), declared in LeanPool/EcTateLean/Algebra/EllipticCurve/Model.lean, line 98: “Proves the identity relating the discriminant to the c-invariants, 1728 * discr = c4^3 - c6^2.”Model.rst_discr(lemma), declared in LeanPool/EcTateLean/Algebra/EllipticCurve/Model.lean, line 202: “Proves that the discriminant is invariant under the rst change-of-coordinates transformation.”Model.discr_in_jacobian_ideal(lemma), declared in LeanPool/EcTateLean/Algebra/EllipticCurve/Model.lean, line 275: “Expresses the discriminant as an explicit combination of the Weierstrass polynomial and its partial derivatives, witnessing membership in the Jacobian ideal.”Model.discr_eq_zero_of_singular(lemma), declared in LeanPool/EcTateLean/Algebra/EllipticCurve/Model.lean, line 440: “Proves that a model with a singular point has vanishing discriminant.”Model.Field.isSingularPoint_singularPoint(lemma; a main declaration), declared in LeanPool/EcTateLean/Algebra/EllipticCurve/Model.lean, line 523: “Proves that the explicitly constructed singular point of a singular model over a perfect field is indeed a singular point (Connell, Proposition 1.5.4).” Its source, as the card gives it: “Ian Connell, Elliptic Curve Handbook, February 1999, Proposition 1.5.4.”Model.Field.move_singular_point_to_origin, which the scan does not find declared in the project's files at this commit: “Proves that the change of coordinates moving the singular point places it at the origin.”Kodaira(inductive), declared in LeanPool/EcTateLean/Algebra/EllipticCurve/KodairaTypes.lean, line 24: “Enumerates the Kodaira reduction types, including the extra types arising over imperfect residue fields of characteristic 2 or 3.”
Project
- Authors: Sacha H., Sander R. Dahmen, Anne Baanen, Alex J. Best.
- Source: Elliptic Curve Handbook by Ian Connell, https://www.math.rug.nl/~top/ian.pdf.
- Project repository: KisaraBlue/ec-tate-lean.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 11G05, 11G07, 14H52.
- In Lean Pool: LeanPool/EcTateLean, from the card LeanPool/projects/ec-tate-lean.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.