Prove2Me

Solving a four-equation linear system

Proved
WorkbookSource.problem_48161

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Solve the system: x−y+z−t=1x - y + z-t=1, 8x−4y+2z−t=168x -4 y + 2z-t=16, 27x−9y+3z−t=8127x -9y+ 3z-t=81, 64x−16y+4z−t=25664x-16y+4z-t=256.

Source: InternLM Lean-Workbook, record lean_workbook_48161 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_48161 (x y z t : ℝ) : x - y + z - t = 1 ∧ 8 * x - 4 * y + 2 * z - t = 16 ∧ 27 * x - 9 * y + 3 * z - t = 81 ∧ 64 * x - 16 * y + 4 * z - t = 256 ↔ x = 10 ∧ y = 35 ∧ z = 50 ∧ t = 24  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_48161; Apache-2.0

View graph