lean_workbook_plus_67677

Proved

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

Find a solution for $(x,y,z)$ in the form $(5^n*2^{n-1}, 10^n, 5^{2n} *2^{2n-1})$ where $n$ is a natural number.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67677 (x y z : ℕ) (n : ℕ) (hn: x = 5^n*2^(n-1) ∧ y = 10^n ∧ z = 5^(2*n)*2^(2*n-1)) : x*y*z = 10^n * (5^n * 2^(n-1)) * (5^(2*n) * 2^(2*n-1))   :=  by sorry

Source

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

View graph