1. FormalConjectures
  2. ErdosProblems
  3. «741»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 741

References:

    erdosproblems.com/741

    [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.

open scoped Pointwiseopen Setnamespace Erdos741

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive upper density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive upper density?

This was proved by the DeepMind prover agent.

@[category research solved, AMS 5, formal_proof using formal_conjectures at "https://github.com/google-deepmind/formal-conjectures/blob/9d492049e42167b0d2fd58a9e91da3bf160172b5/FormalConjectures/ErdosProblems/741.lean#L228"] theorem erdos_741.parts.i : answer(True) ↔ ∀ A : Set ℕ, 0 < upperDensity (A + A) → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < upperDensity (A₁ + A₁) ∧ 0 < upperDensity (A₂ + A₂) := ⊢ True ↔ ∀ (A : Set ℕ), 0 < (A + A).upperDensity → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).upperDensity ∧ 0 < (A₂ + A₂).upperDensity All goals completed! 🐙

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive lower density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive lower density?

@[category research open, AMS 5] theorem erdos_741.variants.lower : answer(sorry) ↔ ∀ A : Set ℕ, 0 < lowerDensity (A + A) → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < lowerDensity (A₁ + A₁) ∧ 0 < lowerDensity (A₂ + A₂) := ⊢ True ↔ ∀ (A : Set ℕ), 0 < (A + A).lowerDensity → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).lowerDensity ∧ 0 < (A₂ + A₂).lowerDensity All goals completed! 🐙

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive density in the literal sense that its natural density exists and is positive. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive density in this sense?

This was disproved by the DeepMind prover agent.

@[category research solved, AMS 5, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/486bc8afae062b6711cd16d3466d651ee2880a52/FormalConjectures/ErdosProblems/741.lean#L1449"] theorem erdos_741.variants.exact_density : answer(False) ↔ ∀ A : Set ℕ, HasPosDensity (A + A) → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ HasPosDensity (A₁ + A₁) ∧ HasPosDensity (A₂ + A₂) := ⊢ False ↔ ∀ (A : Set ℕ), (A + A).HasPosDensity → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ (A₁ + A₁).HasPosDensity ∧ (A₂ + A₂).HasPosDensity All goals completed! 🐙

Is there a basis $A$ of order $2$ such that if $A=A_1\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?

This was proved by DeepMind prover agent.

@[category research solved, AMS 5, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/486bc8afae062b6711cd16d3466d651ee2880a52/FormalConjectures/ErdosProblems/741.lean#L1629"] theorem erdos_741.parts.ii : answer(True) ↔ ∃ A : Set ℕ, IsAddBasisOfOrder (A ∪ {0}) 2 ∧ ∀ A₁ A₂, A = A₁ ∪ A₂ → Disjoint A₁ A₂ → ¬ (IsSyndetic (A₁ + A₁) ∧ IsSyndetic (A₂ + A₂)) := ⊢ True ↔ ∃ A, (A ∪ {0}).IsAddBasisOfOrder 2 ∧ ∀ (A₁ A₂ : Set ℕ), A = A₁ ∪ A₂ → Disjoint A₁ A₂ → ¬(IsSyndetic (A₁ + A₁) ∧ IsSyndetic (A₂ + A₂)) All goals completed! 🐙end Erdos741