Conjectures.io

Number theory

Erdős 1072 - part i

Is it true that there are infinitely many pp for which f(p)=p−1f(p) = p − 1?

References

No one has attempted this yet.

Formal statement

Lean type

True ↔ {p | Nat.Prime p ∧ Erdos1072.f p = p - 1}.Infinite

What you must prove

import FormalConjectures.ErdosProblems.«1072»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1072.erdos_1072.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1072.lean

Source type SHA-256
sha256:549d7f97f1b8311cb01cca64fe7235468408a4881e9d8f78eac594e03262c3a0
Task id
fc-379fc029-parts-i-9ee6e9f9a8-formalized-v1
Task commitment
sha256:61368ef472d478945cad7d32cf5643dad8132500b52da09d00748608c4b6a416

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.