Reciprocal-triple-free sets: finite maxima through 734
Let f(n) be the maximum size of a subset of {1,...,n} containing no three distinct a,b,c satisfying 1/a = 1/b + 1/c. A published finite frontier for Erdős problem 302 asks whether f(732) is 606 or 607, using the existing OEIS value f(731)=606.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Extremal sets avoiding distinct reciprocal triples
- Posed by
- Finite frontier: Erdős Frontier Atlas P302, recorded July 2026. Parent problem: Erdős and Graham (1980); the parent asymptotic problem is not solved.
- Year posed
- 2026
- Years open
- 0y
- Solved
- 2026-09-07
- Model
- OpenAI ChatGPT/Codex (exact model identifier unavailable)
- Vendor
- OpenAI
- Collaborators
- Sodelin (project owner and research direction)
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 4 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The Lean development proves f(732)=f(731), f(733)=f(732)+1 and f(734)=f(732)+2. The 732 step replaces an isolated five-vertex component without reducing an admissible set. Exact finite certificates show that neither 733 nor 734 belongs to a forbidden reciprocal triple with vertices at most 734, so each new vertex raises the maximum by one. Conditional on the published OEIS value f(731)=606, the resulting values are f(732)=606, f(733)=607 and f(734)=608. The historical asymptotic Erdős problem remains open. Priority is provisional; the elementary component argument may be folklore.
What the AI did
The assistant selected the 732 finite target, found the isolated-component replacement proof, computed exact witnesses and wrote the Lean formalization. Further assistant work proved the 733 and 734 transfers, added exact 607- and 608-element witnesses, and replaced native-checker finite steps with kernel-checked certificates. Separate assistant instances reviewed arithmetic and formal statements. Sodelin initiated and directed the research. No independent human expert review has occurred.
Verification
Lean 4.33.1 compiles the structural theorems through 734, including domain cardinality and the rational-equation bridge. At the current pinned source commit, the final theorems report only propext, Classical.choice and Quot.sound; the earlier bv_decide/native LRAT checker axiom has been removed. Closed finite certificates for the gadget and endpoints are kernel checked without axioms. Independent exact Python verifiers check 606-, 607- and 608-element witnesses and enumerate all 738 forbidden triples through 734. The numerical baseline f(731)=606 is external OEIS data, not a theorem proved here. The formal statement and priority remain unaudited by an independent human expert. This is a partial finite result in a public repository, not peer-reviewed.
Sources
Submitted by ZestyDingo473 on