Prove2Me

Factorial arithmetic identity #77227

Disproved
WorkbookCorrected.plus_77227

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

arithmeticcorrectedelementaryworkbook

The elementary natural-number / rational identity

(6!)/(2!∗2!)=90(6!)/(2!*2!) = 90

holds by direct arithmetic evaluation.

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

Preamble
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic.NormNum
Formal statement
theorem WorkbookCorrected.plus_77227 : (Nat.factorial 6)/((Nat.factorial 2)*(Nat.factorial 2)) = 90 := by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook; record lean_workbook_plus_77227; Apache-2.0; corrects Open node 927c9b63-9619-4286-ae1a-e7afd755e336

View graph