Number theory
Erdős 1003
Are there infinitely many solutions to , where is the Euler totient function?References
No one has attempted this yet.
Formal statement
Lean type
True ↔ {n | n.totient = (n + 1).totient}.InfiniteWhat you must prove
import FormalConjectures.ErdosProblems.«1003»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos1003.erdos_1003" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/1003.lean
- Source type SHA-256
- sha256:5902565df865cd02e0fe1594a872f85f4cd73fa838872192fb91d562fadd53f7
- Task id
- fc-379fc029-erdos1003-erdos-1003-0b7cccd2cc-formalized-v1
- Task commitment
- sha256:8c7a6a70a5546c68fd606b9ba59940a5340302ac0f0cebbf268f8e44bb32ca40
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.