Pick one.

theorem P_ne_NP : P ≠ NP

theorem navier_stokes_existence_and_smoothness_R3 (nu : ℝ) (hnu : nu > 0) (u₀ : ℝ³ → ℝ³) (hu₀ : InitialVelocityConditionDecay u₀) : ∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ (f := 0) v p

theorem riemannHypothesis : RiemannHypothesis

theorem erdos_101 : (fun n => (numLinesWithFourPointMax n : ℝ)) =o[atTop] (fun n => (n : ℝ)^2)

theorem erdos_1020 (r : ℕ) (hr : 3 ≤ r) (n k : ℕ) (hk : 0 < k) (hrk : r * k - 1 ≤ n) : f n r k = max ((r * k - 1).choose r) (n.choose r - (n - k + 1).choose r)

theorem erdos_1029 : Tendsto (fun k : ℕ ↦ (SimpleGraph.diagonalRamsey k : ℝ) / ((k : ℝ) * (2 : ℝ) ^ ((k : ℝ) / 2))) atTop atTop

theorem erdos_1030 : ∃ c > (0 : ℝ), ∃ L : ℝ, Tendsto (fun k : ℕ ↦ (SimpleGraph.classicalRamsey (k + 1) k : ℝ) / (SimpleGraph.classicalRamsey k k : ℝ)) atTop (nhds L) ∧ L > 1 + c

theorem erdos_104 : (fun n : ℕ => (maxUnitCircleCount n : ℝ)) =o[atTop] (fun n : ℕ => (n : ℝ) ^ 2)

theorem erdos_1107 : ∀ r ≥ 2, ∀ᶠ n in atTop, SumOfRPowerful r n

theorem finite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (n : γ.ToType → ℕ) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => (n α : Cardinal.{u}) + 1) → cardinalPartitionRel lam r γ (fun α => (n α : Cardinal.{u}))

theorem erdos_159 : ∃ (c : ℝ) (_ : 0 < c) (C : ℝ), ∀ (n : ℕ), 1 ≤ n → (SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4) (SimpleGraph.completeGraph (Fin n)) : ℝ) ≤ C * (n : ℝ) ^ (2 - c)

theorem erdos_233 : (fun N => ((∑ n ∈ Finset.range N, (primeGap n) ^ 2) : ℝ)) =O[atTop] fun N => N * (log N)^2

theorem erdos_236: (fun n => (f n : ℝ)) =o[atTop] (fun n => Real.log (n : ℝ))

theorem erdos_242 (n : ℕ) (hn : 2 < n) : ∃ x y z : ℕ, 1 ≤ x ∧ x < y ∧ y < z ∧ (4 / n : ℚ) = 1 / x + 1 / y + 1 / z

theorem erdos_243 (a : ℕ → ℕ) (ha₀ : StrictMono a) (ha₁ : Tendsto (fun n ↦ (a n : ℝ) / a (n - 1) ^ 2) atTop (𝓝 1)) (ha₂ : Summable ((1 : ℚ) / a ·)) : ∀ᶠ n in atTop, a n = a (n - 1) ^ 2 - a (n - 1) + 1

theorem erdos_282 {x : ℚ} (hx : x ∈ Set.Ioo 0 1) (hx_den : Odd x.den) : greedyUnitFractionRem { n | Odd n } x =ᶠ[atTop] 0

theorem erdos_364 : ¬ ∃ (n : ℕ), Powerful n ∧ Powerful (n + 1) ∧ Powerful (n + 2)

theorem erdos_371 : { n | Nat.maxPrimeFac (n + 1) > Nat.maxPrimeFac n }.HasDensity (1/2)

theorem erdos_373 : S.Finite

theorem erdos_41 (A : Set ℕ) (h_triple : NtupleCondition A 3) (h_infinite : A.Infinite) : Filter.atTop.liminf (fun N => (A ∩ Icc 1 N).ncard / (N : ℝ)^(1/3 : ℝ)) = 0

theorem erdos_535 : ∀ r ≥ 3, ∃ c > (0 : ℝ), ∀ᶠ (N : ℕ) in atTop, (f r N : ℝ) ≤ (N : ℝ) ^ (c / log (log (N : ℝ)))

theorem erdos_563 : ∀ (α : ℝ), 0 ≤ α → α < 1 / 2 → ∃ (c : ℝ), 0 < c ∧ Tendsto (fun n : ℕ => (F n α : ℝ) / Real.log n) atTop (nhds c)

theorem erdos_572 (k : ℕ) (hk : 3 ≤ k) : ∃ c > (0 : ℝ), ∀ᶠ (n : ℕ) in atTop, c * (n : ℝ) ^ (1 + 1 / (k : ℝ)) ≤ (SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph (2 * k)) : ℝ)

theorem erdos_583 {V : Type*} [Fintype V] (G : SimpleGraph V) (hG : G.Connected) : ∃ D : Finset G.Subgraph, (∀ H ∈ D, IsPathSubgraph H) ∧ IsDecomposition G D ∧ D.card ≤ ⌈(Fintype.card V : ℚ) / 2⌉₊

theorem erdos_617 (r : ℕ) (hr : r ≥ 3) {V : Type} [Fintype V] [DecidableEq V] (hV : Fintype.card V = r^2 + 1) (coloring : Sym2 V → Fin r) : ∃ (S : Finset V) (k : Fin r), S.card = r + 1 ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ k

theorem erdos_779 (n : ℕ) (hn : n ≥ 1): let P := ∏ i ∈ range (n + 1), nth Nat.Prime i ∃ p, p.Prime ∧ (P + p).Prime ∧ nth Nat.Prime n < p ∧ p < P

theorem erdos_82 : Tendsto (fun n => F n / Real.log n) atTop atTop

theorem erdos_859 : ∃ c₁ > 0, ∃ c₂ > (0 : ℝ), ∃ d : ℕ → ℝ, (∀ t > 0, (DivisorSumSet t).HasDensity (d t)) ∧ (fun (t : ℕ) ↦ d t) ~[atTop] (fun t ↦ c₁ / Real.log t ^ c₂)

theorem erdos_89 : (fun (n : ℕ) => n/(n : ℝ).log.sqrt) =O[atTop] (fun n => (minimalDistinctDistances ℝ² n : ℝ))

