Exceptional Set in the abc… to Modular forms and the…

LemmaExceptional Set in the abc Conjecture#

Formalizes reductions and optimization bounds for a power-saving estimate on exceptional triples in the abc conjecture.

Quoted from the card LeanPool/projects/abc-exceptions.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.

Project
Sources
LeanabcConjecture_iff_countTriples · thm_4_point_3

TheoremFermat's Last Theorem for regular primes#

Formalizes Kummer's proof of Fermat's Last Theorem for every odd regular prime exponent. The development proves both cases of the theorem and includes the required theory of cyclotomic integers, relative units, Hilbert 90 and 92, ramification, class groups, and Kummer's lemma.

Quoted from the card LeanPool/projects/flt-regular.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.

Project
  • Authors: FltRegular contributors.
  • Source: Fermat's Last Theorem for regular primes by Riccardo Brasca, Ruben Van de Velde, Andrew Yang, Chris Birkbeck, Alex J. Best, Eric Rodriguez.
  • Project repository: leanprover-community/flt-regular, at commit 94a1d789.
  • Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
  • License: Apache-2.0.
  • MSC2020: 11D41, 11R18, 11R29.
  • In Lean Pool: LeanPool/FltRegular, from the card LeanPool/projects/flt-regular.yaml.
Sources
Leanflt_regular

TheoremFLT Eichler-Shimura#

Collects the definitions and theorems from the Anthropic Fermat's Last Theorem formalization needed for the Eichler-Shimura isomorphism, relating modular forms to cohomology of modular curves, and properties of the Galois representations of elliptic curves. Includes integer-multiplication results for elliptic curves with transcendental j-invariant, explicit function-field models of modular curves, and the genus formula for X_1(N).

Quoted from the card LeanPool/projects/flt-eichler-shimura.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.

Project
Sources
LeanHeckeEis.exists_eichlerShimura_heckeEquivariant · WeierstrassCurve.tateModuleRep_charpoly_frobenius · WeierstrassCurve.isogenyEnd_eq_zsmul_of_transcendental_j · ModularCurve.x0_modularPolynomialPresentation · ModularCurve.LevelN.frickeFunctionFieldModel · ModularCurve.genusFF_gamma1_formula_of_isAlgClosed

TheoremGalois groups of quadratic polynomial iterates#

Formalizes Stoll's criterion for when the Galois group of the n-th iterate of X² + a over the rationals is the full n-fold iterated wreath product of C₂. It proves the criterion in terms of two-independence of a signed critical-orbit sequence and its pairwise-coprime Möbius factors, and derives the paper's congruence families for which maximality holds at every level. The supporting library develops reusable multiquadratic-extension, iterated wreath-product, Möbius-factor, and valuation results.

Quoted from the card LeanPool/projects/quadratic-iterates.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.

Project
Sources
LeanQuadraticIterates.section3_main

TheoremThe Hasse–Minkowski theorem over ℚ#

Proves the local–global principle for quadratic forms over the rationals: a form is isotropic over ℚ exactly when it is isotropic over ℝ and over every p-adic completion, together with Meyer's theorem that an indefinite rational form in at least five variables is isotropic. The development builds the Hilbert symbol at every place of ℚ with Serre's explicit formulas (including the 2-adic case), proves Hilbert reciprocity and the existence theorem for prescribed local symbols, the Hasse invariant and the rank-two and rank-three local representability criteria, Legendre's ternary descent, and the rank-four and rank-≥5 inductions.

Quoted from the card LeanPool/projects/hasse-minkowski.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.

Project
Sources
LeanHasseMinkowski.hasseMinkowski · HasseMinkowski.meyer

TheoremImproved long gaps between consecutive primes#

Formalizes the unconditional lower bound showing that, for all sufficiently large X, the largest gap between consecutive primes below X is at least a positive constant times log X (log log X)^2 log log log log X / (log log log X)^2. The development includes the short-translates sieve proposition, divisor coefficient estimates, truncated product weights, moment bounds, and the Erdos--Rankin covering argument used to derive the headline result.

Quoted from the card LeanPool/projects/long-gaps-between-primes.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.

Project
Sources
LeanLongGapsBetweenPrimes.long_prime_gaps

TheoremImproved Lower Bounds for Strong n-Conjectures#

