What was already known
Nathanson defined these sets and asked whether unions are closed and which sets can arise. Intersection closure was known, but these full classifications were open.
AI involvement
Van Doorn, Monticone and Tang report that Aristotle autonomously discovered and Lean-verified the classifications. They supplied the problems, repaired the definition bridge and rewrote the exposition.
The v2 abstract and appendix expressly describe autonomous discovery of both classifications by Aristotle after human problem prompts.
Importance
Answers Nathanson’s Problems 10 and 11 through single-exclusion constructions and their products.
Limitations
The authors corrected a gap between Aristotle’s initially stronger decreasing definition and Nathanson’s definition. The Lean check is reported in the paper and was not locally rebuilt.
Technical verification
The authors report Lean verification of both classifications and of the equivalence correcting Aristotle's stronger definition. This is a source-reported machine check, without a local replay.
Formal checking
Lean 4 formal verification reported in the appendix and linked source file
- Checker
- Lean kernel through Aristotle's formalization
- Scope
- Theorem 1.1 for asymptotically strictly decreasing sequences, Theorem 1.2 for each cardinality of Q, and equivalence of the two decreasing definitions
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The human authors describe and rewrite the single-exclusion semigroup construction and product assembly, and explain the correction from Aristotle's stronger decreasing definition.
Correction and publication history
Answers Nathanson’s Problems 10 and 11 through single-exclusion constructions and their products.
Read this published revision