Skip to content

Erdős problem 123

Start work

Let a,b,c>1a,b,c>1 be pairwise coprime integers. Is every large integer a sum of distinct numbers of the form akblcma^k b^l c^m (k,l,m≥0k,l,m\ge 0), none dividing another?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/123.lean

Formal Conjectures

FormalConjectures/ErdosProblems/123.leanErdos123.erdos_1236 linesExact file
True ↔  ∀ a > 1,    ∀ b > 1,      ∀ c > 1,        Erdos123.PairwiseCoprime a b c →          Erdos123.IsDComplete (↑(Submonoid.powers a) * ↑(Submonoid.powers b) * ↑(Submonoid.powers c))
SolvedProof has a holelean4external proof

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

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:123
  • PLBY Lean proofsErdosProblems.Erdos123

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry