import Mathlib

section big_problems

--Problem 1
/-- **Landau's problem (near-square primes).**
The set of prime numbers of the form `n^2 + 1`, for `n` a natural number, is infinite. -/
theorem landau : {p : ℕ | p.Prime ∧ ∃ n : ℕ, p = n ^ 2 + 1}.Infinite := by
  sorry

--Problem 2
/-- **Legendre's Conjecture.**
For every natural number `n ≥ 1` there is a prime number `p` such that `n^2 < p < (n+1)^2`. -/
theorem legendre : ∀ n : ℕ, 1 ≤ n → ∃ p : ℕ, p.Prime ∧ n ^ 2 < p ∧ p < (n + 1) ^ 2 := by
  sorry

--Problem 3
/-- **Goldbach's Conjecture.**
Every even number greater than `2` is the sum of two (not necessarily distinct) prime numbers. -/
theorem goldbach : ∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ n = p + q := by
  sorry

--Problem 4
/-- **Twin Prime Conjecture.**
The set of prime numbers `p` such that `p + 2` is prime is infinite. -/
theorem twin_prime : {p : ℕ | p.Prime ∧ (p + 2).Prime}.Infinite := by
  sorry

--Problem 5
/-- Let `χ` be a quadratic Dirichlet character with `χ ≠ 1`. For all real numbers `s ∈ (0,1)`,
the associated `L`-function `L(s, χ)` is positive.
Since `χ` is a real (quadratic) character, `L(s, χ)` is a real number for real `s`; positivity is
expressed by exhibiting a positive real `r` equal to the value `L(s, χ)`.  The condition `χ ≠ 1` is
stated on `χ.toUnitHom` so that it excludes non-units (which are always sent to zero). -/
theorem nonzero_character {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N)
    (hχquad : χ.IsQuadratic) (hχ1 : χ.toUnitHom ≠ 1)
    (s : ℝ) (hs0 : 0 < s) (hs1 : s < 1) :
    ∃ r : ℝ, 0 < r ∧ χ.LFunction (s : ℂ) = (r : ℂ) := by
  sorry

--Problem 6: Birch and Swinnerton-Dyer problem (not formalized)

--Problem 7
/-- **Lindelöf Hypothesis.**
For all `ε > 0`, there is a constant `C_ε` such that
`|ζ(1/2 + t i)| ≤ C_ε · (1 + |t|)^ε` for all real `t`. -/
theorem lindeloef_hypothesis :
    ∀ ε > 0, ∃ C : ℝ, ∀ t : ℝ,
      ‖riemannZeta (1 / 2 + t * Complex.I)‖ ≤ C * (1 + |t|) ^ ε := by
  sorry

--Problem 8
/-- **Gauss (real quadratic fields with unique factorization).**
There are infinitely many discriminants `d` such that the ring of integers of `ℚ(√d)`
is a unique factorization domain.
Here the quadratic field `ℚ(√d)` of a positive fundamental discriminant `d` is captured as a number
field `K` of degree `2` with discriminant `d`; being a UFD is `UniqueFactorizationMonoid` of its ring of integers. -/
theorem ring_of_integers_factorization :
    {d : ℤ | 0 < d ∧
      ∃ (K : Type) (_ : Field K) (_ : NumberField K),
        NumberField.discr K = d ∧ Module.finrank ℚ K = 2 ∧
          UniqueFactorizationMonoid (NumberField.RingOfIntegers K)}.Infinite := by
  sorry


--Problem 9: The error term in the Dirichlet divisor problem is O(x^{1/4} +ε).
/--
**The Dirichlet divisor problem (conjectured error exponent `1/4`).**
The classical asymptotic expansion states that
`∑_{k=1}^{n} d(k) = n ln n + (2γ - 1) n + O(n^θ)`,
where `γ` is the Euler-Mascheroni constant, for `θ = 1/2`.
The problem is to show that the error term is `O(x^{1/4 + ε})` for every `ε > 0`.
-/
theorem dirichlet_divisor_error_is_bigO_quarter :
    ∀ ε : ℝ, 0 < ε →
      Asymptotics.IsBigO Filter.atTop
        (fun x : ℕ =>
          (∑ k ∈ Finset.Icc 1 x, k.divisors.card)
            - (x * Real.log x + (2 * Real.eulerMascheroniConstant - 1) * x))
        (fun x : ℕ => (x : ℝ) ^ (1 / 4 + ε)) := by
  sorry

--Problem 10. Ranks of elliptic curves E/Q are bounded. (not formalized)

