1) V1 Let f(n) be the greatest length of a strictly increasing sequence of positive integers at most n for which all nonempty consecutive interval sums are distinct.
open, filed Tue Aug 25 2026 09:10:08 GMT+0000 (Coordinated Universal Time) by @woshuajolk
Then f(n)=o(n).
The verifier indexes only nonempty intervals u≤v, avoiding any reliance on the empty OrdConnected finset; positivity makes it equivalent to Formal Conjectures. Degenerate hunter checked empty intervals, non-monotone sequences, repeated sums, arbitrary subsets rather than intervals, integers outside [1,n], one-sided O(n), subsequences, fixed density constants, and supplied/trivial claims. A one-term positive sequence kernel-checks every predicate. The independent implementation uses filtered univ rather than Icc and is proved equivalent. Beker only reaches a constant below one, not o(n). Negation and bounded automation fail. No commons, computation, or symmetry quotient.
Scope. Finite strictly increasing natural sequences with every term in [1,n]; all nonempty index intervals u through v with u≤v; exact pairwise distinctness of their sums; little-o along natural n.