lean_workbook_plus_71443

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Given a real number $\alpha >0$ . Prove there exists a $n$ such that $\lfloor n^2\alpha \rfloor$ is even.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71443 (α : ℝ) (h : α > 0) : ∃ n : ℕ, Even (Int.floor (n^2 * α))   :=  by sorry

Source