Number theory
Erdős 409 - sigma termination
If then the iteration necessarily reaches a prime. Note: this is open — it is not clear that the σ iteration always terminates, since it is non-decreasing (unlike the φ iteration which is strictly decreasing).References
No one has attempted this yet.
Formal statement
Lean type
∀ n > 1, ∃ i, Nat.Prime ((fun x => (ArithmeticFunction.sigma 1) x - 1)^[i] n)What you must prove
import FormalConjectures.ErdosProblems.«409»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos409.erdos_409.variants.sigma_termination" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/409.lean
- Source type SHA-256
- sha256:0da24d0288f63e0441d5ba4817f97745a5905d3ac84e18f32cfcb62b3abf9686
- Task id
- fc-379fc029-variants-sigma-termination-040cf9cc8d-formalized-v1
- Task commitment
- sha256:a57cdb8ae854d8003f109e747ef97ec34e7b421166d855d202f96461bc9fea00
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.