Prove2Me

Factorial arithmetic identity #24602

Proved
WorkbookCorrected.plus_24602

by carlok · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmeticcorrectedelementaryworkbook

The elementary natural-number / rational identity

12∗10∗8∗6∗4/(5!)=19212 * 10 * 8 * 6 * 4 / (5!) = 192

holds by direct arithmetic evaluation.

Formalization Note: This corrects Lean-Workbook record lean_workbook_plus_24602, which omitted a compilable colon/type annotation and/or used a preamble of only Mathlib.Analysis.Complex.Basic.

Source: InternLM Lean-Workbook, record lean_workbook_plus_24602 (Apache-2.0).

Preamble
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic.NormNum
Formal statement
theorem WorkbookCorrected.plus_24602 : 12 * 10 * 8 * 6 * 4 / (Nat.factorial 5) = 192 := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook; record lean_workbook_plus_24602; Apache-2.0; corrects Open node d1b49dc0-21c9-4838-9e76-9e50b8de2560

View graph