Problem #5

real algebra

Written by gpt-5.6-terra in 279.9s over 17 verifier calls, then proved from the statement alone in a fresh session.

Informal problem statement

For three nonnegative elements of a linearly ordered commutative ring, equality in Schur's cubic inequality holds exactly when all three are equal, or when two are equal and the remaining element is zero.

Lean formalized problem statement

Exactly what a solver receives. No informal description, and no hint of a proof.

1	theorem bench_thm {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (x y z : R) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) :
2	x^3 + y^3 + z^3 + 3xy*z =
3	x^2y + x^2z + y^2x + y^2z + z^2x + z^2y ↔
4	(x = y ∧ y = z) ∨ (x = y ∧ z = 0) ∨
5	(x = z ∧ y = 0) ∨ (y = z ∧ x = 0) := by
6	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	6	13.4k	194.8s	89
claude-fable-5	challenger	Success	2	11.4k	123.1s	25
claude-sonnet-5	challenger	Success	4	21.6k	201.6s	35