theorem cantor_diag {α : Type} (f : α → Set α) : ¬ Function.Surjective f := Function.cantor_surjective f

theorem identity_mob {α : Type} (a : α) : a = a := by rfl

theorem identity_prod {α : Type} (a : α) : a = a := by rfl

/-- 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

@[category test, AMS 11] theorem isBehrend_of_contains_one {ι : Type*} (A : ι → ℕ) (h : 1 ∈ Set.range A) : IsBehrend A := by rw [IsBehrend, Set.HasDensity] exact tendsto_atTop_of_eventually_const (i₀ := 1) fun n hn ↦ by simp [multiplesOf_eq_univ A h, Set.partialDensity] lia -- closed: sorry-free in formal-conjectures @ b5389792

/-- 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

open Filter open scoped Topology Real abbrev IsSumDistinctSet (A : Finset ℕ) (N : ℕ) : Prop := A ⊆ Finset.Icc 1 N ∧ (fun (⟨S, _⟩ : A.powerset) => S.sum id).Injective theorem erdos1_least_N_3 : IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3 } 4 := by refine ⟨⟨{1, 2, 4}, ?_⟩, ?_⟩ · simp refine ⟨by decide, ?_⟩ let P := Finset...

@[category research solved, AMS 11] theorem fixture_fc_pipeline (n : ℕ) : 0 < n.factorial := Nat.factorial_pos n