Erdős problem 206 · problems.science

Let $x>0$ be a real number. For any $n\geq 1$ let $R_n(x) = \sum_{i=1}^n\frac{1}{m_i}<x$ be the maximal sum of $n$ distinct unit fractions which is $<x$ .

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/206.lean

Formal Conjectures

FormalConjectures/ErdosProblems/206.leanErdos206.erdos_2061 lineExact file

1False ↔ ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), Erdos206.EventuallyGreedy x

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:206
PLBY Lean proofsErdosProblems.Erdos206

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Formalization
Erdős AI contributions wiki · 28 Apr, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science