/-- If $A\subseteq\{1, ..., N\}$ with $|A| = n$ is such that the subset sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$ then $$ N \gg 2 ^ n. $$ -/ @[category research open, AMS 5 11] theorem erdos_1 : ∃ C > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℕ) (_ : IsSumDistinctSet A N), N ≠ 0 → C * 2 ^ A.card < N := by sorry

/-- Does every almost-disjoint family of countably infinite sets whose pairwise intersections all have size ≠ 1 have Property B? Formally: let `α` be any type, let `(A_i)_{i ∈ I}` be a family of countably infinite subsets of `α` such that for all `i ≠ j`, the intersection `A_i ∩ A_j` is finite and `|A_i ∩ A_j| ≠ 1`. Does there exist a 2-colouring `f : α → Fin 2` such that no `A_i` is monochromatic? This is an open question about Property B for almost-disjoint families with a forbidden intersection size of 1. **Note:** This generalises the formulation in which the ground set is `ℕ`. Since every countably infinite set is in bijection with `ℕ`, the two formulations are equivalent, but working over an arbitrary ground type makes the statement apply immediately to, e.g., almost-disjoint families of countable subsets of an uncountable space. -/ @[category research open, AMS 3 5] theorem erdos_602 : answer(sorry) ↔ ∀ {α : Type*} {I : Type*} (A : I → Set α), (∀ i, (A i).Countable ∧ (A i).Infinite) → (∀ i j, i ≠ j → (A i ∩ A j).Finite) → (∀ i j, i ≠ j → Set.ncard (A i ∩ A j) ≠ 1) → HasPropertyB I A := by sorry

/-- Does every set of $n$ distinct points in $\mathbb{R}^2$ contain at most $n^{1+O(\frac{1}{\log\log n})}$ many pairs which are distance $1$ apart? This was [disproved](https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf) by an internal model at OpenAI, which constructed (for infinitely many $n$) a set $P$ of $n$ points in $\mathbb{R}^2$ such that the number of unit distance pairs in $P$ is at least $n^{1+c}$, where $c > 0$ is an absolute constant. -/ @[category research solved, AMS 52] theorem erdos_90 : answer(False) ↔ ∃ (O : ℕ → ℝ) (hO : O =O[atTop] (fun n => 1 / (n : ℝ).log.log)), (fun n => (maxUnitDistances n : ℝ)) =ᶠ[atTop] fun (n : ℕ) => (n : ℝ) ^ (1 + O n) := by sorry

/-- Let $A\subset\mathbb{N}$ be infinite such that $\sum_{a \in A} \frac{1}{a} = \infty$. Must there exist some $k\geq 1$ such that almost all integers have a divisor of the form $a+k$ for some $a\in A$? This was formalized in Lean by Alexeev using Aristotle. -/ @[category research solved, AMS 11, formal_proof using lean4 at "https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos26.lean"] theorem erdos_26 : answer(False) ↔ ∀ A : ℕ → ℕ, StrictMono A → IsThick A → ∃ k, IsBehrend (A · + k) := by sorry

/-- Fermat's Last Theorem is true -/ theorem Wiles_Taylor_Wiles : FermatLastTheorem := by -- Suppose Fermat's Last Theorem is false by_contra h -- then there exists a Frey package obtain ⟨P : FreyPackage⟩ := FreyPackage.of_not_FermatLastTheorem h -- but there is no Frey package exact P.false

-- If aˣ + bʸ = cᶜ with x, y, z > 2, then a, b, c share a common prime factor. theorem beal (a b c x y z : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hx : 2 < x) (hy : 2 < y) (hz : 2 < z) (h : a ^ x + b ^ y = c ^ z) : ∃ p : ℕ, Nat.Prime p ∧ p ∣ a ∧ p ∣ b ∧ p ∣ c :=

-- There is always a prime between n² and (n+1)² for every positive n. theorem legendre (n : ℕ) (hn : 0 < n) : ∃ p : ℕ, n^2 < p ∧ p < (n + 1)^2 ∧ Nat.Prime p :=

-- Every even integer greater than 2 is the sum of two primes. theorem goldbach (n : ℕ) (hn : 2 < n) (heven : Even n) : ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ p + q = n :=

-- There are infinitely many primes of the form 2ⁿ - 1. theorem inf_mersenne_primes : ∀ N : ℕ, ∃ n : ℕ, N < n ∧ Nat.Prime (2^n - 1) :=

-- Does there exist an odd perfect number? -- (A number n is perfect if it equals the sum of its proper divisors.) theorem no_odd_perfect : ∀ n : ℕ, Odd n → ¬(∑ d ∈ Nat.divisors n \ {n}, d = n) :=