lean_workbook_plus_67995

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that there are infinitely many composite numbers $n$ for which \n

n | 3^{n-1} - 2^{n-1}

I would be very grateful if you could explain your solution, I think that I should use Fermat's Little theorem for proof but I am not sure how should I use it.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67995 : ∃ n, Nat.Prime n ∧ n ∣ 3 ^ (n - 1) - 2 ^ (n - 1)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph