Number theory
Erdős 249
Is irrational? Here is the Euler totient function.References
No one has attempted this yet.
Formal statement
Lean type
True ↔ Irrational (∑' (n : ℕ), ↑n.totient / 2 ^ n)What you must prove
import FormalConjectures.ErdosProblems.«249»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos249.erdos_249" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/249.lean
- Source type SHA-256
- sha256:50958c75eb82dfa63690899d9c7a87adaf9c4c6dc67de73e9782172842b2fe4d
- Task id
- fc-379fc029-erdos249-erdos-249-db6e2417ae-formalized-v1
- Task commitment
- sha256:a806efd018a3ba0535a1c9f79519a3a617bb9bf480bfebceb69d3e0c424756bf
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.