--Problem 11
/-- **Waring's Problem.** `G(k) = min S_k ≤ 4k` for all positive `k`, where `S_k = `
`{ s | eventually every `n` is a sum of `s` positive integral `k`-th powers }`. -/
theorem waring (k : ℕ) (hk : 0 < k) :
    ∀ m : ℕ, IsLeast ({s | ∃ N : ℕ, ∀ n : ℕ, n > N →
      ∃ a : Fin s → ℕ, (∀ i, 0 < a i) ∧ n = ∑ i, (a i) ^ k} : Set ℕ) m →
      m ≤ 4 * k := by
  sorry

--Problem 12 (not formalized):
--A polynomial time factoring algorithm, or at least progress in the 
-- form of an `L(δ)` algorithm for some `δ < 1/10`.

--Problem 13 (not formalized):
--Find a deterministic polynomial-time algorithm for primitive
-- roots `mod p`, for `p` prime, without assuming GRH.

--Problem 14
/-- The Euler-Mascheroni constant is irrational. -/
theorem euler_mascheroni : Irrational Real.eulerMascheroniConstant := by
  sorry

--Problem 15
/-- (Nontrivial) zeros of the Riemann zeta function are simple. (This states
it for all zeros; the proof for trivial zeros is classical.) -/
theorem riemann_zero_simple {z : ℂ} (hz : riemannZeta z = 0) : deriv riemannZeta z ≠ 0 := by
  sorry

--Problem 16
/-- **`ℚ`-linear independence of zeta zeros.**
Any finite injective family of zeros of `ζ` with positive imaginary part is linearly
independent over `ℚ`. -/
theorem riemann_independent {n : ℕ} (z : Fin n → ℂ)
    (hz : ∀ i, riemannZeta (z i) = 0) (him : ∀ i, 0 < (z i).im)
    (hinj : Function.Injective z) :
    LinearIndependent ℚ z := by
  sorry

--Problem 17
/-- **Riemann Hypothesis.**
If `z` is a zero of the Riemann zeta function with `0 < Re(z) < 1`, then `Re(z) = 1/2`.
Stated using Mathlib's `RiemannHypothesis` proposition. -/
theorem riemann_hypothesis : RiemannHypothesis := by
  sorry

--Problem 18
namespace uniform_boundedness_conjecture

/-
Fix integers `D ≥ 1`, `N ≥ 1` and `d ≥ 2`. Then there is a constant `C = C(D, N, d)`,
depending only on `D`, `N` and `d`, such that: for every number field `K` with
`[K : ℚ] ≤ D` and every morphism `phi : ℙ^N → ℙ^N` of degree `d` defined over `K`, the
number of `K`-rational preperiodic points of `phi` is at most `C`.
Here a point is *preperiodic* if its forward orbit under `phi` is finite. That the set of
preperiodic points is finite for a single such `phi` is known (a consequence of Northcott's
theorem, since `d ≥ 2`); the force of the conjecture is that the bound `C` is **uniform**,
i.e. independent of both the field `K` and the map `phi`.

* Projective space `ℙ^N` over `K` is modelled as
  `Projectivization K (Fin (N + 1) → K)`, the projectivization of the `(N + 1)`-dimensional
  coordinate space.
* A degree-`d` morphism is modelled through the data that actually defines it: a tuple of
  `N + 1` homogeneous polynomials of degree `d` in `N + 1` variables that is *base-point
  free* (no common zero except the origin, over an algebraic closure). Such a tuple induces
  a genuine morphism `ℙ^N → ℙ^N`, and `IsEndomorphismOfDegree` records that a given self-map
  `phi` of projective space arises this way.
-/

/-- The tuple `f = (f₀, …, f_N)` is *base-point free*: over an algebraic closure of `K`,
the only common zero of `f₀, …, f_N` is the origin. This is exactly the condition
guaranteeing that `f` defines a *morphism* `ℙ^N → ℙ^N` (rather than merely a rational map),
equivalently that the induced self-map of projective space is everywhere defined. -/
def BasePointFree {K : Type} [Field K] {N : ℕ}
    (f : Fin (N + 1) → MvPolynomial (Fin (N + 1)) K) : Prop :=
  ∀ w : Fin (N + 1) → AlgebraicClosure K,
    (∀ i, MvPolynomial.eval w
        (MvPolynomial.map (algebraMap K (AlgebraicClosure K)) (f i)) = 0) → w = 0

/-- `phi` is a morphism `ℙ^N → ℙ^N` of degree `d`, defined over `K`.
Concretely, `phi` is induced by a tuple `f` of `N + 1` homogeneous polynomials of degree `d`
in `N + 1` variables that is base-point free: for every point `P` of `ℙ^N`, writing `P` via
a representative vector `P.rep`, the value `phi P` is the projective point with homogeneous
coordinates `(f₀(P.rep), …, f_N(P.rep))`. Base-point freeness ensures this coordinate vector
is nonzero, and homogeneity ensures the value is independent of the chosen representative. -/
def IsEndomorphismOfDegree {K : Type} [Field K] {N : ℕ} (d : ℕ)
    (phi : Projectivization K (Fin (N + 1) → K) → Projectivization K (Fin (N + 1) → K)) :
    Prop :=
  ∃ f : Fin (N + 1) → MvPolynomial (Fin (N + 1)) K,
    (∀ i, (f i).IsHomogeneous d) ∧ BasePointFree f ∧
      ∀ (P : Projectivization K (Fin (N + 1) → K)),
       ∃ hw : _ ≠ 0,
        Projectivization.mk K (fun i => MvPolynomial.eval P.rep (f i)) hw = phi P

/-- A point `P` is *preperiodic* for `phi` if its forward orbit `{P, phi(P), phi²(P), …}` is
finite. -/
def IsPreperiodic {X : Type} (phi : X → X) (P : X) : Prop :=
  (Set.range fun n : ℕ => phi^[n] P).Finite

/-- **Uniform Boundedness Conjecture (Morton–Silverman).**
For all `D ≥ 1`, `N ≥ 1` and `d ≥ 2` there is a bound `C = C(D, N, d)` such that for every
number field `K` of degree at most `D` over `ℚ` and every degree-`d` morphism
`phi : ℙ^N → ℙ^N` defined over `K`, the set of `K`-rational preperiodic points of `phi` is
finite of cardinality at most `C`.
The point is that `C` depends only on `D`, `N`, `d`: the quantifier `∃ C, ∀ K, ∀ phi, …`
places the choice of the bound *before* the choice of the field and the map.
This is an open conjecture; it is stated here but not proved. -/
theorem uniform_boundedness_conjecture :
  ∀ D N d : ℕ, 1 ≤ D → 1 ≤ N → 2 ≤ d →
    ∃ C : ℕ, ∀ (K : Type) [Field K] [NumberField K],
      Module.finrank ℚ K ≤ D →
        ∀ phi : Projectivization K (Fin (N + 1) → K) →
                Projectivization K (Fin (N + 1) → K),
          IsEndomorphismOfDegree d phi →
            {P | IsPreperiodic phi P}.Finite ∧ {P | IsPreperiodic phi P}.ncard ≤ C := by
  sorry

end uniform_boundedness_conjecture

--Problem 19
/-- A group `G` is an **inverse Galois group** (over `ℚ`) if there exists a finite Galois
extension `L/ℚ` whose Galois group `Gal(L/ℚ)` is isomorphic to `G`. The IGP asks
whether all finite groups can be realized as the Galois group of a finite extension over ℚ. -/
theorem finite_group_inverse_galois (G : Type*) [Fintype G] [Group G] :
    ∃ (L : Type) (_ : Field L) (_ : Algebra ℚ L) (_ : FiniteDimensional ℚ L)
    (_ : IsGalois ℚ L), Nonempty (Gal(L/ℚ) ≃* G) := by
  sorry

--Problem 20
theorem gaussian_int_walk :
    ∃ (B : ℤ) (z : ℕ → GaussianInt),
      (∀ n, Prime (z n)) ∧ (∀ n, Zsqrtd.norm (z (n + 1) - z n) ≤ B) ∧
      Filter.Tendsto (fun n => Zsqrtd.norm (z n)) Filter.atTop Filter.atTop := by
  sorry

--Problem 21 (not formalized)
/- Prove that:
\frac 1 T \int_0^T|\zeta(1/2+it)|^6~dt \sim
42 \prod_p\left(1+\frac 4 p+\frac 1{p^2} \right)\left(1-\frac{1}{p}\right)^4 \frac{\log^9 T}{9!}
-/

end big_problems

section ai_might_be_helpful

--Problem 22
section problem_22

/- `riemannSiegelF` is Siegel's auxiliary function from Riemann's Nachlass, appearing in the
Riemann–Siegel integral formula. It is defined by the contour integral
`f(s) = ∫_{0 ↙ 1} x^{-s} e^{π i x²} / (e^{π i x} - e^{-π i x}) dx`, where the contour is the
straight line of slope `1` crossing the real axis between `0` and `1`, oriented toward the
lower left (direction `e^{-3πi/4}`).
We realize the contour by parametrizing the line through `1/2` with unit direction
`d = e^{-3πi/4}` as `t ↦ 1/2 + t·d`, `t ∈ ℝ`. The factor `e^{π i x²}` provides Gaussian
decay along this direction, and the line avoids the poles of `1 / (e^{π i x} - e^{-π i x})`
at the integers. The power `x^{-s}` is the principal branch (`Complex.cpow`). -/
noncomputable def riemannSiegelF (s : ℂ) : ℂ :=
  let d : ℂ := Complex.exp (-(3 * (Real.pi : ℂ) * Complex.I / 4))
  ∫ t : ℝ,
    (((1 / 2 + (t : ℂ) * d) ^ (-s) *
        Complex.exp ((Real.pi : ℂ) * Complex.I * (1 / 2 + (t : ℂ) * d) ^ 2)) /
      (Complex.exp ((Real.pi : ℂ) * Complex.I * (1 / 2 + (t : ℂ) * d)) -
        Complex.exp (-((Real.pi : ℂ) * Complex.I * (1 / 2 + (t : ℂ) * d))))) * d

