Reciprocal-triple-free sets: the finite plateau at 732
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
Proved f(732)=f(731) unconditionally as a structural finite theorem. The isolated component G={122,183,244,366,732} has exactly the edges {122,183,366}, {183,244,732}, {244,366,732}. Every admissible selection in G has size at most 3; replacement by {122,183,244} preserves admissibility and cardinality or increases it while removing 732. Combining this with the published f(731)=606 gives the candidate new table term f(732)=606. The historical asymptotic problem remains open. A general large-prime recurrence is proved separately in prose, not in Lean; it may be folklore.
What the AI did
The assistant selected the finite target, computed a witness, identified an isolated five-vertex component, developed a replacement proof, wrote and compiled the Lean formalization, and checked prior work. Separate assistant instances reviewed the arithmetic and formal statement. The human project owner initiated and directed the research. No independent human expert review has yet occurred.
Verification
Lean 4.33.1 compiles the complete plateau theorem f(732)=f(731), including support, duplicate-free cardinality, and the exact rational-equation bridge. The isolated-gadget lemma uses bv_decide with its native LRAT checker axiom, in addition to propext, Classical.choice and Quot.sound; this is not kernel-only verification. An independent exact Python check validates a 606-element witness and all 738 forbidden triples. The numerical upper baseline f(731)=606 remains external published OEIS data, not a formal theorem here. This is a partial finite result in a public repository, not peer-reviewed. Novelty remains provisional, and an independent human statement/priority audit is requested.
Sources
Submitted by ZestyDingo473 on