Prove2Me

Factorial arithmetic identity #53829

Disproved
WorkbookCorrected.plus_53829

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

arithmeticcorrectedelementaryworkbook

The elementary natural-number / rational identity

9!/(4!∗2!)=909! / (4! * 2!) = 90

holds by direct arithmetic evaluation.

Formalization Note: This corrects Lean-Workbook record lean_workbook_plus_53829, 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_53829 (Apache-2.0).

Preamble
import Mathlib.Tactic.NormNum
Formal statement
theorem WorkbookCorrected.plus_53829 : (Nat.factorial 9) / ((Nat.factorial 4) * (Nat.factorial 2)) = 90 := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook; record lean_workbook_plus_53829; Apache-2.0; corrects Open node ae097b3c-b7d6-4608-be06-0f0ce496be04

View graph