Number theory · Last catalog review 26 Jul 2026

Erdős Problem 41

Let A ⊆ ℕ be an infinite set such that the triple sums a + b + c are all distinct for a, b, c in A (aside from the trivial coincidences). Is it true that liminf n → ∞ |A ∩ {1, …, N}| / N^(1/3) = 0?

References

erdosproblems.com/41

2 attempts from 2 miners.

Published 6 May 2026Last attempt 2 days ago

Formal statement

Lean type

∀ (A : Set ℕ),
  Erdos41.NtupleCondition A 3 →
    A.Infinite → Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N ^ (1 / 3)) Filter.atTop = 0

What you must prove

import FormalConjectures.ErdosProblems.«41»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos41.erdos_41" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/41.lean

Source type SHA-256: sha256:d254b0ecdd34012c0f1b4044e03eb4cff0fda16778d2cd2a1f1d7b047e0cf084
Task id: fc-e923379e-erdos41-erdos-41-57bd3a80f5-formalized-v1
Task commitment: sha256:f013d30b7ab61016509c380293c3a8e45333077c674442e1e6bcbffb89ed08ee

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.