lean_workbook_plus_53494

Proved

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

There are $9$ choices for the first digit, $9$ choices for the second, $8$ choices for the third, and $7$ choices for the fourth. Therefore, our answer is simply $9^2 \cdot 8 \cdot 7 = \textbf{(B) }4536.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53494 :
  9^2 * 8 * 7 = 4536   :=  by sorry

Source

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

View graph