Conjectures.io

Number theory

Erdős 242 - schinzel generalization

Schinzel conjectured (see [Si56]) the generalisation that, for any fixed aa, if nn is sufficiently large in terms of aa then there exist distinct integers 1≤x<y<z1\leq x < y < z such that an=1x+1y+1z.\frac{a}{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

∀ (a : ℕ), 0 < a → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ x y z, 1 ≤ x ∧ x < y ∧ y < z ∧ ↑a / ↑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.variants.schinzel_generalization" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/242.lean

Source type SHA-256
sha256:b141d6fbf1dbb8c97357e6826fd853a1f6d34d12832fa021225f8b1a4afcb6b5
Task id
fc-379fc029-variants-schinzel-generalization-4d2ea57cb3-formalized-v1
Task commitment
sha256:61ad2964428252cededba1cbb869cac6949573d670051a59220beb80ff4dacdb

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.