Prove2Me

lean_workbook_plus_43746

Proved

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

Write x2=mn {x\over 2} = {m\over n} with m∈Z,n∈N,gcd⁡(m,n)=1 m\in\mathbb{Z},n\in\mathbb{N},\gcd (m,n) = 1 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43746 (x : ℤ) : ∃ m n : ℤ, x / 2 = m / n ∧ m.gcd n = 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph