Conjectures.io

Number theory

Erdős 456 - part iii

Are there infinitely many primes pp such that p−1p-1 is the only nn for which mn=pm_n=p?

References

  • [Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73--82.

No one has attempted this yet.

Formal statement

Lean type

True ↔ {q | Nat.Prime q ∧ ∀ (n : ℕ), Erdos456.m n = q ↔ n = q - 1}.Infinite

What you must prove

import FormalConjectures.ErdosProblems.«456»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos456.erdos_456.parts.iii" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/456.lean

Source type SHA-256
sha256:8ceaf9e76ee4bcdc74fdb1532edaca6f235386adaeeadd88e0407a41a4107a18
Task id
fc-379fc029-parts-iii-db20e22e31-formalized-v1
Task commitment
sha256:e2461c557b1214ea2c8d5d9a3479afba21b2b0bec0082f5681258f948107f067

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.