theorem proved term proof

`liouville_thirty`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

1041theorem liouville_thirty : liouville 30 = -1 := by native_decide

Term-mode proof.

1042
1043/-- λ(8) = -1 (8 = 2³, Ω(8) = 3, odd). -/

Lean names referenced from this declaration's body.

liouville in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use