Formalizes the disproof of Ramaekers's conjecture, constructing tuple families whose abc-style quality stays bounded above 1, and proves Browkin-Brzezinski lower bounds on the quality of the n-conjecture tuples.

Quoted from the card LeanPool/projects/redhill.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.

Project
  • Authors: Jeremy Tan.
  • Source: Improved Lower Bounds for Strong n-Conjectures by Rupert Hölzl, Sören Kleine, Frank Stephan, doi:10.1017/S1446788725000084.
  • Project repository: Parcly-Taxel/Redhill.
  • 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) 2026 Jeremy Tan / Parcly Taxel”.
  • MSC2020: 11A41, 11D75.
  • In Lean Pool: LeanPool/Redhill, from the card LeanPool/projects/redhill.yaml.
Sources
Leannot_ramaekersConjecture_ge_six · le_quality_nConjectureTuples

TheoremInteger Moore determinants and iterated Fermat quotients#

Proves Granville's integrality and congruence formulas for iterated Fermat quotients at odd primes, including the exceptional order p - 1. For 1 ≤ d ≤ p and integers x_j prime to p, it proves that the nonzero integer Moore determinant det(x_j^(p^i)) is divisible by p^C(d+1,3), and that the next power does not divide it exactly when the Fermat quotients q_p(x_j) are pairwise distinct modulo p. The development supplies polynomial coefficient identities, denominator-clearing and valuation estimates, a determinant reduction ladder, and weighted Vandermonde formulas over general commutative rings.

Quoted from the card LeanPool/projects/granville-moore.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.

Project
Sources
LeanGranvilleMoore.not_pow_succ_dvd_det_mooreMatrix_iff

TheoremIrrationality of the Riemann zeta function at five#

Proves that Mathlib's Riemann zeta function at five is an irrational real number, following Aabir Fauzan's September 2026 preprint. Constructs integer polynomials of degree 37n with positive values at zeta(5) that decay exponentially in n squared. Includes a general integer-polynomial irrationality criterion, Hankel determinant and moment-integral identities, logarithmic-energy estimates, prime-adic integrality bounds, and kernel-checked rational certificates. The formalization uses a different normalizer and a positive decay constant in place of the paper's specific constant 139/5. Reuses the prime number theorem infrastructure already in the MooreBound project.

Quoted from the card LeanPool/projects/zeta-five-irrational.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.

  • Zeta5Irrational.irrational_five (theorem; a main declaration), declared in LeanPool/Zeta5Irrational/Main.lean, line 37: “There exists an irrational real number x whose complex coercion equals Mathlib's Riemann zeta function evaluated at five.” Its source, as the card gives it: “Fauzan, zeta(5) is irrational, Theorem 1.1, September 17, 2026, https://doi.org/10.5281/zenodo.22826419; upstream Apery/Main.lean. The completed formalization was released on September 23, 2026.”
  • Zeta5Irrational.main_estimate (theorem), declared in LeanPool/Zeta5Irrational/MainEstimate.lean, line 85: “There is a positive real c such that, for all sufficiently large n, an integer polynomial Q of degree 37n is a positive rational multiple of the constructed determinant polynomial and satisfies 0 < Q(zeta(5)) < exp(-c*n^2).” Its source, as the card gives it: “Upstream Apery/MainEstimate.lean; variant of the paper's Theorem 2.1 with c = -800*(Aeff + U) instead of 139/5.”
  • Zeta5Irrational.irrational_of_eventually_exists_int_poly (theorem), declared in LeanPool/Zeta5Irrational/Criterion.lean, line 62: “A real xi is irrational if, eventually, integer polynomials of degree at most d(n) have positive values at xi bounded by epsilon(n), and b^d(n)*epsilon(n) tends to zero for every positive natural b.” Its source, as the card gives it: “Upstream Apery/Criterion.lean; the paper's Section 1.1.”
Project
Sources
LeanZeta5Irrational.irrational_five

TheoremIrrationality of ζ(3)#

Formalizes Beukers' proof of Apéry's theorem for ζ(3), including the integral identities, denominator estimates, positivity, upper bounds, and final irrationality contradiction.

Quoted from the card LeanPool/projects/zeta_3_irrational.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.

Project
Sources
LeanLeanPool.Zeta3Irrational.zeta3_irrational

TheoremIwaniec's linear sieve and Jacobsthal's bound#

