Nair–Tenenbaum short sums of… to Square-difference-free…
TheoremNair–Tenenbaum short sums of arithmetic functions#
Uniform upper bounds for arithmetic functions at polynomial values in short intervals, including prime arguments, arithmetic progressions, Hooley moments, smooth values and Goldbach upper bounds. Preserves the sieve, polynomial-root, number-field counting and lattice-discrepancy infrastructure. Includes a counterexample to the printed Lemma 1, replacement comparisons used by the main proofs, and the nonconstant-coordinate restriction for Corollary 6.
Quoted from the card LeanPool/projects/nair-tenenbaum-short-sums.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.
NairTenenbaum.theoremOne_for_families(theorem; a main declaration), declared in LeanPool/NairTenenbaum/Results/FamilyTheorems.lean, line 42: “For an integer polynomial family of positive total degree with no fixed prime divisor, short sums of admissible nonnegative arithmetic functions satisfy the Nair–Tenenbaum sieve bound in its degree-dependent interval range. The height threshold is independent of the coefficients and discriminant; the bound constant depends on the restricted discriminant. Factorization data are constructed from the original family.”NairTenenbaum.theoremTwo(theorem), declared in LeanPool/NairTenenbaum/Results/TheoremTwo.lean, line 29: “For any nonconstant irreducible integer polynomial Q and integer k greater than its degree, the greatest prime factor of the product of its values over (x, x + y], with y = x^(degree(Q)/k), eventually exceeds y times exp((log x)^alpha), for each alpha < 2 - log 4.”NairTenenbaum.theoremThree_for_families(theorem), declared in LeanPool/NairTenenbaum/Results/PrimeFamilyTheorem.lean, line 31: “Under the same family and growth hypotheses, with nonzero constant term of the product polynomial, the corresponding bound holds at prime arguments. The constant-term correction is explicit and factorization data are constructed from the original family.”NairTenenbaum.lemmaTwo(theorem), declared in LeanPool/NairTenenbaum/Results/LemmaTwo.lean, line 125: “The smooth-weight tail estimate holds for general scalar class-M weights, with the stated cutoff, convergent series and uniform constant.”
Project
- Authors: Jason Davies.
- Source: Short sums of certain arithmetic functions by Mohan Nair, Gérald Tenenbaum, doi:10.1007/BF02392880.
- Project repository: jasondavies/nair-tenenbaum-short-sums, at commit 0102e310.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11N37, 11N36, 11N25, 11N32.
- In Lean Pool: LeanPool/NairTenenbaum, from the card LeanPool/projects/nair-tenenbaum-short-sums.yaml.
Sources
TheoremNeukirch's Algebraic Number Theory: Hilbert ramification theory#
Formalizes Hilbert's ramification theory for Galois extensions of number fields, including the fundamental identity and the decomposition and inertia groups, ported from the jjdishere/neukirch project.
Quoted from the card LeanPool/projects/neukirch.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.
NumberField.ramificationIdx_mul_inertiaDegOfIsGalois(theorem; a main declaration), declared in LeanPool/Neukirch/HilbertRamificationTheory.lean, line 753: “Proves the fundamental identity g·e·f = [L : K] for a Galois extension of number fields.”NumberField.finrank_eq_ramificationIdx_mul_inertiaDeg(theorem), declared in LeanPool/Neukirch/HilbertRamificationTheory.lean, line 1145: “Shows that when P is the unique prime over p, the degree [L : K] equals the ramification index times the inertia degree.”NumberField.IsMaximal_conjugates(theorem), declared in LeanPool/Neukirch/HilbertRamificationTheory.lean, line 566: “Proves the Galois group acts transitively on the primes lying over a fixed prime.”NumberField.DecompositionGroup_card_eq_ramificationIdx_mul_inertiaDeg(theorem), declared in LeanPool/Neukirch/HilbertRamificationTheory.lean, line 821: “Computes the order of the decomposition group as the product of the ramification index and inertia degree.”NumberField.InertiaFieldAutEquivResidueFieldAut(def), declared in LeanPool/Neukirch/HilbertRamificationTheory.lean, line 1133: “Identifies the Galois group of the inertia field over K with the Galois group of the residue field extension.”NumberField.InertiaGroup_card_eq_ramificationIdx(theorem), declared in LeanPool/Neukirch/HilbertRamificationTheory.lean, line 1293: “Computes the order of the inertia group as the ramification index of p in L.”Ideal.ramificationIdx_algebra_tower_of_eq(theorem), declared in LeanPool/Neukirch/ExtensionOfDedekindDomains.lean, line 34: “Proves multiplicativity of the ramification index in a tower of Dedekind domains.”Ideal.inertiaDeg_algebra_tower_of_eq(theorem), declared in LeanPool/Neukirch/ExtensionOfDedekindDomains.lean, line 65: “Proves multiplicativity of the inertia degree in a tower of Dedekind domains.”
Project
- Authors: Hu Yongle.
- Source: doi:10.1007/978-3-662-03983-0.
- Project repository: jjdishere/neukirch.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 11R32, 11S15, 13B25.
- In Lean Pool: LeanPool/Neukirch, from the card LeanPool/projects/neukirch.yaml.
Sources
TheoremNewman normalizer bounds for congruence subgroups#
Characterizes the normalizer of Gamma0(N) in SL(2, R), for every positive level N, by explicit integral matrices scaled by a square root. Extends the necessary matrix form to GammaDelta(N) for every subgroup Delta of the units modulo N. Preserves Atkin-Lehner elements, rational representatives, integral matrix lattices, prime valuations and a generic normalizer argument. The upstream finite presentations, group orders and modular-curve automorphism classifications are outside this import's scope.
Quoted from the card LeanPool/projects/congruence-normalizers.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 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.
CongruenceNormalizers.newman_iff(theorem; a main declaration), declared in LeanPool/CongruenceNormalizers.lean, line 36: “For N > 0, put h = 2^min(3, floor(v_2(N)/2)) times 3^min(1, floor(v_3(N)/2)) and n = N/h^2. A real determinant-one matrix normalizes Gamma0(N) exactly when it equals plus or minus 1/sqrt(e) times [[a*e, b/h], [N*c/h, d*e]], for integers a, b, c, d and a positive divisor e of n satisfying a*d*e^2 - b*c*n = e.”CongruenceNormalizers.newman_delta(theorem; a main declaration), declared in LeanPool/CongruenceNormalizers.lean, line 41: “For N > 0 and Delta a subgroup of the units modulo N, let epsilon be gcd(N, u^2 - 1 for representatives u in Delta), and let h be the product over primes p dividing N of p^min(v_p(epsilon), floor(v_p(N)/2)). Every determinant-one real matrix normalizing GammaDelta(N) has the same integral Newman form with this h and n = N/h^2. This is a necessary bound; no converse for GammaDelta(N) is asserted.”CongruenceNormalizers.hPart_isGreatest'(theorem), declared in LeanPool/CongruenceNormalizers/NormalizerLean/Basic.lean, line 199: “At every positive level, h(N) is the greatest divisor of 24 whose square divides N.”
Project
- Authors: Filip Najman.
- Source: The normalizer of Gamma0(N) in PSL(2, R) by M. Akbas, D. Singerman, doi:10.1017/S001708950000940X.
- Project repository: F-Najman/normalizer-lean, at commit ea4445c0.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11F06, 20H05.
- In Lean Pool: LeanPool/CongruenceNormalizers, from the card LeanPool/projects/congruence-normalizers.yaml.
Sources
TheoremOn the paucity of lattice triangles#
Formalizes an analytic lower bound used in the paucity theorem for lattice triangles.
Quoted from the card LeanPool/projects/lattice-triangle.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.
analyticEngine_lower_bound(theorem; a main declaration), declared in LeanPool/LatticeTriangle/Solution.lean, line 6894: “Proves the analytic-engine lower bound underlying the lattice-triangle result.”
Project
- Authors: Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang.
- Source: arXiv:2603.23928.
- Project repository: AxiomMath/lattice-triangle.
- 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 Axiom Math”.
- MSC2020: 11H06, 11B30.
- In Lean Pool: LeanPool/LatticeTriangle, from the card LeanPool/projects/lattice-triangle.yaml.
Sources
TheoremThe optimal exponent relating sumsets and difference sets#
For a finite integer set A with at least two elements, proves that C(A) = log(|A+A|/|A|) / log(|A-A|/|A|) is strictly below 2, while explicit finite sets have exponents tending to 2. Thus 2 is the supremum and is never attained. Also gives an explicit witness within 10^(-999) of 2. This imports the upstream base-39 row-and-column variant, not the paper's base-12 automaton construction or its quantitative cardinality estimates. Supporting infrastructure includes injective digit expansions and the strict Pluennecke-Petridis equality argument for finite integer sets.
Quoted from the card LeanPool/projects/sum-difference-exponent.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.
SumDifferenceExponent.growthExponent_lt_two(theorem), declared in LeanPool/SumDifferenceExponent/Basic.lean, line 449: “For every finite set A of integers with at least two elements, log(|A+A|/|A|) / log(|A-A|/|A|) is strictly less than 2.”SumDifferenceExponent.tendsto_growthExponent_approximatingSet(theorem), declared in LeanPool/SumDifferenceExponent/Main.lean, line 37: “The growth exponents of the explicit finite integer sets approximatingSet l converge to 2 as l tends to infinity; these sets have at least two elements whenever l is positive.”SumDifferenceExponent.isLUB_admissibleExponents(theorem), declared in LeanPool/SumDifferenceExponent/Main.lean, line 53: “The number 2 is the least upper bound of the growth exponents of all finite integer sets with at least two elements.”SumDifferenceExponent.sSup_admissibleExponents(theorem; a main declaration), declared in LeanPool/SumDifferenceExponent/Main.lean, line 67: “The supremum of the growth exponents of all finite integer sets with at least two elements equals 2.”SumDifferenceExponent.supremum_not_attained(theorem), declared in LeanPool/SumDifferenceExponent/Main.lean, line 77: “No finite integer set with at least two elements has growth exponent equal to 2.”SumDifferenceExponent.quantitative_example(theorem), declared in LeanPool/SumDifferenceExponent/Quantitative.lean, line 131: “The explicitly defined finite integer set quantitativeSet has growth exponent strictly between 2 - 10^(-999) and 2.”
Project
- Authors: Haowei Lin, Shanda Li.
- Source: Settling the Optimal Exponent Relating Sumsets and Difference Sets by Haowei Lin, Shanda Li, arXiv:2607.27199.
- Project repository: linhaowei1/sum-diff-proof, at commit f53f8422.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11B13, 11B30, 05D10.
- In Lean Pool: LeanPool/SumDifferenceExponent, from the card LeanPool/projects/sum-difference-exponent.yaml.
Sources
TheoremPoitou's Explicit Odlyzko Bound for Root Discriminants#
Formalizes the unconditional explicit-formula argument for a lower bound on root discriminants of totally complex number fields. Develops the completed Dedekind zeta function and its functional equation, Poitou's explicit formula, the Tartar test function, and a certified numerical estimate proving that degree at least 18 forces root discriminant at least 8.25.
Quoted from the card LeanPool/projects/odlyzko-bound.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.
NumberField.Odlyzko.odlyzkoBound(theorem; a main declaration), declared in LeanPool/Odlyzko/ExplicitFormula/PoitouEstimate.lean, line 1666: “Proves that every totally complex number field of degree at least 18 has absolute discriminant at least 8.25 raised to its degree.” Its source, as the card gives it: “Georges Poitou, Sur les petits discriminants, equation (26) and the table on p. 17; Lean source adapted from ImperialCollegeLondon/FLT commit 01370b013e55c83f1994af814cd31cb8fb2ef653.”
Project
- Authors: The FLT Project, √2.
- Source: Sur les petits discriminants by Georges Poitou, https://www.numdam.org/item/SDPP_1976-1977__18_1_A6_0/.
- Project repository: ImperialCollegeLondon/FLT.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11R29, 11R42.
- In Lean Pool: LeanPool/Odlyzko, from the card LeanPool/projects/odlyzko-bound.yaml.
Sources
TheoremPolynomial ABC (Mason–Stothers) and its corollaries#
Formalizes the Mason–Stothers theorem (the polynomial ABC theorem) and derives the polynomial Fermat's Last Theorem, the Fermat–Catalan inequality, Davenport's theorem, and a no-parametrization corollary.
Quoted from the card LeanPool/projects/lean-poly-abc.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 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.
LeanPolyABC.Polynomial.abc(theorem; a main declaration), declared in LeanPool/LeanPolyABC/MasonStothers.lean, line 136: “Mason–Stothers — for coprime non-constant polynomials with a+b=c, the max degree is below the degree of the radical of abc.”LeanPolyABC.Polynomial.flt(theorem; a main declaration), declared in LeanPool/LeanPolyABC/Corollaries/FltCatalan.lean, line 233: “The polynomial Fermat's Last Theorem — no nontrivial coprime polynomial solutions of aⁿ+bⁿ=cⁿ for n ≥ 3.”LeanPolyABC.Polynomial.flt_catalan(theorem), declared in LeanPool/LeanPolyABC/Corollaries/FltCatalan.lean, line 211: “The polynomial Fermat–Catalan inequality bounding solutions of aᵖ+bᵍ=cʳ.”
Project
- Authors: Seewoo Lee.
- Source: Formalization of Polynomial ABC and FLT, arXiv:2408.15180.
- Project repository: seewoo5/lean-poly-abc.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 11C08, 12E05.
- In Lean Pool: LeanPool/LeanPolyABC, from the card LeanPool/projects/lean-poly-abc.yaml.
Sources
TheoremPolynomial degree bounds for rational points on varieties#
Proves the six main results of Castryck, Cluckers, Dittmann and Nguyen on dimension growth, uniform rational-point counts on curves and hypersurfaces, a lower-bound curve construction, and two-torsion in number-field class groups. Preserves the determinant method, Hilbert-function degree and dimension, bounded birational projections, and the required Bombieri-Vaaler and Mertens dependencies. Imports the main-result closure, excluding the separate intermediate-statement and counterexample library.
Quoted from the card LeanPool/projects/ccdn-dimension-growth.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.
CCDN.projective_dimension_growth(theorem; a main declaration), declared in LeanPool/CCDN/ProjectiveDimensionGrowth.lean, line 141: “For every ambient projective dimension n, a constant depending only on n bounds the rational points of height at most B on every integral projective variety of degree d at least five by C d^(2n^2+5n-5) B^dim(X), for B at least one.”CCDN.projectiveCurveBound(theorem), declared in LeanPool/CCDN/ProjectiveCurveBound.lean, line 25: “In ambient dimension n at least two and for B at least one, every integral projective curve of degree d has at most C(n) d^4 B^(2/d) rational points of height at most B, uniformly in its coefficients.”CCDN.affineCurveBound(theorem), declared in LeanPool/CCDN/AffineCurveBound.lean, line 24: “In ambient dimension n at least two and for B at least one, every integral affine curve of degree d has at most C(n) d^3 B^(1/d) (log B+d) integer points in the box of radius B.”CCDN.affine_hypersurface_dimension_growth(theorem), declared in LeanPool/CCDN/AffineHypersurfaceDimensionGrowth.lean, line 27: “In N at least three variables, an affine hypersurface of degree d at least five whose top form is absolutely irreducible has at most C(N) d^(3N+9) B^(N-2) integer points in the box of radius B, for B at least one.”CCDN.projective_integral_curve_lower_bound(theorem), declared in LeanPool/CCDN/ProjectiveCurveLowerBound.lean, line 28: “For every positive degree d, an integral projective plane curve and a radius B at least one attain at least d^2 B^(2/d)/5 rational points of height at most B.”CCDN.classGroup_two_torsion_bound(theorem), declared in LeanPool/CCDN/ClassGroupBound.lean, line 30: “For number fields K of degree n at least three, the two-torsion cardinality is at most C(n) |disc K|^(1/2-1/(2n)) (log |disc K|)^(1-(n mod 2)).”
Project
- Authors: Jason Davies, Ralf Stephan, PrimeNumberTheoremAnd contributors.
- Source: The dimension growth conjecture, polynomial in the degree and without logarithmic factors, doi:10.2140/ant.2020.14.2261, arXiv:1904.13109.
- Project repository: jasondavies/ccdn-dimension-growth, at commit bb025e72.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11D45, 14G05, 11R29.
- In Lean Pool: LeanPool/CCDN, from the card LeanPool/projects/ccdn-dimension-growth.yaml.
Sources
TheoremThe polynomial Freiman–Ruzsa conjecture#
Formalizes Marton's polynomial Freiman–Ruzsa conjecture by the entropy method, including the characteristic-two bounds with exponents twelve and nine, the bounded-torsion theorem with an explicit exponent, and quantitative consequences for affine dimension and approximate homomorphisms. The supporting development builds entropic Ruzsa distance, multidistance, conditional entropy, and additive-energy machinery. This optimized import reuses the pooled Zhang–Yeung entropy and kernel library in place of duplicate upstream modules while preserving all six closed headline statements.
Quoted from the card LeanPool/projects/polynomial-freiman-ruzsa.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.
Marton.pfr_conjecture(theorem; a main declaration), declared in LeanPool/PFR/Solution.lean, line 43: “A nonempty finite set A of doubling at most K in an abelian group of exponent two is covered by fewer than 2 K^12 cosets of a finite subgroup no larger than A.”Marton.pfr_conjecture_nine(theorem), declared in LeanPool/PFR/Solution.lean, line 59: “Strengthens the characteristic-two covering theorem to fewer than 2 K^9 cosets of a finite subgroup no larger than A.”Marton.torsion_pfr_conjecture(theorem), declared in LeanPool/PFR/Solution.lean, line 99: “In an abelian group of exponent m at least two, a nonempty finite set of doubling at most K is covered by fewer than m K^(256 m^3 + 1) cosets of a subgroup no larger than A.”Marton.weak_pfr_int(theorem), declared in LeanPool/PFR/Solution.lean, line 109: “A nonempty finite set of doubling at most K in a finite-rank free abelian group has a subset of relative size at least K^(-34) and affine dimension at most (80 / log 2) log K.”Marton.homomorphism_pfr(theorem), declared in LeanPool/PFR/Solution.lean, line 149: “A map between finite abelian groups of exponent two whose additive defects lie in S differs from a homomorphism by a map taking at most |S|^10 values.”Marton.approx_hom_pfr(theorem), declared in LeanPool/PFR/Solution.lean, line 179: “A map between finite abelian groups of exponent two that is additive on at least a 1/K fraction of pairs agrees with a homomorphism on at least (|G| / (2^144 K^122) - 1) / 2 points.”
Project
- Authors: PFR contributors.
- Contributors: Aaron Anderson, Mantas Bakšys, Jonas Bayer, Mauricio Collares, Rémy Degenne, Yaël Dillies, Bhavik Mehta, Ella Yu, Ben Eltschig, Sébastien Gouëzel, Kalle Kytölä, Rob Lewis, Paul Lezeau, Lorenzo Luccioli, Heather Macbeth, Patrick Massot, Arend Mellendijk, Kyle Miller, Pietro Monticone, Kim Morrison, Oliver Nash, Utensil Song, Terence Tao, Floris van Doorn, Sky Wilshaw, Lawrence Wu.
- Source: Marton's conjecture (the polynomial Freiman–Ruzsa conjecture) by W. T. Gowers, Ben Green, Freddie Manners, Terence Tao, arXiv:2311.05762.
- Project repository: teorth/pfr, at commit 07839bdd.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 11B30, 11P70, 20K01, 94A17.
- In Lean Pool: LeanPool/PFR, from the card LeanPool/projects/polynomial-freiman-ruzsa.yaml.
Sources
TheoremThe polynomial method and restricted sums of congruence classes#
Formalizes the polynomial method (Alon–Tarsi-style combinatorial Nullstellensatz arguments) and applies it to restricted sums of congruence classes, including Cauchy–Davenport, Dias da Silva–Hamidoune, and a Vandermonde coefficient formula.
Quoted from the card LeanPool/projects/polynomial-method-restricted-sums.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.
ANR_polynomial_method(theorem; a main declaration), declared in LeanPool/PolynomialMethodRestrictedSums/ANRPolynomialMethod.lean, line 1073: “The Alon–Nathanson–Rusza polynomial method theorem, giving a non-vanishing-coefficient criterion for restricted sums.” Its source, as the card gives it: “N. Alon, M. B. Nathanson, I. Z. Ruzsa, The polynomial method and restricted sums of congruence classes, J. Number Theory 56 (1996), 404-417, doi:10.1006/jnth.1996.0029.”cauchy_davenport(theorem; a main declaration), declared in LeanPool/PolynomialMethodRestrictedSums/CauchyDavenportTheorem.lean, line 193: “The Cauchy–Davenport theorem on sums of subsets of the cyclic group of prime order.” Its source, as the card gives it: “N. Alon, Combinatorial Nullstellensatz, Combinatorics, Probability and Computing 8 (1999), 7-29, doi:10.1017/S0963548398003411.”dias_da_silva_hamidoune(theorem; a main declaration), declared in LeanPool/PolynomialMethodRestrictedSums/DiasDaSilvaHamidoune.lean, line 102: “The Dias da Silva–Hamidoune lower bound for restricted sums of distinct elements in a prime cyclic group.” Its source, as the card gives it: “J. A. Dias da Silva, Y. O. Hamidoune, Cyclic spaces for Grassmann derivatives and additive theory, Bull. London Math. Soc. 26 (1994), 140-146, doi:10.1112/blms/26.2.140.”restricted_sum_distinct_sizes(theorem), declared in LeanPool/PolynomialMethodRestrictedSums/RestrictedSumDistinctSizes.lean, line 293: “A lower bound for restricted sums when the summand sets have distinct sizes.” Its source, as the card gives it: “N. Alon, M. B. Nathanson, I. Z. Ruzsa, The polynomial method and restricted sums of congruence classes, J. Number Theory 56 (1996), 404-417, doi:10.1006/jnth.1996.0029.”Vandermonde_coefficient_formula(theorem), declared in LeanPool/PolynomialMethodRestrictedSums/VandermondeCoefficientFormula.lean, line 553: “A closed-form expression for a specific Vandermonde-style coefficient used by the polynomial method.” Its source, as the card gives it: “N. Alon, M. B. Nathanson, I. Z. Ruzsa, The polynomial method and restricted sums of congruence classes, J. Number Theory 56 (1996), 404-417, doi:10.1006/jnth.1996.0029.”
Project
- Authors: Nick Adfor.
- Project repository: NickAdfor/The-polynomial-method-and-restricted-sums-of-congruence-classes.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 11B30, 11B75, 11P70.
- In Lean Pool: LeanPool/PolynomialMethodRestrictedSums, from the card LeanPool/projects/polynomial-method-restricted-sums.yaml.
Sources
TheoremPolynomial parametrizations of Pythagorean triples#
Formalizes Frisch and Vaserstein's result that Pythagorean triples are not parametrizable by one triple of integer-coefficient polynomials in any number of variables, but are parametrizable by a single triple of integer-valued rational polynomials, including the positive and sixteen-parameter variants.
Quoted from the card LeanPool/projects/pythagorean-polynomial-parametrization.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.
LeanPool.PythagoreanPolynomialParametrization.no_int_poly_parametrization(theorem), declared in LeanPool/PythagoreanPolynomialParametrization/Obstructions.lean, line 74: “Proves that no single triple of integer-coefficient polynomials in any number of variables parametrizes all Pythagorean triples.”LeanPool.PythagoreanPolynomialParametrization.exists_int_valued_parametrization(theorem; a main declaration), declared in LeanPool/PythagoreanPolynomialParametrization/IntegerValued.lean, line 124: “Gives the explicit four-variable integer-valued polynomial parametrization of all Pythagorean triples.”LeanPool.PythagoreanPolynomialParametrization.positive_triples_parametrization(theorem), declared in LeanPool/PythagoreanPolynomialParametrization/Positive.lean, line 146: “Formalizes the positive Pythagorean-triple parametrization with positive parameters and a nonnegative auxiliary parameter.”LeanPool.PythagoreanPolynomialParametrization.exists_16_param_parametrization(theorem), declared in LeanPool/PythagoreanPolynomialParametrization/Positive.lean, line 351: “Converts the positive parametrization to an unrestricted sixteen-integer-parameter parametrization using the four-square theorem.”LeanPool.PythagoreanPolynomialParametrization.single_intValued_parametrization_yields_finite_intPoly_parametrization(theorem), declared in LeanPool/PythagoreanPolynomialParametrization/Explanatory.lean, line 203: “Proves the cited reduction from one integer-valued polynomial tuple to finitely many integer-coefficient polynomial tuples.”LeanPool.PythagoreanPolynomialParametrization.integerValued_polynomial_ring_not_uniqueFactorization(theorem), declared in LeanPool/PythagoreanPolynomialParametrization/Explanatory.lean, line 354: “Records the integer-valued polynomial ring non-UFD phenomenon behind the paper's motivating discussion.”
Project
- Authors: Lazar Milikic.
- Source: Parametrization of Pythagorean triples by a single triple of polynomials by Sophie Frisch, Leonid Vaserstein, doi:10.1016/j.jpaa.2007.05.019, arXiv:0706.0290.
- Project repository: epfl-lara/AutoformalizedProjects.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11D09, 11D85, 13F20.
- In Lean Pool: LeanPool/PythagoreanPolynomialParametrization, from the card LeanPool/projects/pythagorean-polynomial-parametrization.yaml.
Sources
TheoremPrimitive Sets Above x (Erdos Problem 1196)#
Formalizes Math Inc.'s proof around primitive sets above x for Erdos Problem 1196.
Quoted from the card LeanPool/projects/erdos1196.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.
PrimitiveSetsAboveX.mainTheorem(theorem; a main declaration), declared in LeanPool/Erdos1196/Main.lean, line 58: “Proves the main primitive-sets-above-x theorem.”Erdos1196.erdos_1196(theorem; a main declaration), declared in LeanPool/Erdos1196/FormalConjecturesErdos1196.lean, line 69: “States the formalized version of Erdos Problem 1196.”
Project
- Authors: Math Inc..
- Source: arXiv:2605.00301.
- Project repository: math-inc/Erdos1196.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11N25, 05D05.
- In Lean Pool: LeanPool/Erdos1196, from the card LeanPool/projects/erdos1196.yaml.
Sources
TheoremQuadratic-order prime classification#
Formalizes foundational algebra for quadratic orders associated to discriminants, including their power basis, norm and discriminant identities, odd-prime splitting/ramification/inertness criteria via Legendre symbols, and root-counting results for quadratic congruences modulo odd prime powers.
Quoted from the card LeanPool/projects/singular-moduli.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.
QuadraticOrder.prime_inert_iff(theorem; a main declaration), declared in LeanPool/SingularModuli/QuadraticOrder/Prime/Inert.lean, line 83: “Proves that for an odd rational prime p and a valid discriminant d, the ideal (p) is maximal in the quadratic order O_d exactly when the Legendre symbol (d/p) is -1.” Its source, as the card gives it: “C. Geiger, Singular Moduli and the Ideal Class Group, Section 3.2, Proposition 3.2.1.”QuadraticOrder.prime_ramified_iff(theorem), declared in LeanPool/SingularModuli/QuadraticOrder/Prime/Ramified.lean, line 175: “Proves that for an odd rational prime p and a valid discriminant d, the ideal (p) is not radical in O_d exactly when p divides d.” Its source, as the card gives it: “C. Geiger, Singular Moduli and the Ideal Class Group, Section 3.2, Proposition 3.2.1.”QuadraticOrder.prime_split_iff(theorem; a main declaration), declared in LeanPool/SingularModuli/QuadraticOrder/Prime/Split.lean, line 48: “Proves that for an odd rational prime p and a valid discriminant d, the ideal (p) is radical but not maximal exactly when the Legendre symbol (d/p) is 1.” Its source, as the card gives it: “C. Geiger, Singular Moduli and the Ideal Class Group, Section 3.2, Proposition 3.2.1.”QuadraticOrder.cardSqrts_prime_pow_coprime(theorem), declared in LeanPool/SingularModuli/QuadraticOrder/RootCounting.lean, line 405: “Counts roots of x^2 = c modulo p^n for odd prime p and p not dividing c, giving two roots when the Legendre symbol is 1 and none otherwise.” Its source, as the card gives it: “C. Geiger, Singular Moduli and the Ideal Class Group, Section 3.1.”QuadraticOrder.cardSqrts_prime_pow_even_val(theorem), declared in LeanPool/SingularModuli/QuadraticOrder/RootCounting.lean, line 746: “Counts roots of x^2 = p^(2r) u modulo p^n for odd prime p, p not dividing u, and 2r < n, reducing to the coprime case and multiplying by p^r.” Its source, as the card gives it: “C. Geiger, Singular Moduli and the Ideal Class Group, Section 3.1.”QuadraticOrder.tau_sub_tauConj_sq_of_valid_disc(lemma), declared in LeanPool/SingularModuli/QuadraticOrder/Discriminant.lean, line 62: “Proves the discriminant identity (tau - tauConj)^2 = d for valid quadratic-order discriminants d congruent to 0 or 1 modulo 4.” Its source, as the card gives it: “C. Geiger, Singular Moduli and the Ideal Class Group, Section 2.”
Project
- Authors: Caleb L. Geiger.
- Source: Singular Moduli and the Ideal Class Group by C. Geiger.
- Project repository: ElodinLaarz/lean-thesis.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 11R11, 11R29, 11A15.
- In Lean Pool: LeanPool/SingularModuli, from the card LeanPool/projects/singular-moduli.yaml.
Sources
TheoremThe Ramanujan-Nagell theorem#
Formalizes the Ramanujan-Nagell theorem, proving that the Diophantine equation x^2 + 7 = 2^n has exactly the five positive-integer solutions (|x|, n) = (1, 3), (3, 4), (5, 5), (11, 7), (181, 15).
Quoted from the card LeanPool/projects/ramanujan-nagell.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.
ramanujanNagellExact(theorem; a main declaration), declared in LeanPool/RamanujanNagell/Basic.lean, line 1125: “Proves that the integer solutions of x^2 + 7 = 2^n are exactly (x, n) = (+/-1, 3), (+/-3, 4), (+/-5, 5), (+/-11, 7), (+/-181, 15).” Its source, as the card gives it: “T. Nagell, The Diophantine equation x^2 + 7 = 2^n, Ark. Mat. 4 (1961), 185-187; L. J. Mordell, Diophantine Equations, Academic Press, 1969, Ch. 20.”
Project
- Authors: Barinder S. Banwait, Xinze Li.
- Source: arXiv:2604.09808.
- Project repository: BarinderBanwait/ramanujan_nagell.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 11D61, 11D45, 11R11.
- In Lean Pool: LeanPool/RamanujanNagell, from the card LeanPool/projects/ramanujan-nagell.yaml.
Sources
TheoremSelberg Sieve#
Formalizes the Selberg sieve with applications to prime-counting bounds and a Brun-Titchmarsh-style estimate.
Quoted from the card LeanPool/projects/selberg-sieve4.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.
fundamental_theorem_simple(theorem; a main declaration), declared in LeanPool/SelbergSieve4/MainResults.lean, line 29: “Proves the simple Selberg sieve upper-bound theorem.”primeCounting_isBigO_atTop(theorem; a main declaration), declared in LeanPool/SelbergSieve4/MainResults.lean, line 35: “Derives the asymptotic prime-counting upper bound.”primeCounting_le_mul(theorem), declared in LeanPool/SelbergSieve4/MainResults.lean, line 39: “Gives an eventual explicit constant upper bound for the prime-counting function.”primesBetween_le(theorem; a main declaration), declared in LeanPool/SelbergSieve4/MainResults.lean, line 42: “Bounds the number of primes in an interval using the sieve estimate.”
Project
- Authors: Arend Mellendijk.
- Source: Sieve Methods by Heini Halberstam, Hans-Egon Richert, https://archive.org/details/sievemethods0000halb.
- Project repository: amellendijk/selberg-sieve4.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 11N35, 11N05, 11N13.
- In Lean Pool: LeanPool/SelbergSieve4, from the card LeanPool/projects/selberg-sieve4.yaml.
Sources
TheoremSerre's mass formula for totally ramified local-field extensions#
Proves both of Serre's mass formulas for totally ramified separable extensions of a nonarchimedean local field of any positive degree, together with the discriminant bound, tame-ramification criterion, finiteness dichotomy, convergence, and automorphism-weighted orbit count. The proof develops Eisenstein monogenicity, quantitative Newton-Hensel lifting, local constancy of root counts, and Haar measures of lattices over discrete valuation rings.
Quoted from the card LeanPool/projects/serre-mass-formula.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.
MassFormula.tsum_one_div_q_pow_c(theorem; a main declaration), declared in LeanPool/MassFormula/First.lean, line 2794: “For every nonarchimedean local field K with residue-field cardinality q and every positive integer n, the sum of q^(-c(L)) over the totally ramified degree-n subextensions L of a separable closure of K is n, where c(L) is the discriminant exponent minus n plus one.”MassFormula.tsum_one_div_w_mul_q_pow_c(theorem), declared in LeanPool/MassFormula/Second.lean, line 98: “For every nonarchimedean local field K, positive n, and set of representatives of K-isomorphism classes of totally ramified separable degree-n extensions, the sum of 1/(|Aut_K(L)| q^c(L)) is one.”MassFormula.sigma_infinite_iff(theorem), declared in LeanPool/MassFormula/Finiteness.lean, line 345: “For positive n, the set of totally ramified separable degree-n subextensions is infinite exactly when K and its residue field have the same characteristic p and p divides n.”MassFormula.sub_one_le_d(theorem), declared in LeanPool/MassFormula/Discriminant.lean, line 670: “For positive n, the discriminant exponent of a totally ramified degree-n extension is at least n-1.”MassFormula.c_eq_zero_iff(theorem), declared in LeanPool/MassFormula/Tame.lean, line 145: “For positive n and a totally ramified degree-n extension, the wild discriminant exponent vanishes exactly when the residue characteristic does not divide n.”MassFormula.summable_one_div_q_pow_c(theorem), declared in LeanPool/MassFormula/Convergence.lean, line 45: “For positive n, the real-valued series of the unweighted mass terms is summable.”MassFormula.ncard_isomorphic_mul_w(theorem), declared in LeanPool/MassFormula/Orbit.lean, line 129: “For a nonarchimedean local field K and a totally ramified separable extension L of positive degree n, the number of K-isomorphic copies of L inside a separable closure, multiplied by |Aut_K(L)|, is n.”
Project
- Authors: Hyeon Seung-Hyeon.
- Source: Une «formule de masse» pour les extensions totalement ramifiées de degré donné d'un corps local by Jean-Pierre Serre, https://gallica.bnf.fr/ark:/12148/bpt6k6234149b/f323.item.
- Project repository: 0stellensatz/MassFormula, at commit 7fa41a62.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11S15, 11S05.
- In Lean Pool: LeanPool/MassFormula, from the card LeanPool/projects/serre-mass-formula.yaml.
Sources
TheoremSharp asymptotic bounds for runs of multiples in finite sets#
For a finite set S of n positive integers, let k(S,a) be the least positive integer k for which k*a is outside S. Proves an upper bound for every such S and a matching positive lower bound attained by some set of every sufficiently large cardinality n, establishing the extremal order n log n log log n. Contains entropy and chain-compression upper bounds and two lower-bound constructions, sharing definitions, prime estimates and padding. Preserves prime-weighted entropy estimates, smooth-number constructions and abstract cardinality-preserving compression lemmas.
Quoted from the card LeanPool/projects/runs-of-multiples.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.
RunsOfMultiples.main_theorem(theorem; a main declaration), declared in LeanPool/RunsOfMultiples/Main.lean, line 32: “Every sufficiently large finite set S of positive integers has sum of its first missing multiple indices at most C*n*log(n)*log(log(n)); for every sufficiently large n, a set of exactly n positive integers attains at least c*n*log(n)*log(log(n)), for a fixed c>0. This proof uses entropy and smooth numbers.”RunsOfMultiples.main_theorem_alt(theorem; a main declaration), declared in LeanPool/RunsOfMultiples/Alt/Main.lean, line 27: “The identical sharp asymptotic statement, proved using compression to divisor-closed, prime-shift-closed sets and a box-times-simplex construction.”
Project
- Authors: Jason Hoelscher-Obermaier, Claude Opus 5.5 (Lean proofs).
- Source: Runs of multiples in a finite set of integers by Claude Opus 5.5 (AI; published by Jason Hoelscher-Obermaier), https://github.com/jas-ho/runs-of-multiples-lean/blob/8b7e5f23534c321722725f78b6e64981557f0ef5/docs/runs-of-multiples.pdf.
- Project repository: jas-ho/runs-of-multiples-lean.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11N25, 11B75, 05D05.
- In Lean Pool: LeanPool/RunsOfMultiples, from the card LeanPool/projects/runs-of-multiples.yaml.
Sources
TheoremSharp Five-Distance and Sup-Norm Gap Theorems#
Formalizes sharp gap theorems for Kronecker sequences on tori: the Euclidean five-distance theorem on the 2-torus and the sup-norm gap bound, together with explicit arithmetic witnesses realizing the extremal cases - five distinct nearest-neighbour distances for the Euclidean and sup-norm metrics in dimension two, and nine distinct sup-norm distances in dimension three (Haynes-Marklof-Ramirez), via exact modular arithmetic on best simultaneous Diophantine approximations.
Quoted from the card LeanPool/projects/five-distance-sharp.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 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.
ThreeGap.EuclideanRecords.sharp_attained(theorem), declared in LeanPool/ThreeGap/EuclideanFiveDistanceSharpArith.lean, line 488: “Exhibits a base point on the 2-torus with an irrational coordinate and an N whose Euclidean nearest-neighbour distances realize exactly five distinct values, showing the Euclidean five-distance bound is sharp.” Its source, as the card gives it: “A. Haynes and J. Marklof, A five distance theorem for Kronecker sequences, International Mathematics Research Notices 2022(24):19747-19789, doi:10.1093/imrn/rnab205, arXiv:2009.08444.”ThreeGap.LinftyRecords.sharp_attained(theorem), declared in LeanPool/ThreeGap/LinftyFiveDistanceSharpArith.lean, line 366: “Exhibits a base point on the 2-torus with an irrational coordinate and an N whose sup-norm nearest-neighbour distances realize exactly five distinct values, showing the sup-norm gap bound is sharp in dimension two.”ThreeGap.LinftyRecords3.nine_attained(theorem; a main declaration), declared in LeanPool/ThreeGap/LinftyThreeTorusNine.lean, line 1173: “Exhibits a base point on the 3-torus with an irrational coordinate and an N whose sup-norm nearest-neighbour distances realize at least nine distinct values, showing the sup-norm gap bound is sharp in dimension three.”
Project
- Authors: Vico Bonfioli.
- Source: Higher dimensional gap theorems for the maximum metric by Alan Haynes, Jens Marklof, Ana Cristina Moreira Ramirez, arXiv:2010.08842.
- Project repository: ElVec1o/five-distance-sharp.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 11J71.
- In Lean Pool: LeanPool/ThreeGap, from the card LeanPool/projects/five-distance-sharp.yaml.
Sources
TheoremSimple zeros of the Riemann zeta function#
Formalizes Lamzouri's Hilbert-space proof of lower bounds for simple and distinct zeros of the Riemann zeta function. From explicit Riemann--von Mangoldt and unconditional pair-correlation hypotheses, the development proves that eventually more than 67.25% of nontrivial zeros are simple and on the critical line and more than 83.625% are distinct. It includes the finite-multiset Hilbert-space inequality, zeta-zero multiplicity symmetries, an admissible cutoff construction, and certified trigonometric estimates.
Quoted from the card LeanPool/projects/zeta-zeros.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.
ZetaZeros.simple_proportion_d4(theorem; a main declaration), declared in LeanPool/ZetaZeros/Main.lean, line 110: “Assuming the stated Riemann--von Mangoldt and unconditional pair-correlation formulas, beyond some height more than 67.25% of nontrivial zeta zeros are simple and lie on the critical line.”ZetaZeros.distinct_proportion_d5(theorem), declared in LeanPool/ZetaZeros/Main.lean, line 129: “Under the same two explicit analytic hypotheses, beyond some height more than 83.625% of nontrivial zeta zeros are distinct.”ZetaZeros.card_simpleRealPart_lower(theorem), declared in LeanPool/ZetaZeros/Hilbert/AlphaExpansion.lean, line 2473: “Bounds from below the number of multiplicity-one real points in a finite nonempty conjugation-invariant multiset using the squared test-kernel sum of any admissible function.”ZetaZeros.card_lower(theorem), declared in LeanPool/ZetaZeros/Hilbert/AlphaExpansion.lean, line 2603: “Bounds from below the number of distinct points in a finite nonempty conjugation-invariant multiset using the same Hilbert-space kernel method.”
Project
- Authors: Kenny Lau.
- Source: A new proof that more than 2/3 of the zeros of the Riemann zeta function are simple and on the critical line by Youness Lamzouri, doi:10.48550/arXiv.2609.02882, arXiv:2609.02882.
- Project repository: AxiomMath/ZetaZeros, at commit 4bcaf70e.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 11M06, 11M26.
- In Lean Pool: LeanPool/ZetaZeros, from the card LeanPool/projects/zeta-zeros.yaml.
Sources
TheoremSquare-difference-free polynomials beyond Naslund's conjectured bound#
Constructs square-difference-free subsets of polynomials over the field with three elements that refute Naslund's Conjecture 13 at every degree bound divisible by four and at least eight. An explicit degree-eight lift multiplies cardinality by 810 and yields a lower bound of 16/21 for the lower limiting normalized logarithmic growth rate.
Quoted from the card LeanPool/projects/naslund-counterexample.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.
NaslundCounterexample.exists_card_810(theorem), declared in LeanPool/NaslundCounterexample/Main.lean, line 40: “There is a square-difference-free set of 810 polynomials over F_3 with degree less than eight.”NaslundCounterexample.conjecture_fails_at_eight(theorem), declared in LeanPool/NaslundCounterexample/Main.lean, line 50: “The upper bound 3^6 = 729 in Naslund's Conjecture 13 fails for square differences over F_3 at degree bound eight.”NaslundCounterexample.exists_card_pow(theorem), declared in LeanPool/NaslundCounterexample/Main.lean, line 61: “For every positive integer e, there is a square-difference-free set of 810^e polynomials over F_3 with degree less than 8e.”NaslundCounterexample.exists_card_twenty_seven_mul_pow(theorem), declared in LeanPool/NaslundCounterexample/Main.lean, line 70: “For every natural number e, there is a square-difference-free set of 27 times 810^e polynomials over F_3 with degree less than 8e + 4.”NaslundCounterexample.conjecture_fails(theorem; a main declaration), declared in LeanPool/NaslundCounterexample/Main.lean, line 80: “For every n divisible by four with n at least eight, there is a square-difference-free set of polynomials over F_3 of degree less than n whose cardinality exceeds 3^(3n/4).”NaslundCounterexample.liminf_ge(theorem; a main declaration), declared in LeanPool/NaslundCounterexample/Asymptotics.lean, line 196: “If D(n) is the largest cardinality of a square-difference-free set of polynomials over F_3 of degree less than n, then the lower limit of log D(n) divided by n log 3 is at least 16/21.”
Project
- Authors: JD Jones.
- Source: Square-difference-free sets in F_3[T] past the conjectured bound by JD Jones.
- Project repository: JD-Jones-ASES/ns-lean, at commit 035e9b0c.
- 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: 11B75, 05D05.
- In Lean Pool: LeanPool/NaslundCounterexample, from the card LeanPool/projects/naslund-counterexample.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.