Legendre's conjecture: exponent progress, formalized reductions, and a no-sorry/no-axiom audit. Deep analytic proofs are NOT formalized.
-
Updated
Oct 18, 2026 - Lean
#
legendre-conjecture
Here are 4 public repositories matching this topic...
Legendre's conjecture in function fields (v7): proved for q >= d-1 (Hayes-Weil), verified for every q when d <= 8, conjecture for q <= d-2. Paper, review, code, data.
python latex reproducible-research finite-fields numba number-theory galois-theory computer-assisted-proof arithmetic-geometry legendre-conjecture monodromy function-fields irreducible-polynomials prime-polynomials chebotarev-density lang-weil hayes-characters keating-rudnick
-
Updated
Oct 6, 2026 - TeX
Draft (unpublished): exact explicit-formula verification of the function-field Legendre conjecture for d <= 10, fluctuations of prime counts, and a characteristic-2 anomaly.
finite-fields number-theory random-matrix-theory computer-assisted-proof exact-arithmetic explicit-formula legendre-conjecture function-fields irreducible-polynomials hayes-characters
-
Updated
Oct 20, 2026 - Python
Real-process formal verification of Legendre conjecture in Lean 4. Leveraging strong normalization of type theory, potential infinity automatically evolves, purging unrequested ZFC actual infinity and overriding OpenAI's Result 013 via phase-locked invariants (0 sorrys/axioms).
-
Updated
Oct 21, 2026 - Lean
Add this topic to your repo
To associate your repository with the legendre-conjecture topic, visit your repo's landing page and select "manage topics."