Pick one.

theorem coP_eq_P : { L | Lᶜ ∈ P } = P

theorem lambert_series_eq_num_divisor_sum : ∀ t : ℚ, ∑' n : ℕ+, 1 / ((t : ℝ) ^ (n : ℕ) - 1) = ∑' n : ℕ+, (n : ℕ).divisors.card / ((t : ℝ) ^ (n : ℕ))

theorem f_undefined_at_2 : f 2 = 0

theorem isGood_example : IsGood {p ^ 2 | (p : ℕ) (_ : p ≡ 3 [MOD 4]) (_ : p.Prime)}

theorem factorial_isPractical (n : ℕ) : Nat.IsPractical n.factorial

theorem le_chromaticNumber : (n : ℕ∞) ≤ C.graph.chromaticNumber

lemma exists_k (N : ℕ) : ∃ (k : ℕ) (n : Fin k → ℕ), (∀ i, N ≤ n i) ∧ StrictMono n ∧ ∑ i, (1 / n i : ℝ) = 1

lemma claim2_inequality : ∀ᶠ n in atTop, ∀ δ : (Fin n) → ℚ, δ '' Set.univ ⊆ {-1,0,1} → letI lhs := |∑ k, ((δ k : ℚ) / (k + 1))| lhs ≠ 0 → lhs ≥ 1 / (Icc 1 n).lcm id

theorem exists_sidon_pos_density : ∃ (A : Set ℕ), IsSidon A ∧ 0 < sidonUpperDensity A

theorem f_id : f id = fun n ↦ #{d ∈ n.divisors | Odd d}

theorem example_maximal_sidon : IsMaximalSidonSetIn {1, 2, 4} 4

theorem maxSidonSubsetCard_icc_bound (N : ℕ) (hN : 1 ≤ N) : maxSidonSubsetCard (Icc 1 N) ≤ 2 * Real.sqrt N

theorem sum_factorial_inv_eq_geometric : let f (n k : ℕ) : ℝ := 1 / ((n + 2).factorial : ℝ) ^ (k + 1) ∑' n : ℕ, (1 : ℝ) / ((n + 2).factorial - 1) = ∑' n : ℕ, ∑' k : ℕ, f n k

theorem erdos_69 : Irrational <| ∑' n, ω (n + 2) / 2 ^ (n + 2)

theorem erdos_872.trivial_upper_bound (n : ℕ) (hn : 2 ≤ n) : L n ≤ n - 1

theorem two_mul_add (a b : Nat) : 2 * (a + b) = 2 * a + 2 * b

theorem even_or_odd (n : Nat) : n % 2 = 0 ∨ n % 2 = 1

theorem two_pow_pos' (n : Nat) : 0 < 2 ^ n

theorem gauss_sum (n : Nat) : 2 * ((List.range (n + 1)).foldl (· + ·) 0) = n * (n + 1)

theorem mod_seven_periodic (n : Nat) : (n + 7) % 7 = n % 7

theorem reverse_reverse' (xs : List Nat) : xs.reverse.reverse = xs

theorem gcd_self' (n : Nat) : Nat.gcd n n = n

theorem min_le_max' (a b : Nat) : min a b ≤ max a b

theorem squarefree_of_isCarmichael {a : ℕ} (ha₁ : a.Composite) (ha₂ : IsCarmichael a) : Squarefree a

theorem flt_of_beal_conjecture (H : bealConjecture) : FermatLastTheorem

theorem carmichealTotientFor_odd {n : ℕ} (hn : Odd n) : CarmichaelTotientFor n

theorem not_congruentNumber_1 : ¬ congruentNumber 1

theorem new_mersenne_conjecture_of_prime : (∀ p, p.Prime → Odd p → NewMersenneConjectureStatement p) → ∀ p, Odd p → NewMersenneConjectureStatement p

lemma completeGraphIsClique (s : Finset V) : (⊤ : SimpleGraph V).IsClique s

theorem isSurjunctive_of_finite (G : Type) [Group G] [Finite G] : IsSurjunctive G

theorem pellNumber_sq_add_pellNumber_succ_sq (n : ℕ) : pellNumber (2 * n + 1) = pellNumber n ^ 2 + pellNumber (n + 1) ^ 2

lemma discr_rat_of_modEq_one (hd₄ : d ≡ 1 [ZMOD 4]) : discr (QuadraticAlgebra ℚ d 0) = d

theorem jacobson_conjecture_of_comm_ring (R : Type u) [CommRing R] [IsNoetherianRing R] : JacobsonConjectureFor R

theorem ABφθSpec.existsUnique : ∃! ABφθ : ℝ × ℝ × ℝ × ℝ, ABφθSpec ABφθ.1 ABφθ.2.1 ABφθ.2.2.1 ABφθ.2.2.2

theorem pollock_tetrahedral.ncard_exceptions : type_of% pollock_tetrahedral.salzer_levine ↔ NotSumOfFourTetrahedral.ncard = 241

theorem exists_not_hasResolution_of_not_perfectField (k : Type u) [Field k] (hk : ¬ PerfectField k) : ∃ (X : Scheme.{u}) (sX : X ⟶ Spec (.of k)), IsIntegral X ∧ LocallyOfFiniteType sX ∧ QuasiCompact sX ∧ IsSeparated sX ∧ topologicalKrullDim X = 0 ∧ ¬ Scheme.HasResolution sX

theorem card_heightLE_div_pow_five_div_six_tensto : atTop.Tendsto (fun H ↦ (heightLE H).ncard / (H : ℝ) ^ (5 / 6 : ℝ)) (𝓝 (2 ^ (4 / 3 : ℝ) * 3 ^ (-3 / 2 : ℝ) / (riemannZeta 10).re))

theorem wolstenholme_theorem (p : ℕ) (h : p > 3) (hp : Nat.Prime p) : (2 * p - 1).choose (p - 1) ≡ 1 [MOD p ^ 3]