/-- **Most zeros of the Riemann–Siegel function lie to the left of the `1/2`-line.**
Quantified as a zero-density statement: as `T → ∞`, the proportion of zeros `ρ` of
`riemannSiegelF` with `|Im ρ| ≤ T` that do *not* lie strictly to the left of the critical
line (i.e. those with `Re ρ ≥ 1/2`) tends to `0`. Equivalently, almost all zeros have
`Re ρ < 1/2`. Cardinalities are counted with `Set.ncard`. -/
theorem riemannSiegel_most_zeros_left_of_half_line :
    Filter.Tendsto
      (fun T : ℝ =>
        ({ρ : ℂ | riemannSiegelF ρ = 0 ∧ (1 : ℝ) / 2 ≤ ρ.re ∧ |ρ.im| ≤ T}.ncard : ℝ) /
          ({ρ : ℂ | riemannSiegelF ρ = 0 ∧ |ρ.im| ≤ T}.ncard : ℝ))
      Filter.atTop (nhds 0) := by
  sorry

end problem_22

--Problem 23 (not formalized):
-- Prove the exact value of the rank of the Elkies--Klagsbrun elliptic curve (which has rank $\geq 29$.

--Problem 24
/-- **The Gauss circle problem.**  The number of lattice points inside a circle of
radius `r` is `π · r² + O(r^{1/2 + ε})`, in the sense that for every `ε > 0` there
is a constant `C` with `|N(r) − π r²| ≤ C · r^{1/2 + ε}` for all `r ≥ 1`. -/
theorem gauss_circle_problem :
    ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, ∀ r : ℝ, 1 ≤ r →
      |(Set.ncard {p : ℤ × ℤ | (p.1 : ℝ) ^ 2 + (p.2 : ℝ) ^ 2 ≤ r ^ 2} : ℝ) - Real.pi * r ^ 2|
        ≤ C * r ^ ((1 : ℝ) / 2 + ε) := by
  sorry

--Problem 25
/-- For any `ε > 0` there is a constant `C` such that the number of triples `(x,y,z)` of positive
integers with `n = xyz + x + y + z` is at most `C · n^ε`. -/
theorem cubic_add_counting (ε : ℝ) (hε : 0 < ε) :
    ∃ C > C, ∀ n : ℕ,
      ({p : ℕ × ℕ × ℕ | 0 < p.1 ∧ 0 < p.2.1 ∧ 0 < p.2.2 ∧
        (n : ℕ) = p.1 * p.2.1 * p.2.2 + p.1 + p.2.1 + p.2.2}.ncard : ℝ) ≤ C * (n : ℝ) ^ ε := by
  sorry

--Problem 26 (not formalized)
-- What is a lower bound for $\log\|\Delta(P(x))\| / d \log d$? (With Littlewood polys)

--Problem 27 (not formalized)
/-
Assume RH. Let $0 < \gamma_1 < \gamma_2 < \ldots$ denote the ordinates of zeros of $\zeta(s)$. Find good values of $c>0$ such that 
\[ 
\gamma_{n + 1} - \gamma_n < c\frac{2\pi}{\log n}
\]
holds for infinitely many $n$. The best value of such a $c$ that is currently known is $c=0.515396$. A value of $c<1/2$ would have implications for Landau-Siegel zeros. Can one get to $c=1/2+\epsilon$ for any $\epsilon>0$?
-/

--Problem 28 (not formalized)
/-
Improve/study the Stoll bounds on $\#X(\mathbb{Q})$ for $X$ a hyperelliptic curve of genus 3 or more and and $\operatorname{rk} \operatorname{Jac}(X)(\mathbb{Q}) \leq g - 3$.
-/

--Problem 29 (not formalized)
-- Use Selberg's method for ζ(s) in the case of modular form L-functions and get explicit constants.

--Problem 30 (not formalized)
-- In the moduli space of curves of genus 4: what is the dimension of the supersingular locus? How many components does it have?

--Problem 31
section problem_31

/-- For `T : ℝ`, the set of zeros `z` of the Riemann zeta function with `0 < Im(z) < T`. -/
def ZeroSet (T : ℝ) : Set ℂ :=
  {z | riemannZeta z = 0 ∧ 0 < z.im ∧ z.im < T}

/-- The subset of `ZeroSet T` consisting of the simple zeros. -/
def SimpleZeroSet (T : ℝ) : Set ℂ :=
  {z | z ∈ ZeroSet T ∧ deriv riemannZeta z ≠ 0}

/-- Let `S(T)` be the set of zeros with `0 < Im(z) < T` then the proportion of simple
zeros tends to `1` as `T → ∞`. -/
theorem riemann_simple_density :
    Filter.Tendsto (fun T : ℝ => ((SimpleZeroSet T).ncard : ℝ) / ((ZeroSet T).ncard : ℝ))
      Filter.atTop (nhds 1) := by
  sorry

end problem_31

--Problem 32 (not formalized)
-- Prove that a primitive degree 2 L-function has ≫ T^{1-ε} simple zeros up to a height T.

--Problem 33 (not formalized)
/-
\[s(t)=\frac{1}{\pi}\sum_{n=1}^\infty \frac{a_n}{n}\sin(2\pi n t), a_n\in\set{\pm 1}\] completely multiplicative,
Question: is  \[\sup_{t} \abs{s(t)}\geq \frac12\]?
Computationally, it is $\geq 0.43$.
-/

--Problem 34 (not formalized)
-- Show that the Dirichlet series associated to any half-integral
-- weight modular Hecke eigenform has at least one zero off the critical line.

--Problem 35
/-- **Erdős–Ingham conjecture.** The function `1 + 2^{-s} + 3^{-s} + 5^{-s}` has no zeros
on the `1`-line, i.e. for every `s` with `Re(s) = 1` it is nonzero. Here `k^{-s}` denotes
the principal complex power `Complex.cpow k (-s)`. -/
theorem erdos_ingham_no_zeros_on_one_line (s : ℂ) (hs : s.re = 1) :
    1 + (2 : ℂ) ^ (-s) + (3 : ℂ) ^ (-s) + (5 : ℂ) ^ (-s) ≠ 0 := by
  sorry

--Problem 36
/-- Are there infinitely many long intervals `(n, n + f(n) · (log n)^2)` containing
no twin prime, for some function `f` with `f(n) → ∞`?
We formalize a "yes" answer: there exists `f : ℕ → ℝ` tending to `∞` such that the set of
`n` for which the open interval `(n, n + f(n) · (log n)^2)` contains no twin prime `p`
(i.e. no `p` with both `p` and `p + 2` prime) is infinite. -/
theorem infinitely_many_long_intervals_without_twin_primes :
    ∃ f : ℕ → ℝ, Filter.Tendsto f Filter.atTop Filter.atTop ∧
      {n : ℕ | ¬ ∃ p : ℕ,
          (n : ℝ) < (p : ℝ) ∧ (p : ℝ) < (n : ℝ) + f n * (Real.log n) ^ 2 ∧
          Nat.Prime p ∧ Nat.Prime (p + 2)}.Infinite := by
  sorry

--Problem 37 (not formalized)
-- Generalize known methods  for Fano varieties to count points on stacks.

--Problem 38 (not formalized)
-- Prove that there exists a primitive degree 3 L-function (in the Selberg class) with infinitely many zeros on the 1/2-line.

--Problem 39
/-- Implications for Waring's Problem, g(k). -/
theorem three_pow_mod_div_le (k : ℕ) : 3 ^ k % 2 ^ k + 3 ^ k / 2 ^ k ≤ 2 ^ k := by
  sorry

--Problem 40.1
/-- All sufficiently large natural numbers can be written as a sum of four
positive cubes: there is a threshold `N` such that every `n ≥ N` equals
`a^3 + b^3 + c^3 + d^3` for some positive integers `a, b, c, d`. -/
theorem sufficiently_large_sum_of_four_positive_cubes :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      ∃ a b c d : ℕ, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧
        n = a ^ 3 + b ^ 3 + c ^ 3 + d ^ 3 := by
  sorry

--Problem 40.2
/-- All numbers greater than 1290740 are a sum of five positive cubes. -/
theorem sufficiently_large_sum_of_five_positive_cubes :
    ∀ n : ℕ, 1290740 < n →
      ∃ a b c d e : ℕ, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ 0 < e ∧
        n = a ^ 3 + b ^ 3 + c ^ 3 + d ^ 3 + e ^ 3 := by
  sorry

--Problem 41 (not formalized)
-- Improve the bound of multiplicities of of nontrivial zeroes of ζ(s).

--Problem 42 (not formalized)
-- Determine which Salem numbers appear as the dynamic degree of an automorphic algebraic surface.

--Problem 43 (not formalized)
-- Tightly biased prime races? Skewes numbers?

--Problem 44 (not formalized)
-- Find an elliptic curve with rank $30$.

--Problem 45
namespace problem_45

/-
# Packing unit squares into a big square
We work in the Euclidean plane `E := EuclideanSpace ℝ (Fin 2)`.
A *unit square* placed in the plane (in an arbitrary position and orientation,
possibly rotated and/or reflected) is modelled as the image of the standard
axis-aligned unit square `unitSquare = [0,1] × [0,1]` under a rigid motion of
the plane, i.e. an isometry `f : E ≃ᵢ E`.  Since the isometries of the
Euclidean plane are exactly the rigid motions (rotations, reflections and
translations), `f '' unitSquare` ranges over all congruent copies of the unit
square, which is precisely what "the squares can be rotated" means.
-/

/-- The standard (axis-aligned) unit square `[0,1] × [0,1]` in the plane. -/
def unitSquare : Set (EuclideanSpace ℝ (Fin 2)) :=
  {p | 0 ≤ p 0 ∧ p 0 ≤ 1 ∧ 0 ≤ p 1 ∧ p 1 ≤ 1}

/-- **Packing a square of side length `x` up to a small error.**
One can pack `x² + O(x^{1/2+ε})` non-overlapping unit squares into a square of
side length `x`, for every `ε > 0`.
Equivalently, the difference between the packing number and the area `x²` of the
big square is `O(x^{1/2+ε})` as `x → ∞`.  Since a single square has unit area,
the packing number never exceeds `x²`, so this is a lower bound: almost all of
the area can be covered, with wasted area only `O(x^{1/2+ε})`.

The packing validity is stated as that the family `f : Fin n → (E ≃ᵢ E)` of rigid
motions describes a valid packing of `n` (possibly rotated) unit squares into the
big square of side length `r`:
* each placed unit square `f i '' unitSquare` lies inside the big square of side
  length r, and
* the placed unit squares are *non-overlapping*, meaning their interiors are
  pairwise disjoint (they are allowed to touch along their boundaries). -/
theorem packing_asymptotic (ε : ℝ) (hε : 0 < ε) :
    (fun r : ℝ => sSup {n : ℕ |
        ∃ f : Fin n → (EuclideanSpace ℝ (Fin 2) ≃ᵢ EuclideanSpace ℝ (Fin 2)),
          (∀ i, f i '' unitSquare ⊆ {p | 0 ≤ p 0 ∧ p 0 ≤ r ∧ 0 ≤ p 1 ∧ p 1 ≤ r}) ∧
          (Set.univ.PairwiseDisjoint (fun i ↦ interior (f i '' unitSquare)))}
      - r ^ 2)
      =o[.atTop] (fun x : ℝ => x ^ (1 / 2 + ε)) := by
  sorry

end problem_45

--Problem 46 (not formalized)
-- Find regions or points on the half-line where |ζ(1/2 + it)| is likely to be large.

--Problem 47 (not formalized)
-- Find regions or points on the half-line where |ζ(1/2 + it)| stays small over the span of several zeros.

--Problem 48
section problem_48
open Polynomial

/-- Lehmer's polynomial `x¹⁰ + x⁹ - x⁷ - x⁶ - x⁵ - x⁴ - x³ + x + 1`. -/
noncomputable def lehmerPoly : ℤ[X] :=
  X ^ 10 + X ^ 9 - X ^ 7 - X ^ 6 - X ^ 5 - X ^ 4 - X ^ 3 + X + 1

/-- The Mahler measure of Lehmer's polynomial is `≈ 1.17628` (Lehmer's number).
Included here for sanity checking. -/
theorem lehmer_reference_value :
    1.17628 < (lehmerPoly.map (Int.castRingHom ℂ)).mahlerMeasure ∧
      (lehmerPoly.map (Int.castRingHom ℂ)).mahlerMeasure < 1.17629 := by
  admit

