lean_workbook_plus_30442

Proved

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

Prove or disprove: Given $\alpha$ , an irrational real number, the set $\{ k\alpha - \lfloor k\alpha \rfloor : k \in \mathbb{N}\}$ is dense in $[0,1]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30442 (α : ℝ) (h : ¬ ∃ a : ℚ, α = a) :
  ∀ ε : ℝ, ε > 0 → ∃ k : ℕ, |k * α - ⌊k * α⌋| < ε   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph