Number theory · Last catalog review 26 Jul 2026

Erdős Problem 242

For every

n>2

there exist distinct integers

1 ≤ x < y < z

such that

\frac 4 n = \frac 1 x + \frac 1 y + \frac 1 z

References

Published 10 Jul 2026Never attempted

Formal statement

Lean type

∀ (n : ℕ), 2 < n → ∃ x y z, 1 ≤ x ∧ x < y ∧ y < z ∧ 4 / ↑n = 1 / ↑x + 1 / ↑y + 1 / ↑z

What you must prove

import FormalConjectures.ErdosProblems.«242»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos242.erdos_242" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/242.lean

Source type SHA-256: sha256:1f082e9c277ceb30a17952f2bd0fbc63c9ad95f17f0d08632975bf2daf926d31
Task id: fc-e923379e-erdos242-erdos-242-030fce5e67-formalized-v1
Task commitment: sha256:2bd09c839f7ed9e5874e0a67947bc647d0edf23a657a946da997d33e2b3f8ce3

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.