feat: add hardest theorems from LeanTriathlon

LeanEval/NumberTheory/FriedlanderIwaniec.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2026 Project Numina. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Numina Team
+-/
+import Mathlib
+import EvalTools.Markers
+
+namespace FriedlanderIwaniec
+
+/-!
+# Friedlander–Iwaniec theorem
+
+There are infinitely many primes of the form `a² + b⁴`.
+
+ See <https://en.wikipedia.org/wiki/Friedlander%E2%80%93Iwaniec_theorem>.
+-/
+
+section Main
+
+open Nat
+
+@[eval_problem]
+theorem friedlander_iwaniec : {p : ℕ | p.Prime ∧ ∃ a b, p = a ^ 2 + b ^ 4}.Infinite := by
+  sorry
+
+end Main
+
+end FriedlanderIwaniec

LeanEval/NumberTheory/KoukoulopoulosMaynard.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2026 Project Numina. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Numina Team
+-/
+import Mathlib
+import EvalTools.Markers
+
+namespace KoukoulopoulosMaynard
+
+/-!
+# Duffin–Schaeffer theorem (Koukoulopoulos–Maynard)
+
+For a nonnegative function `f`, almost every real is approximable by infinitely
+many reduced fractions `p / q` with `|x - p/q| < f q / q` if and only if the
+series `∑ φ(n) f(n) / n` diverges.
+
+ See <https://en.wikipedia.org/wiki/Duffin%E2%80%93Schaeffer_theorem>.
+-/
+
+section Main
+
+open MeasureTheory Set Nat
+
+@[eval_problem]
+theorem koukoulopoulos_maynard {f : ℕ → ℝ} (hf : ∀ n, 0 < f n) :
+    (∀ᵐ (x : ℝ), {(p, q) : ℕ × ℕ | p.Coprime q ∧ |x - p / (↑q : ℝ)|
+      < f q / (↑q : ℝ)}.Finite) ↔ Summable fun n ↦ φ n * f n / (↑n : ℝ) := by
+  sorry
+
+end Main
+
+end KoukoulopoulosMaynard

LeanEval/NumberTheory/Linnik.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2026 Project Numina. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Numina Team
+-/
+import Mathlib
+import EvalTools.Markers
+
+namespace Linnik
+
+/-!
+# Linnik's theorem (L = 5.5)
+
+The least prime in the arithmetic progression `a mod d` (for `a` coprime to `d`)
+is bounded polynomially in `d`, with the explicit Linnik constant `L = 5.5`
+(due to Heath-Brown, 1992).
+
+ See D. R. Heath-Brown, *Zero-free regions for Dirichlet L-functions, and the
+ least prime in an arithmetic progression*, Proc. London Math. Soc. (3) 64
+ (1992), no. 2, 265–338. <https://doi.org/10.1112/plms/s3-64.2.265>
+-/
+
+section Main
+
+open Nat
+
+/-- The least prime in the progression `a, a + d, a + 2d, …`
+(or `0` if no such prime exists). -/
+noncomputable def p (a d : ℕ) : ℕ := sInf ({a + k * d | k : ℕ} ∩ {p | p.Prime})
+
+/-- Linnik's theorem with the explicit constant `L = 5.5`: the least prime in the
+progression `a mod d` is bounded by `c * d ^ 5.5` for some constant `c`. -/
+@[eval_problem]
+theorem linnik : ∃ c : ℝ, ∀ ⦃a d : ℕ⦄,
+    0 < a → a < d → a.Coprime d → p a d ≤ c * (↑d : ℝ) ^ (5.5 : ℝ) := by
+  sorry
+
+end Main
+
+end Linnik

LeanEval/NumberTheory/TwoNinetyTheorem.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 Project Numina. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Numina Team
+-/
+import Mathlib
+import EvalTools.Markers
+
+namespace Matrix
+
+variable {R : Type} [Ring R] {n : ℕ}
+
+/-- A quadratic form, represented as a matrix, takes a particular value for some
+integer vector input. -/
+def TakesValue (M : Matrix (Fin n) (Fin n) R) (m : ℕ) : Prop :=
+  ∃ v : Fin n → ℤ, (fun i => (v i : R)) ⬝ᵥ (M *ᵥ (fun i => (v i : R))) = (m : R)
+
+/-- A quadratic form, represented as a matrix, is universal if it takes every
+positive integer value. -/
+def Universal (M : Matrix (Fin n) (Fin n) R) : Prop :=
+  ∀ m : ℕ, 0 < m → M.TakesValue m
+
+/-- A quadratic form is integral if it takes only integer values on integer
+vectors. -/
+def Integral (M : Matrix (Fin n) (Fin n) R) : Prop :=
+  ∀ v : Fin n → ℤ,
+    (fun i => (v i : R)) ⬝ᵥ (M *ᵥ (fun i => (v i : R))) ∈ Set.range ((↑) : ℤ → R)
+
+end Matrix
+
+namespace TwoNinety
+
+/-!
+# The 290 theorem
+
+A positive-definite integral quadratic form represents every positive integer
+as soon as it represents the 29 critical numbers
+`1, 2, 3, 5, 6, 7, 10, 13, 14, 15, 17, 19, 21, 22, 23, 26, 29, 30, 31, 34, 35,
+37, 42, 58, 93, 110, 145, 203, 290`.
+
+ See <https://en.wikipedia.org/wiki/15_and_290_theorems>.
+-/
+
+section Main
+
+open Matrix
+
+/-- The 29 critical numbers of the 290 theorem. -/
+def critical_290_numbers : Finset ℕ :=
+  {1, 2, 3, 5, 6, 7, 10, 13, 14, 15, 17, 19, 21, 22, 23, 26, 29, 30, 31,
+   34, 35, 37, 42, 58, 93, 110, 145, 203, 290}
+
+@[eval_problem]
+theorem two_ninety_theorem {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ)
+    (hpos : M.PosDef)
+    (hIntegral : M.Integral)
+    (hrep : ∀ m ∈ critical_290_numbers, M.TakesValue m) :
+    M.Universal := by
+  sorry
+
+end Main
+
+end TwoNinety

