Skip to content

feat(ErdosProblems/741): solution for variants.upper #3778

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mo271 merged 4 commits into from
Apr 24, 2026
Merged

feat(ErdosProblems/741): solution for variants.upper #3778

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9d49204
feat(ErdosProblems/741): solution for `variants.upper`
mo271 Apr 16, 2026
4120c04
remove long proof
mo271 Apr 24, 2026
03ff32e
uncomment
mo271 Apr 24, 2026
85fd914
whitespace
mo271 Apr 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions FormalConjectures/ErdosProblems/741.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,9 +61,12 @@ theorem erdos_741.variants.lower : answer(sorry) ↔ ∀ A : Set ℕ, 0 < lowerD
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?

The DeepMind prover agent found a formal proof for this statement
-/
@[category research open, AMS 5]
theorem erdos_741.variants.upper : answer(sorry) ↔ ∀ A : Set ℕ, 0 < upperDensity (A + A) → ∃ A₁ A₂,
@[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.variants.upper : answer(True) ↔ ∀ A : Set ℕ, 0 < upperDensity (A + A) → ∃ A₁ A₂,
A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < upperDensity (A₁ + A₁)
∧ 0 < upperDensity (A₂ + A₂) := by
sorry
Expand Down
Loading