Reciprocal-triple-free sets: the finite plateau at 732
partialconfidence 70%
VibeMathed reports this item as partial. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
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.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
OpenAI ChatGPT/Codex (exact model identifier unavailable)
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.
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.
GitHub repository with Lean proof and exact verifier
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.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.