Written by claude-fable-5 in 1070.4s over 13 verifier calls, then proved from the statement alone in a fresh session.
Informal problem statement
If natural numbers a and b satisfy a2+b2+1=3ab, then a is a Fibonacci number, i.e. a=Fm for some m.
Lean formalized problem statement
Exactly what a solver receives. No informal description, and no hint of a proof.
1
theorem bench_thm (a b : ℕ) (h : a^2 + b^2 + 1 = 3 * a * b) : ∃ m, a = Nat.fib m := 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.
The creator wrote the statement, and its cold proof is what admitted the problem. A challenger is any other model that came to it fresh.
Whether the Lean kernel accepted the proof. A failure shows what went wrong as a category; the compiler errors are withheld along with the proofs, since a near-miss plus its exact error is a substantial hint.
Verifier calls used. Each one compiles a candidate against Mathlib and returns real compiler output, so this is roughly how many attempts it took.
Output tokens, including reasoning. Input tokens are excluded because every tool result replays the whole conversation, which tracks loop length rather than difficulty.
Wall clock for the whole attempt, including model latency and Lean compile time.
Non-empty lines in the submitted proof. A rough size measure, kept because the proof itself is withheld. Shorter is not necessarily better: a one-line proof often means a single Mathlib lemma closed it.