Skip to content

Erdős problem 198

Start work

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

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

198.lean

Retained formal statement4 of 4

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

This was found and proved by AlphaProof.

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

FormalConjectures/ErdosProblems/198.leanErdos198.erdos_198.variants.concrete1 lineExact file
∃ 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.