Problem

erdos:399

False ↔ ¬∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n.factorial = x ^ k + y ^ k ∨ n.factorial + y ^ k = x ^ k)

Open Current State

Declared status: disproved (Lean)
Formalization: formalized
Subjects: number theoryfactorials
OEIS: N/A
Sources: source:erdos-ai-contributions-wikisource:erdos-problemssource:formal-conjecturessource:jayyhk-erdos-leansource:plby-lean-proofs
Statement: www.erdosproblems.com

Matching claims

0

No direct claims

This problem has no directly related claim record.

Browse this Repository’s Claims