Comparing two large integer powers
ProvedWorkbookSource.problem_33828lean-workbooksource-checked
The following strict numerical comparison holds:
Source: InternLM Lean-Workbook, record lean_workbook_33828 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_33828 : (2^(33)*3^(10) : ℝ) > 5^(21) := by sorry
Source