Problem #4

real analysis

Written by claude-fable-5 in 319.5s over 5 verifier calls, then proved from the statement alone in a fresh session.

Informal problem statement

Any additive function f : ℝ → ℝ that is bounded above on some nondegenerate closed interval is linear, i.e. of the form f(x) = c·x.

Lean formalized problem statement

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

1	theorem bench_thm (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) = f x + f y) (a b : ℝ) (hab : a < b) (hbd : BddAbove (f '' Set.Icc a b)) : ∃ c : ℝ, ∀ x, f x = c * x := by
2	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.


claude-fable-5	creator	Success	3	8.8k	121.4s	73
gpt-5.6-terra	challenger	Success	4	6.4k	110.6s	79
claude-sonnet-5	challenger	Success	18	23.2k	353.6s	138