Proves an absolute O((r log r)^2) bound for any run of consecutive integers covered by r distinct primes, using the Rosser-Iwaniec linear sieve at the sifting limit. Preserves the combinatorial sieve, delay-equation majorants, prime-sum estimates and the proved strong prime-number-theorem dependency. This imports the dependency closure of the Jacobsthal corollary, rather than claiming the upstream formalizations of both papers in full.

Quoted from the card LeanPool/projects/iwaniec-linear-sieve.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.

Project
Sources
LeanIwaniecLinearSieve.iwaniecBound

TheoremKloosterman–Weil bounds via Carlitz and Stepanov#

Proves the classical prime Kloosterman–Weil bound by extension-field recurrences and auxiliary-polynomial point counts. Develops exact CRT factorization, squarefree bounds with a unit first coefficient, and centered incomplete reciprocal-phase bounds at the reduced modulus.

Quoted from the card LeanPool/projects/kloosterman-weil.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.

Project
Sources
LeanKloostermanWeil.weil1948_bound · KloostermanWeil.kloostermanUnitSum_crt · KloostermanWeil.centeredReducedIntervalSum_bound

TheoremThe Komlós and Beck–Fiala bounds with constant 36#

Proves that finitely many real vectors of Euclidean norm at most one admit signs whose sum has every coordinate bounded by 36, and deduces the Beck–Fiala discrepancy bound 36 times the square root of the maximum vertex degree for finite hypergraphs. The Karingula–Lovett splitting argument is supported by reusable finite-distribution, total-variation, transport, convex-hull, and matrix-discrepancy infrastructure. The near-invariant distribution uses discrete squared tent weights, and real vectors are handled by coordinatewise truncation toward zero.

Quoted from the card LeanPool/projects/komlos.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.

  • Komlos.discrepancy_le_of_forall_sum_sq_le_one (theorem; a main declaration), declared in LeanPool/Komlos/Main.lean, line 57: “For a real matrix with arbitrary finite row and column index types, if each column has sum of squared entries at most one, its minimum signed-column discrepancy is at most 36.” Its source, as the card gives it: “Theorem 1.2, matrix form.”
  • Komlos.exists_isColouring_forall_abs_sum_apply_le (theorem), declared in LeanPool/Komlos/Main.lean, line 102: “Any finite family of vectors in a finite-dimensional real Euclidean space, each of norm at most one, admits signs in {-1, 1} whose signed sum has absolute value at most 36 in every coordinate.” Its source, as the card gives it: “Theorem 1.2.”
  • Hypergraph.exists_isColouring_forall_abs_finsum_le (theorem), declared in LeanPool/Komlos/BeckFiala.lean, line 77: “If a hypergraph has finitely many vertices and each vertex belongs to at most t edges, there is a {-1, 1} colouring of all vertices whose sum on each edge has absolute value at most 36 times sqrt(t).” Its source, as the card gives it: “Beck–Fiala consequence discussed in Section 1.”
  • Komlos.exists_isColouring_mean_add_sum_mem_convexHull (theorem), declared in LeanPool/Komlos/SignedSums.lean, line 34: “For a finitely supported probability distribution on any real module and n vectors, if translation by six times each vector has total variation distance at most one third, some signed sum added to the mean belongs to the convex hull of the distribution's support.” Its source, as the card gives it: “Lemma 1.4, generalized to arbitrary real modules.”
  • Komlos.exists_nearInvariant (theorem), declared in LeanPool/Komlos/NearInvariant.lean, line 70: “Every positive-denominator integer grid in finite-dimensional real coordinate space admits a finitely supported mean-zero probability distribution in [-6, 6]^d whose total variation distance under any grid translation of Euclidean norm at most one is at most one third.” Its source, as the card gives it: “Lemma 1.5, using discrete squared tent weights.”
Project
Sources
LeanKomlos.discrepancy_le_of_forall_sum_sq_le_one

TheoremLehmer's Polynomial and the E10 Coxeter Element#

Proves that Lehmer's degree-10 polynomial — the integer polynomial of smallest known Mahler measure above 1 — is irreducible over the integers, and that it is the characteristic polynomial of a Coxeter element of the E10 Weyl group (the rank-10 instance of McMullen). Against Mathlib's Mahler-measure API it computes M(L) exactly as the Salem root with the unconditional bounds 1 < M(L) < 7/5, states Lehmer's conjecture as a defined Prop (never assumed) with the strong form implying the gap form, and contrasts the E8 Coxeter element (order exactly 30) with the E10 element (infinite order in GL(10,Z)): the E-series crosses from torsion to a Salem matrix at rank 10, and the crossing value is Lehmer's number.

Quoted from the card LeanPool/projects/lehmer-e10.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.

Project
Sources
LeanLehmerE10.main_theorem

TheoremLeo Moser's finite distinct-subset-sums inequality#

Formalizes the exact finite sum-of-squares inequality that Guy's 1982 account states as Theorem 2 and attributes to Leo Moser: a finite set A of natural numbers with distinct subset sums satisfies 4^|A| - 1 <= 3 * sum(a^2). It then derives direct and square-root lower bounds for the largest element of A. This does not claim the stronger historical asymptotic bound attributed jointly to Erdős and Moser, and Erdős Problem 1 remains open.

Quoted from the card LeanPool/projects/erdos-moser-distinct-subset-sums.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.

Project
Sources
LeanLeanPool.ErdosMoser.leoMoserVarianceBound

TheoremLi's criterion for the Riemann Hypothesis#

Li's criterion for the Riemann zeta function, formalized in Lean 4 over Mathlib: Mathlib's RiemannHypothesis holds if and only if every Li-Keiper coefficient of the completed xi function has nonnegative real part. The zero-indexed analytic coefficient at n is Li's classical lambda_(n+1), the n-th Taylor coefficient at 0 of the logarithmic derivative of s |-> xi(1/(1-s)). A second compared theorem identifies this analytic coefficient with Li's arithmetic coefficient, the symmetrized sum over the nontrivial zeros counted with multiplicity, and proves that symmetrized family summable so the sum is the genuine one. Both results are unconditional: the biconditional, the coefficient identification, the genus-1 Hadamard factorization of xi (with multiplicity), genus-1 summability of 1/|rho|^2, and the growth bound order(xi) <= 1 are all proved. This is a formalization of a classically known equivalence (X.-J. Li, 1997); it is not a proof of the Riemann Hypothesis, nor of the positivity of the coefficients.

Quoted from the card LeanPool/projects/li-criterion-rh-equivalence-lean.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.

Project
Sources
Leanli_criterion · li_coefficients_eq_zero_sum

TheoremLinear independence of 1, zeta(2), and zeta(3)#

Proves that 1, the Riemann zeta function at 2, and its value at 3 are linearly independent over the rationals, using integer polynomial approximation, p-adic coefficient bounds, prime-edge nonvanishing, and logarithmic potential energy estimates for Hankel determinants. Includes reusable irrationality criteria, contour integration, Andreief identities, Newton-basis valuation bounds, and energy inequalities for finite measures. The cited source is the completed Lean proof; independent novelty of the informal argument is not claimed.

Quoted from the card LeanPool/projects/zeta2-zeta3-linear-independence.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.

Project
Sources
LeanZeta32.one_zeta_two_zeta_three_linearIndependent

TheoremMarkoff mod p#

Lean 4 formalization of strong approximation for the Markoff surface modulo sufficiently large primes. The primary source is Bourgain-Gamburd-Sarnak.

Quoted from the card LeanPool/projects/markoff-modp.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.

Project
Sources
LeanBGS.Markoff.reduction_surjective_of_explicitBound

TheoremMinimum modulus for the unique multiset-sum problem#

Formalizes the exact minimum modulus N_min(n) = 2^n - 2^{floor(log_2 n)} for the unique multiset-sum problem on the super-increasing residue set {2^i - 1 : 0 <= i < n}, and proves the sharp elementary-abelian-2-group lower bound k >= n - 1 for unique multiset sums in (Z/2Z)^k.

Quoted from the card LeanPool/projects/min-modulus-unique-multiset-sum.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.

Project
Sources
LeanMinModulus.nmin_eq · MinModulus.elementaryAbelianTwoGroups_optimal

TheoremModular forms and the generalized residue theorem#

Formalizes the Hungerbühler-Wasem generalized residue theorem for Cauchy principal value integrals through poles and applies it to the valence formula for modular forms on the modular group.

Quoted from the card LeanPool/projects/leanmodularforms.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.

Project
Sources
LeangeneralizedResidueTheorem · valence_formula_textbook_orbit_finsum

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.