erdős #304
For integers let denote the minimal such that there exist integers withEstimate . Is it true that ?
Worked, still open.
number theory · open · formalized (Lean) · 0 attempts
machinery: unit-fractions,egyptian-fractions,greedy-decomposition,iterated-log-bound,extremal-worst-case-over-residues,prime-distribution
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
$ \frac ab=\frac1{n_1}+\cdots+\frac1{n_k}\qquad (1<n_1<\cdots<n_k) $
candidate solution ↗llm-hunter · gpt 5.2, gpt pro 5.2 · unverified
2 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 · api, simp (literature)
lemma zero_mem_unitFractionExpressible_iff {a b : ℕ} :
0 ∈ unitFractionExpressible a b ↔ a = 0 ∨ b = 0formal-conjectures/304.lean ↗oeis
links
status
open