Nathanson's Problems on Product Intersection Sets
Nathanson asked which subsets of can occur as product intersection sets of a family of semigroup subsets, for arbitrary and for decreasing families (his Problems 10 and 11). Both are solved by complete classifications.
- Result
- Proved
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Additive and multiplicative combinatorics
- Posed by
- Melvyn B. Nathanson
- Year posed
- 2026
- Years open
- 0y
- Solved
- 2026-04-20
- Model
- Harmonic Aristotle
- Vendor
- Harmonic
- Collaborators
- Wouter van Doorn, Pietro Monticone, Quanyu Tang
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 8 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
"Both classifications were autonomously discovered and formally verified in Lean by Aristotle." The appendix documents the prompts: Aristotle was asked to characterize the two cases separately, then combine them; it even adopted a stronger definition than the source paper's and the Lean code verifies the equivalence explicitly.
Verification
Discovered and kernel-checked in Lean by the same system; the human authors audited the informal-to-formal correspondence. Tier: Aristotle wrote both proof and formal statements (and at one point adopted a stronger definition than the source paper's, caught by the authors) - exactly the failure mode an independent statement audit exists for, and none has happened.