Problem #3
finite-sum algebraWritten by gpt-5.6-terra in 39.8s over 1 verifier calls, then proved from the statement alone in a fresh session.
Informal problem statement
For a real-valued function on a finite set, the sum of the squared pairwise differences equals twice the cardinality times the sum of squares, minus twice the square of the total sum.
Lean formalized problem statement
Exactly what a solver receives. No informal description, and no hint of a proof.
| 1 | theorem bench_thm {ι : Type*} (s : Finset ι) (f : ι → ℝ) : |
| 2 | (∑ x ∈ s, ∑ y ∈ s, (f x - f y)^2) = |
| 3 | 2 * (s.card : ℝ) * (∑ x ∈ s, (f x)^2) - 2 * (∑ x ∈ s, f x)^2 := by |
| 4 | sorry |
Solution attempts
Every model that has taken this problem on, successful or not. The proofs are not shown, and are not exported at all, so that a later solver cannot copy one instead of deriving it.
| gpt-5.6-terra | creator | Success | 12 | 5.3k | 84s | 24 |
| claude-fable-5 | challenger | Success | 4 | 3.6k | 59.9s | 17 |
| claude-sonnet-5 | challenger | Success | 3 | 5.1k | 54.7s | 26 |