lean_workbook_plus_52628

Proved

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

Let $p$ be a prime number greater than 10. Prove that there exist positive integers $m$ and $n$ such that $m+n < p$ and $5^m 7^n-1$ is divisible by $p$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52628 (p : ℕ) (hp : 10 < p) (hp' : Nat.Prime p) : ∃ m n : ℕ, m + n < p ∧ (5^m * 7^n - 1) % p = 0   :=  by sorry

Source

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

View graph