Aristotle 自主发现并 Lean 验证三元素负数 postage-stamp 分类，人类数学家随后给出新证明

van Doorn、Monticone 与 Nathanson 于 10 月 14 日发布三元素 h-bases 的正负性分类：若允许集合 A 含负整数，则对 k=2，最大覆盖区间 n_h^flat(2) 在 h 为奇数或 h=4 时严格小于经典非负值 n_h(2)，而在偶数 h≠4 时两者相等。论文明确说明，这些 comparison results 的原始证明由 Harmonic 的 formal reasoning agent Aristotle 自主发现并在 Lean 中形式验证；论文作者随后给出新的、人类可读证明，并注明 Aristotle 的原始解使该工作成为可能。该事件因此同时具备 autonomous discovery、formal verification 与 human reconstruction 三层证据。