Number theory

Erdős 828 - lehmer conjecture

When

n > 1

, Lehmer conjectured that

\phi(n) | n - 1

if and only if

n

is prime.

References

erdosproblems.com/828

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ n > 1, n.totient ∣ n - 1 ↔ Prime n

What you must prove

import FormalConjectures.ErdosProblems.«828»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos828.erdos_828.variants.lehmer_conjecture" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/828.lean

Source type SHA-256: sha256:337ac83858d3d220844b1daf2652e936386eba74718044de14dec1b34604137f
Task id: fc-379fc029-variants-lehmer-conjecture-1f04906723-formalized-v1
Task commitment: sha256:c567044c32cbafc1dbefad9ac5e55dc71540be9d8eb4013b1e244f8e91f4deae

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.