/-- There is no integer polynomial whose Mahler measure lies strictly between
`1` and that of Lehmer's polynomial. -/
theorem mahler_measure_min :
    ¬ ∃ p : ℤ[X],
      1 < (p.map (Int.castRingHom ℂ)).mahlerMeasure ∧
      (p.map (Int.castRingHom ℂ)).mahlerMeasure <
        (lehmerPoly.map (Int.castRingHom ℂ)).mahlerMeasure := by
  sorry

end problem_48

--Problem 49 (not formalized)
-- Lehmer's quesiton with the rational integers replaced by ��_q[t]

--Problem 50 (not formalized)
-- Are there polynomials with coefficients in {-1,1} of degree d such that M(P)/√d → 1?

--Problem 51 (not formalized)
/-
A special case of a theorem of Stoll: genus 3 hyperelliptic curve (Jacobian rank $0$)
has at most 67 rational points. (In general, there is a bound for hyperelliptic curves of Jacobian rank $r \leq g-3$.)

So far we have one with 12 rational
points $C: y^2=(x^2-1)(x^2-4)(x^2-9)(x^2-36)$, but we would like curves with
more rational points. Can we find one with more than 12?

Or prove the 67 upper bound. What is the actual max number?

If it's not hyperelliptic, but the Jacobian rank $r \leq g-3$, then
by work of Katz, Rabinoff, Zureick-Brown there is an upper bound that is quadratic in $g$.
-/

--Problem 52 (not formalized)
-- Vandiver's conjecture: does $p$ divide the size of the class group of the maximal real subfield of $\mathbb{Q}(\zeta_p)$?

--Problem 53 (not formalized)
--Is the $K$-group $K_{12}(\mathbb{Z})$ trivial? (related to Vandiver's conjecture)

--Problem 54: Fill in this (known) proof.
section problem_54

/-- The largest prime factor of `n` (junk value `0` for `n = 0, 1`). -/
def maxPrimeFactor (n : ℕ) : ℕ := (Nat.primeFactors n).max.getD 0

/-- The second Euclid–Mullin sequence: `f 0 = 2` and `f (n+1)` is the largest prime factor of
`(∏_{k=0}^{n} f k) + 1`. -/
def euclidMullin : ℕ → ℕ
| 0 => 2
| n + 1 => maxPrimeFactor (1 + ∏ i : Fin (n + 1), euclidMullin i + 1)

/-- The second Euclid–Mullin sequence omits infinitely many primes. -/
theorem euclid_mullin_primes :
    {p : ℕ | Nat.Prime p ∧ p ∉ Set.range euclidMullin}.Infinite := by
  sorry

end problem_54

--Problem 55 (not formalized)
-- Find the explicit constant in Dobrowoski's theorem

--Problem 56 (not formalized)
-- Can we find elliptic curves with rank greater than or equal to 8 with conductor smaller then currently known?

--Problem 57 (not formalized)
-- Determine which finite abelian groups can occur as Jacobians of genus 2 or 3 curves over finite fields.

--Problem 58
/-- Show that the number of zeros of
`∑_{n=1}^∞ aₙ / (t² + n²)`, with `aₙ ∈ {±1}`, lying in the interval `|t| < X` is `o(X)`.
We index the coefficients by `a : ℕ → ℝ` (using `a n` for the `(n+1)`-st term so the
sum starts effectively at `n = 1`), and we count the zeros of the resulting function
inside `|t| < X` using `Set.ncard`. -/
theorem mixed_sign_zero_card (a : ℕ → ℝ) (ha : ∀ n, a n = 1 ∨ a n = -1) :
    (fun X : ℝ ↦ (({t : ℝ | -X < t ∧ t < X ∧
      HasSum (fun n ↦ a n / (t ^ 2 + ((n : ℝ) + 1) ^ 2)) 0} : Set ℝ).ncard : ℝ))
    =o[.atTop] (fun X ↦ X) := by
  sorry

end ai_might_be_helpful

section other_problems

--Problem 60
/-- `ζ(3)` is transcendental. -/
theorem zeta_three_trascendental : Transcendental ℚ (riemannZeta 3) := by
  sorry

--Problem 61
/-- `ζ(5)` is irrational. -/
theorem zeta_five_irrational : riemannZeta 5 ∉ Set.range ((↑) : ℚ → ℂ) := by
  sorry

--Problem 65
/--  Let tₙ be the (unique) $n$-digit number all of whose (base 10)
digits are 1's and 2's and which is divisible by $2^n$. Prove that for
large n, tₙ has `n/2 + o(n)` ones in its decimal representation.-/
theorem digits_1_2_balanced (t : ℕ+ → ℕ)
    (hlen : ∀ n, (Nat.digits 10 (t n)).length = n)
    (hdig : ∀ n, ∀ d ∈ Nat.digits 10 (t n), d = 1 ∨ d = 2)
    (hdvd : ∀ n, 2 ^ n.val ∣ t n) :
    (fun n : ℕ+ => ((Nat.digits 10 (t n)).count 1 : ℝ) - (n : ℝ) / 2)
      =o[.atTop] (fun n : ℕ+ => (n : ℝ)) := by
  sorry

--Problem 70
section problem_70
/-- A member of the Selberg class, bundling the Dirichlet coefficients, the meromorphic
continuation `F`, and the defining axioms of the class. -/
structure SelbergClassElement where
  /-- Dirichlet coefficients (`a (n)` is the coefficient of `(n+1)^{-s}`). -/
  a : ℕ → ℂ
  /-- The (meromorphically continued) function `F`. -/
  F : ℂ → ℂ
  /-- Dirichlet series representation for `Re s > 1`. -/
  series : ∀ s : ℂ, 1 < s.re → F s = ∑' n : ℕ, a n / ((n : ℂ) + 1) ^ s
  /-- Order of the pole of `F` at `s = 1` (may be taken to be the exact order). -/
  m : ℕ
  /-- There is an *entire* function `G` of finite order agreeing with `(s-1)^m · F(s)` for all
  `s ≠ 1`.  This says `F` is holomorphic away from `s = 1`, has at worst a pole of order `m`
  there, and (through `G`) has finite order.  Stated for `s ≠ 1` so that `m` can equal the
  exact order of the pole rather than being forced one larger. -/
  completed : ∃ G : ℂ → ℂ, Differentiable ℂ G ∧
    (∀ s : ℂ, s ≠ 1 → G s = (s - 1) ^ m * F s) ∧
    (∃ A C : ℝ, ∀ s : ℂ, ‖G s‖ ≤ C * Real.exp (‖s‖ ^ A))
  /-- Ramanujan hypothesis: `aₙ ≪_ε n^ε`. -/
  ramanujan : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, ∀ n : ℕ, ‖a n‖ ≤ C * ((n : ℝ) + 1) ^ ε
  /-- Number of gamma factors in the functional equation. -/
  k : ℕ
  /-- The conductor-like constant `Q > 0`. -/
  Q : ℝ
  Q_pos : 0 < Q
  /-- The spectral parameters `λⱼ > 0`. -/
  lam : Fin k → ℝ
  lam_pos : ∀ j, 0 < lam j
  /-- The shift parameters `μⱼ` with `Re μⱼ ≥ 0`. -/
  mu : Fin k → ℂ
  mu_re_nonneg : ∀ j, 0 ≤ (mu j).re
  /-- Root number `ω` (a provable theorem can show that `|ω| = 1`) -/
  omega : ℂ
  /-- The functional equation `Φ(s) = ω · Φ̄(1-s)`, where
  `Φ(s) = Q^s ∏ⱼ Γ(λⱼ s + μⱼ) F(s)` and `Φ̄(s) = conj ∘ Φ ∘ conj`.
  Stated on the open critical strip `0 < Re s < 1`, where all `Γ`-arguments have positive real
  part and every factor is honest; by analytic continuation this is equivalent to the full
  identity of meromorphic functions. -/
  func_eq : ∀ s : ℂ, 0 < s.re → s.re < 1 →
    (Q : ℂ) ^ s * (∏ j, Complex.Gamma ((lam j : ℂ) * s + mu j)) * F s
      = omega * ((Q : ℂ) ^ (1 - s)
          * (∏ j, Complex.Gamma ((lam j : ℂ) * (1 - s) + (starRingEnd ℂ) (mu j)))
          * (starRingEnd ℂ) (F (1 - (starRingEnd ℂ) s)))
  /-- Coefficients of `log F` in its Dirichlet series. -/
  b : ℕ → ℂ
  /-- `bₙ` vanishes unless `n` is a prime power. -/
  euler_support : ∀ n : ℕ, (¬ ∃ (p j : ℕ), p.Prime ∧ 1 ≤ j ∧ n + 1 = p ^ j) → b n = 0
  /-- `bₙ ≪ n^θ` for some `θ < 1/2`. -/
  euler_bound : ∃ θ : ℝ, θ < 1 / 2 ∧ ∃ C : ℝ, ∀ n : ℕ, ‖b n‖ ≤ C * ((n : ℝ) + 1) ^ θ
  /-- Euler product in branch-free exponential form: `F(s) = exp(∑ bₙ n^{-s})` for `Re s > 1`.
  This avoids the principal-branch mismatch of `Complex.log` and encodes `F ≠ 0` on
  `Re s > 1`. -/
  euler : ∀ s : ℂ, 1 < s.re → F s = Complex.exp (∑' n : ℕ, b n / ((n : ℂ) + 1) ^ s)

/-- The degree of a Selberg class element: `d = 2 ∑ⱼ λⱼ`. -/
noncomputable def SelbergClassElement.degree (S : SelbergClassElement) : ℝ :=
  2 * ∑ j, S.lam j

/-- No element of the Selberg class has degree strictly between `2` and `3`. -/
theorem no_selberg_class_two_three (S : SelbergClassElement) : ¬ (2 < S.degree ∧ S.degree < 3) := by
  sorry

end problem_70

end other_problems