/-
The verification environment.

Candidate declarations are never added to this file: each one is elaborated in its
own scratch file against this project's imports, so a broken candidate can never
break the environment the next candidate is checked in.

Anything you want every candidate to see -- a shared convention, a local notation --
belongs here.
-/
import Mathlib

namespace LeanBench

/-- Sanity check: if this fails, the toolchain and Mathlib do not agree. -/
theorem environment_ok : (2 : ℕ) + 2 = 4 := by norm_num

end LeanBench