Conjectures.io

Number theory

Erdős 242

For every n>2n>2 there exist distinct integers 1≤x<y<z1 ≤ x < y < z such that 4n=1x+1y+1z\frac 4 n = \frac 1 x + \frac 1 y + \frac 1 z.

References

  • Si56 Sierpiński, W., Sur les décompositions de nombres rationnels en fractions primaires. Mathesis (1956), 16--32.

No one has attempted this yet.

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-379fc029-erdos242-erdos-242-41ec7d6bf8-formalized-v1
Task commitment
sha256:e9aeb895aee78d0edef581543da3c3086649da9982acb18dd39c582ad94c9388

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.