AlphaProof: when Lean became the training signal

Problem 1 of IMO 2024 asks for all real numbers $\alpha$ satisfying the condition above. Write $S_n = \sum_{k=1}^{n} \lfloor k\alpha \rfloor$. The answer is that $\alpha$ must be an even integer.

Even integers work: if $\alpha = 2m$ then every floor is exact and $S_n = 2m \cdot \frac{n(n+1)}{2} = m\, n(n+1)$, a multiple of $n$.

Adding $2$ to $\alpha$ adds $\sum_{k=1}^{n} 2k = n(n+1)$ to $S_n$ (and subtracting $2$ removes it), which does not change divisibility by $n$. So we may assume $0 \le \alpha < 2$ and must show $\alpha = 0$.

If $0 \le \alpha < 1$, suppose $\lfloor k\alpha \rfloor = 0$ for all $k < n$. Then $S_n = \lfloor n\alpha \rfloor$, which lies between $0$ and $n - 1$ and is divisible by $n$, so it is $0$. Hence $\lfloor n\alpha \rfloor = 0$ for every $n$, which forces $\alpha < 1/n$ for all $n$, so $\alpha = 0$.

If $1 \le \alpha < 2$, suppose $\lfloor k\alpha \rfloor = 2k - 1$ for all $k < n$ (true for $k = 1$). Then

Since $n \le \lfloor n\alpha \rfloor \le 2n - 1$, divisibility forces $\lfloor n\alpha \rfloor = 2n - 1$. So $n\alpha \ge 2n - 1$, that is $\alpha \ge 2 - \tfrac1n$, for every $n$, which contradicts $\alpha < 2$.

A human reader accepts “so we may assume $0 \le \alpha < 2$” at a glance. In Lean that step is a lemma about how $\lfloor x + 2k \rfloor$ and finite sums behave, and every inequality between $\lfloor n\alpha \rfloor$, $n$ and $2n - 1$ has to be justified. The reward is that the checker's verdict is binary and needs no human grader, which is what makes it usable as a training signal: a system can try many proof attempts and learn from exactly those the kernel accepts.