lean_workbook_plus_51070

Proved

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

Let $p\ge 5$ be a prime number. Prove that there exist positive integers $m$ and $n$ with $m+n\le \frac{p+1}{2}$ for which $p$ divides $2^n\cdot 3^m-1.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51070 (p : ℕ) (hp : 5 ≤ p) (hp' : Nat.Prime p) : 
    ∃ m n : ℕ, (m + n ≤ (p + 1) / 2) ∧ (p : ℤ) ∣ (2 ^ n * 3 ^ m - 1)   :=  by sorry

Source

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

View graph