theorem
proved
term proof
omega_six
show as:
view Lean formalization →
formal statement (Lean)
811theorem omega_six : omega 6 = 2 := by native_decide
proof body
Term-mode proof.
812
813/-- Ω(12) = 3 (since 12 = 2² × 3). -/