manifests/problems/friedlander_iwaniec.toml

@@ -0,0 +1,9 @@
+id = "friedlander_iwaniec"
+title = "Friedlander–Iwaniec theorem"
+test = false
+module = "LeanEval.NumberTheory.FriedlanderIwaniec"
+holes = ["friedlander_iwaniec"]
+submitter = "Bolton Bailey/Project Numina"
+notes = "The Friedlander–Iwaniec theorem: there are infinitely many primes of the form `a² + b⁴`."
+source = "Friedlander, John, and Henryk Iwaniec. “The Polynomial X² + Y⁴ Captures Its Primes.” Annals of Mathematics, vol. 148, no. 3, 1998, pp. 945–1040. JSTOR, https://doi.org/10.2307/121034."
+informal_solution = "Friedlander and Iwaniec develop a sieve for primes that, unlike classical sieves, can detect primes in a sequence as thin as `a² + b⁴`. The crux is establishing sum-estimates for a bilinear form involving a Möbius-function-like term and a term for counting representations of a number of the `a² + b⁴` form."

manifests/problems/koukoulopoulos_maynard.toml

@@ -0,0 +1,8 @@
+id = "koukoulopoulos_maynard"
+title = "Duffin–Schaeffer theorem (Koukoulopoulos–Maynard)"
+test = false
+module = "LeanEval.NumberTheory.KoukoulopoulosMaynard"
+holes = ["koukoulopoulos_maynard"]
+submitter = "Bolton Bailey/Project Numina"
+notes = "The Duffin–Schaeffer theorem, proved in full by Koukoulopoulos and Maynard (2020): for a positive approximating function `f`, almost every real `x` is approximable by infinitely many reduced fractions `p/q` with `|x - p/q| < f(q)/q` if and only if the series `∑ φ(n) f(n) / n` diverges."
+source = "Dimitris Koukoulopoulos, James Maynard 'On the Duffin-Schaeffer conjecture,' Annals of Mathematics, Ann. of Math. (2) 192(1), 251-307, (July 2020). https://doi.org/10.4007/annals.2020.192.1.5"

manifests/problems/linnik.toml

@@ -0,0 +1,9 @@
+id = "linnik"
+title = "Linnik's theorem (L = 5.5)"
+test = false
+module = "LeanEval.NumberTheory.Linnik"
+holes = ["linnik"]
+submitter = "Bolton Bailey/Project Numina"
+notes = "Linnik's theorem with the explicit constant `L = 5.5` due to Heath-Brown (1992): for `a` coprime to `d` with `0 < a < d`, the least prime `p(a, d)` in the progression `a mod d` satisfies `p(a, d) ≤ c · d ^ 5.5` for some absolute constant `c`."
+source = "Heath-Brown, D.R. (1992), Zero-Free Regions for Dirichlet L-Functions, and the Least Prime in an Arithmetic Progression. Proceedings of the London Mathematical Society, s3-64: 265-338. https://doi.org/10.1112/plms/s3-64.2.265"
+informal_solution = "Heath-Brown's proof rests on three priciples: a quantitative zero-free region for Dirichlet L-functions, the Deuring-Heilbronn phenomenon, and the log-free zero-density estimate. Heath-Brown combines strong versions of these estimates to obtain an exponent of 5.5."

manifests/problems/two_ninety_theorem.toml

@@ -0,0 +1,9 @@
+id = "two_ninety_theorem"
+title = "The 290 theorem"
+test = false
+module = "LeanEval.NumberTheory.TwoNinetyTheorem"
+holes = ["two_ninety_theorem"]
+submitter = "Bolton Bailey/Project Numina"
+notes = "The 290 theorem (Bhargava–Hanke): a positive-definite integral quadratic form represents every positive integer if it represents a particular collection of 29 critical numbers below 290."
+source = "M. Bhargava, J. Hanke, Universal quadratic forms and the 290-theorem, preprint (2011). See also https://en.wikipedia.org/wiki/15_and_290_theorems"
+informal_solution = "The proof combines advances in the escalation method and bounds on Fourier coefficients of weight 2 theta functions. It also uses a trick to allow the analysis to focus mainly on quaternary forms."