NOW PROVING
—
Select a problem and press Run.
0%COMPLETE
∫
Idle
press Run to start
Progress
AI SUMMARYThe proof is a little past halfway. It has rewritten the target into a fully factored form and cleared the first divisibility obligation with a short parity-and-remainder argument.
Attention has moved to the remaining prime factor. Once that piece is in place, a coprimality argument will combine everything into the full claim that 30 divides n⁵ − n.
This overview is regenerated every few steps — the fine-grained work is condensed into the summary above.
Proof state
NOT STARTED- Rewrite the goal in factored form: n⁵ − n = n(n−1)(n+1)(n²+1).
- Among any three consecutive integers n−1, n, n+1, one is even and one is a multiple of 3, so 6 ∣ n(n−1)(n+1).
- In progress — one of the factors is always a multiple of 5, so 5 divides the whole product.
- Since 6 and 5 are coprime, their product 30 ∣ n(n−1)(n+1)(n²+1) = n⁵ − n.∎
import Mathlib set_option maxHeartbeats 0 -- Factorization of n⁵ − n lemma n5_sub_n_factored (n : ℤ) : n ^ 5 - n = n * (n-1) * (n+1) * (n^2+1) := by ring -- 6 ∣ product of three consecutive integers lemma six_dvd_n_pred_succ (n : ℤ) : (6 : ℤ) ∣ n * (n-1) * (n+1) := by have h2 := by rcases Int.even_or_odd n … have h3 := by have : n % 3 = 0 ∨ _ := by omega … exact IsCoprime.mul_dvd ⟨-1,1,by norm_num⟩ h2 h3 -- 5 ∣ full product ← proving nowlemma five_dvd_prod (n : ℤ) : (5 : ℤ) ∣ n*(n-1)*(n+1)*(n^2+1) := by sorry theorem main (n : ℤ) : (30 : ℤ) ∣ n ^ 5 - n := by have h := n5_sub_n_factored n have h6 := six_dvd_n_pred_succ n sorry