Let such that for all large andIs it true that there are infinitely many solutions to with and ?

claimed — no verifier run, no signed judgmentunreviewedOpen. Worked here; no verified result yet.

number theory · disproved · formalized (Lean) · 0 attempts

use this data

vela registry pull vfr_37aec80d874a0239
vela reproduce examples/erdos-problems

Formal proof

AMS 11 · solved (literature)

theorem erdos_331 :
    answer(False) ↔
      ∀ A B : Set ℕ,
      (fun (n : ℕ) ↦ (n : ℝ) ^ (1 / 2 : ℝ)) =O[atTop] (fun (n : ℕ) ↦ (count A n : ℝ)) →
      (fun (n : ℕ) ↦ (n : ℝ) ^ (1 / 2 : ℝ)) =O[atTop] (fun (n : ℕ) ↦ (count B n : ℝ)) →
      { s : ℕ × ℕ × ℕ × ℕ | let ⟨a₁, a₂, b₁, b₂⟩ := s
        a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧
        a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁ }.Infinite
formal-conjectures/331.lean ↗

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Verify this yourself

Run this command — the output must match these fingerprints.

vela reproduce examples/erdos-problems
  • packet.json · sha256 be91ca000748c914b2d3b887c7ae70697f3414250ec10d80c599c9c4b25db764

Search Vela

Search problems, results, contributors, and pages — or jump straight to an id.