Erdős problem 198 · problems.science

The answer is no; Erdős and Graham report this was proved by Baumgartner, presumably referring to the paper [Ba75], which does not state this exactly, but the following simple construction is implicit in [Ba75].

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

198.lean

Retained formal statement4 of 4

In fact one such sequence is $n! + n$ .

This was found and proved by AlphaProof.

It also found $(n + 1)! + n$ .

FormalConjectures/ErdosProblems/198.leanErdos198.erdos_198.variants.concrete1 lineExact file

1∃ A, A = {x | ∃ n, n.factorial + n = x} ∧ IsSidon A ∧ ∀ (Y : Set ℕ), Y.IsAPOfLength ⊤ → (A ∩ Y).Nonempty

SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science