theorem erdos_982 (n : ℕ) (hn : 3 ≤ n) (p : Fin n → ℝ²) (hp : Function.Injective p) (hp' : EuclideanGeometry.IsConvexPolygon p) : ∃ (i : Fin n), { d : ℝ | ∃ j : Fin n, j ≠ i ∧ d = dist (p i) (p j) }.ncard ≥ n / 2

theorem agoh_giuga : AgohGiugaCongr

theorem beck_fiala_conjecture : ∃ C : ℝ, 0 < C ∧ ∀ (n m t : ℕ) (S : Fin m → Finset (Fin n)), (∀ j, (Finset.univ.filter fun i => j ∈ S i).card ≤ t) → ∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧ ∀ i, |∑ j ∈ S i, χ j| ≤ C * Real.sqrt t

theorem brocard_conjecture (n : ℕ) (hn : 1 ≤ n) : letI prev := n.nth Nat.Prime; letI next := (n+1).nth Nat.Prime; 4 ≤ ((Ioo (prev^2) (next^2)).filter Nat.Prime).card

theorem buchi_problem_M5 : IsBuchi 5

theorem charmichaelTotient : ∀ ⦃n : ℕ⦄, 0 < n → CarmichaelTotientFor n

theorem pillais_conjecture (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : { (x, y, m, n) : (ℕ × ℕ × ℕ × ℕ) | 1 < x ∧ 1 < y ∧ 1 < m ∧ 1 < n ∧ (m, n) ≠ (2, 2) ∧ a * x^n - b * y^m = c }.Finite

theorem Tunnell_odd_converse (n : ℕ) (hsqf : Squarefree n) (hodd : Odd n) : 2 * (A n).ncard = (B n).ncard → congruentNumber n

theorem new_mersenne_conjecture (p : ℕ) (hp : Odd p) : NewMersenneConjectureStatement p

theorem dickson_conjecture (fs : Finset ℤ[X]) (hfs : ∀ f ∈ fs, f.degree = 1 ∧ BunyakovskyCondition f) (hfs' : SchinzelCondition fs) : Infinite {n : ℕ | ∀ f ∈ fs, (f.eval (n : ℤ)).natAbs.Prime}

theorem eulers_sum_of_powers_conjecture (n k b : ℕ) (hn : 1 < n) (hk : 5 < k) (a : Fin n → ℕ) (ha : ∀ i, a i > 0) (hsum : ∑ i, (a i) ^ k = b ^ k) : k ≤ n

theorem feit_thompson_primes (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (h : p < q) : ¬ (q ^ p - 1) / (q - 1) ∣ (p ^ q - 1) / (p - 1)

theorem gap_conjecture : ∀ (G : Type) [Group G] (S : Set G), S.Finite → Subgroup.closure S = ⊤ → HasSuperPolynomialGrowth G → ∃ C : ℕ, 0 < C ∧ ∀ᶠ n : ℕ in atTop, Real.exp (Real.sqrt (n : ℝ)) ≤ (GrowthFunction S (C * n) : ℝ)

theorem graceful_tree_conjecture {V : Type*} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree) : let m := T.edgeFinset.card ∃ f : V → ℕ, Function.Injective f ∧ (∀ v, f v ≤ m) ∧ T.edgeFinset.image (fun e => e.lift ⟨fun u v => Int.natAbs ((f u : ℤ) - (f v : ℤ)), fun u v => by show ((f u : ℤ) - f v).natAbs = ((f v : ℤ) - f u).natAbs rw [← Int.natAbs_neg, neg_sub]⟩) = Finset.Icc 1 m

theorem HadamardConjecture (k : ℕ) : ∃ M, IsHadamard (n := 4 * k) M

theorem hall_conjecture : HallConjectureExp 2⁻¹

theorem exists_isWallSunSunPrime : ∃ p, IsWallSunSunPrime p

theorem juggler_conjecture (n : ℕ) (hn : n > 0) : ∃ m, jugglerStep^[m] n = 1

theorem kummer_vandiver (p : ℕ+) (hp : p.Prime) : ¬ ↑p ∣ (classNumber (maximalRealSubfield (CyclotomicField p ℚ)))

theorem KotheConjecture (I J : Ideal R) (hI : IsNil I) (hJ : IsNil J) : IsNil (I + J)

theorem lander_parkin_selfridge : ∀ (k n m : ℕ) (x : Fin n → ℕ) (y : Fin m → ℕ), 0 < n → 0 < m → (∀ i, 0 < x i) → (∀ j, 0 < y j) → (∀ i j, x i ≠ y j) → ∑ i, x i ^ k = ∑ j, y j ^ k → k ≤ n + m

theorem lehmer_mahler_measure_problem : ∃ μ : ℝ, ∀ f : ℤ[X], μ > 1 ∧ (mahlerMeasureZ f > 1 → mahlerMeasureZ f ≥ μ)

theorem local_uniformization (k F : Type*) [Field k] [Field F] [Algebra k F] [Algebra.EssFiniteType k F] (p : ℕ) [Fact p.Prime] [CharP k p] (𝒪 : ValuationSubring F) (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) : 𝒪.HasLocalUniformization k

theorem lonely_runner_conjecture (n : ℕ) (speed : Fin n ↪ ℝ) (lonely : Fin n → ℝ → Prop) (lonely_def : ∀ r t, lonely r t ↔ ∀ r2 : Fin n, r2 ≠ r → dist (t * speed r : UnitAddCircle) (t * speed r2) ≥ 1 / n) (r : Fin n) : ∃ t ≥ 0, lonely r t

theorem volume_eq_sofaConstant_iff_congruent_gerversSofa (s : Set ℝ²) (hs : ∃ m, IsMovingSofa s m) : volume s = sofaConstant ↔ ∃ g : E(2), s = g '' gerversSofa

theorem n_dim_euler_brick_existence :

theorem irrational_seven : ∃ x, Irrational x ∧ riemannZeta 7 = x

theorem pierce_birkhoff_conjecture {n : ℕ} (f : (Fin n → ℝ) → ℝ) (hf : IsPiecewiseMvPolynomial f) : ∃ (ι κ : Type) (g : ι → κ → MvPolynomial (Fin n) ℝ), Finite ι ∧ Finite κ ∧ ∀ x, f x = ⨆ i, ⨅ j, MvPolynomial.eval x (g i j)

theorem pollock_tetrahedral (N : ℕ) : ∃ f : Fin 5 → ℕ, N = ∑ i, tetrahedral (f i)

theorem sheehan_conjecture : ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], (∀ v, G.degree v = 4) → ∀ (v : V) (c : G.Walk v v), IsHamiltonianCycle G c → ∃ (w : V) (c' : G.Walk w w), IsHamiltonianCycle G c' ∧ c'.edges.toFinset ≠ c.edges.toFinset

theorem vaught_conjecture {L : FirstOrder.Language} (hL : Countable L.Symbols) {T : L.Theory} (hT : T.IsComplete) : numberOfCountableModels T ≤ Cardinal.aleph0 ∨ numberOfCountableModels T = Cardinal.continuum

theorem navier_stokes_breakdown_R3 (nu : ℝ) (hnu : nu > 0) : ∃ (u₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³), InitialVelocityConditionDecay u₀ ∧ ForceConditionDecay f ∧ ¬ (∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ f v p)

theorem poincare_conjecture : ConjectureFor 3

theorem erdos_194 : answer(False) ↔ ∀ k ≥ 3, ∀ r : ℝ → ℝ → Prop, IsStrictTotalOrder ℝ r → ∃ s : List ℝ, s.IsAPOfLength k ∧ (s.Pairwise r ∨ s.Pairwise (flip r))

theorem erdos_275 (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ) (H : ∃ k : ℤ, ∀ x ∈ Ico k (k + 2 ^ r), ∃ i, x ≡ a i [ZMOD n i]) (x : ℤ) : ∃ i, x ≡ a i [ZMOD n i]

theorem erdos_277 : answer(True) ↔ ∀ c : ℝ, ∃ n : ℕ, (σ 1 n : ℝ) > c * n ∧ ∀ (m : StrictCoveringSystem ℤ), ∃ i, (n : ℤ) ∉ m.moduli i

theorem erdos_31 : ∀ A : Set ℕ, A.Infinite → ∃ B : Set ℕ, B.HasDensity 0 ∧ ∀ᶠ n in atTop, n ∈ A + B

theorem erdos_437 : answer(True) ↔ ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℕ in atTop, (x : ℝ) ^ (1 - ε) < L x

theorem erdos_438 : Tendsto (fun N : ℕ ↦ (extremalSize N : ℝ) / (N : ℝ)) atTop (𝓝 ((11 : ℝ) / 32))

theorem erdos_482 : (∀ n : ℕ, 1 ≤ n → (a (2 * n + 1) : ℤ) - 2 * a (2 * n - 1) = (Real.digits (√2 / 2) 2 (n - 1) : ℕ)) ∧ Real.ofDigits (Real.digits (√2 / 2) 2) = √2 / 2

theorem erdos_484 : ∃ c : ℝ, 0 < c ∧ ∀ k : ℕ, 0 < k → ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → ∀ f : ℕ → Fin k, c * N ≤ (((Finset.Icc 1 N).filter fun n => ∃ a ∈ Finset.Icc 1 N, ∃ b ∈ Finset.Icc 1 N, a ≠ b ∧ f a = f b ∧ a + b = n).card : ℝ)

theorem erdos_519 : answer(True) ↔ ∃ c : ℝ, 0 < c ∧ ∀ (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ), z ⟨0, hn⟩ = 1 → ∃ k : Fin n, c < ‖powerSum z (k.val + 1)‖

theorem erdos_645 (c : ℕ → Bool) : ∃ x d, 0 < x ∧ x < d ∧ (∃ C, c x = C ∧ c (x + d) = C ∧ c (x + 2 * d) = C)

theorem erdos_646 : answer(True) ↔ ∀ S : Finset ℕ, (∀ p ∈ S, p.Prime) → {n : ℕ | ∀ p ∈ S, Even (padicValNat p (n !))}.Infinite

theorem erdos_690 : answer(False) ↔ ∀ k ≥ 1, ∀ d : ℕ → ℝ, (∀ p, p.Prime → (kthPrimeFactorSet k p).HasDensity (d p)) → IsUnimodalOnPrimes d

theorem erdos_728 : answer(True) ↔ ∀ᶠ ε : ℝ in 𝓝[>] 0, ∀ C > (0 : ℝ), ∀ C' > C, ∃ a b n : ℕ, 0 < n ∧ ε * n < a ∧ ε * n < b ∧ a ! * b ! ∣ n ! * (a + b - n)! ∧ a + b > n + C * log n ∧ a + b < n + C' * log n

theorem isWeakGiuga_iff_prime_dvd {n : ℕ} (hn : n.Composite) : IsWeakGiuga n ↔ ∀ p ∈ n.primeFactors, p ∣ (n / p - 1)

theorem beck_fiala_theorem (n m t : ℕ) (ht : 1 ≤ t) (S : Fin m → Finset (Fin n)) (hdeg : ∀ j, (Finset.univ.filter fun i => j ∈ S i).card ≤ t) : ∃ χ : Fin n → ℝ, (∀ j, χ j = 1 ∨ χ j = -1) ∧ ∀ i, |∑ j ∈ S i, χ j| ≤ 2 * (t : ℝ) - 1

theorem brocard_conjecture.ferreira_large_n : ∀ᶠ n in atTop, letI prev := n.nth Nat.Prime; letI next := (n+1).nth Nat.Prime; 4 ≤ ((Ioo (prev^2) (next^2)).filter Nat.Prime).card

theorem carchimaelTotient_bound {n : ℕ} (hn : 0 < n) (hn' : n < 10 ^ (10 ^ 10)) : CarmichaelTotientFor n

theorem eulers_sum_of_powers_conjecture.false_for_k4 : ¬ (∀ (n b : ℕ) (_ : 1 < n) (a: Fin n → ℕ) (_ : ∀ i, a i > 0) (_ : ∑ i, (a i) ^ 4 = b ^ 4), 4 ≤ n)

theorem GromovPolynomialGrowthTheorem [Group.FG G] : HasPolynomialGrowth G ↔ Group.IsVirtuallyNilpotent G

theorem jacobian_conjecture {k : Type} [CommRing k] [Nontrivial k] : answer(False) ↔ ∀ {σ : Type} [Fintype σ] [DecidableEq σ], JacobianConjectureProp k σ

theorem jacobson_conjecture_of_right_noetherian : answer(False) ↔ ∀ (R : Type) [Ring R] [IsRightNoetherianRing R], JacobsonConjectureFor R

theorem bounded_gap_legendre (H : ∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime < (n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c)) : ∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

theorem abelian_is_leinster_iff_cyclic_perfect (G : Type*) [CommGroup G] [Fintype G] : IsLeinster G ↔ IsCyclic G ∧ Nat.Perfect (Fintype.card G)

theorem local_uniformization_of_charZero (k F : Type*) [Field k] [Field F] [Algebra k F] [Algebra.EssFiniteType k F] [CharZero k] (𝒪 : ValuationSubring F) (hk : ∀ x : k, algebraMap k F x ∈ 𝒪) : 𝒪.HasLocalUniformization k

theorem pierce_birkhoff_conjecture_dim_one (f : ℝ → ℝ) (hf : IsPiecewisePolynomial f) : ∃ (ι κ : Type) (g : ι → κ → Polynomial ℝ), Finite ι ∧ Finite κ ∧ ∀ x, f x = ⨆ i, ⨅ j, Polynomial.eval x (g i j)

theorem snake_small_dimensions : map LongestSnakeInTheBox (range 9) = [0, 1, 2, 4, 7, 13, 26, 50, 98]

theorem lovasz_plummer_conjecture : ∃ c : ℝ, 0 < c ∧ ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], (∀ v, G.degree v = 3) → G.IsBridgeless → (2 : ℝ) ^ (c * Fintype.card V) ≤ perfectMatchingCount G

theorem shitov_upper_bound : ∃ f : ℝ → ℝ, f =o[atTop] (fun n : ℝ => n ^ 3) ∧ ∀ {α : Type*} {σ : Type*} [Fintype σ] (M : DFA α σ) (hM : M.IsSynchronizing) , ∃ w : List α, M.IsSynchronizingWord w ∧ (w.length : ℝ) ≤ (7 / 48 + 2 * 15625 / 1597536) * (Fintype.card σ : ℝ) ^ 3 + f (Fintype.card σ : ℝ)

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]

theorem implies_riemannHypothesis : type_of% (generalized_riemann_hypothesis 1 1) ↔ RiemannHypothesis

theorem f_zero_eq : f 0 = 0

theorem two_not_mem_pillaiPrimes : ¬ 2 ∈ PillaiPrimes

theorem greedySidonSet_isSidon (n : ℕ) : IsSidon (Finset.greedySidonBelow n : Set ℕ)

theorem greedyUnitFractionRem_zero (n : ℕ) : greedyUnitFractionRem .univ (1 / n) 0 = 0

theorem erdos_287.test.best_possible : let s : Fin 3 → ℕ := ![2, 3, 6] StrictMono s ∧ 1 < s 0 ∧ ∑ i : Fin 3, 1 / (s i : ℝ) = 1 ∧ max_gap 3 s = 3

theorem M_one : M 1 = 1

theorem maxSubsetSumAvoidingCard_three_four : maxSubsetSumAvoidingCard 3 4 = 2

theorem exists_three_full_then_two_full : ∃ n > 0, (3).Full n ∧ (2).Full (n + 1)

theorem erdos_445.test.small_example : Erdos445Prop 1 5 1

theorem tauPlus_six : tauPlus 6 = 3

private lemma evens_infinite : Set.Infinite {n : ℕ | Even n}

theorem bookNumber_bot {n : ℕ} : bookNumber (⊥ : SimpleGraph (Fin n)) = 0

theorem unitDistanceCounts_BddAbove (n : ℕ) : BddAbove <| unitDistanceCounts n

theorem not_isCoprimePowerfulAP4_zero_one : ¬ IsCoprimePowerfulAP4 0 1

theorem add_zero_right (n : Nat) : n + 0 = n

theorem add_comm_nat (a b : Nat) : a + b = b + a

theorem double_mod_two (n : Nat) : (2 * n) % 2 = 0

theorem lt_succ_self' (n : Nat) : n < n + 1

theorem sum_range_eleven : (List.range 11).foldl (· + ·) 0 = 55

theorem length_append' (xs ys : List Nat) : (xs ++ ys).length = xs.length + ys.length

theorem three_dvd_twelve : 3 ∣ 12

theorem two_add_two : 2 + 2 = 4

lemma isCarmichael_561 : IsCarmichael 561

theorem buchi_false_M0 : ¬ IsBuchi 0

theorem carchimichealTotientFor_zero : ¬ CarmichaelTotientFor 0

theorem lebesgue_nagell_solution_pos_one (p : ℕ) (hodd : Odd p) : (1 : ℤ) ^ 2 - 2 = (-1 : ℤ) ^ p

theorem congruentNumber_5 : congruentNumber 5

lemma graceful_tree_one_vertex : let T : SimpleGraph Unit := ⊥ let m := T.edgeFinset.card ∃ f : Unit → ℕ, Function.Injective f ∧ (∀ v, f v ≤ m) ∧ T.edgeFinset.image (fun e => e.lift ⟨fun u v => Int.natAbs ((f u : ℤ) - (f v : ℤ)), fun u v => by show ((f u : ℤ) - f v).natAbs = ((f v : ℤ) - f u).natAbs rw [← Int.natAbs_neg, neg_sub]⟩) = Finset.Icc 1 m

theorem growthFunction_not_polynomial_of_infinite [Infinite G] {S : Set G} (hS : S.Finite) (h : Subgroup.closure S = ⊤) {C : ℝ} (d : ℕ) : ∃ (n : ℕ), C * n ^ d < GrowthFunction S n

theorem isHadamard_equiv_isHadamard' (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : IsHadamard' M ↔ IsHadamard M

theorem elkies_bound (C : ℝ) : HallIneq C 2⁻¹ → C < 0.0215

theorem jacobian_conjecture_identity (H : JacobianConjectureProp k σ) : ∃ (G : RegularFunction k σ σ), G.comp (id k σ) = id k σ ∧ (id k σ).comp G = id k σ

theorem jugglerStep_36 : jugglerStep 36 = 6

theorem hasLocalUniformization_top {F : Type*} [Field F] {k : Type*} [Field k] [Algebra k F] (A : Subalgebra k F) [Algebra.FiniteType k A] [IsFractionRing A F] : (⊤ : ValuationSubring F).HasLocalUniformization k

theorem rev10_120 : rev10 120 = 21

theorem additionChainLength_first_values : [ℓ(1), ℓ(2), ℓ(3), ℓ(4), ℓ(5), ℓ(6), ℓ(7), ℓ(8), ℓ(9), ℓ(10)] = [0, 1, 2, 2, 3, 3, 4, 3, 4, 4]

theorem snake_zero_zero : LongestSnakeInTheBox 0 = 0