Number theory · Last catalog review 26 Jul 2026

Erdős Problem 11

Is every odd

n > 1

the sum of a squarefree number and a power of 2?

References

erdosproblems.com/11

Published 18 Jul 2026Never attempted

Formal statement

Lean type

∀ (n : ℕ), Odd n → 1 < n → ∃ k l, Squarefree k ∧ n = k + 2 ^ l

What you must prove

import FormalConjectures.ErdosProblems.«11»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos11.erdos_11" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/11.lean

Source type SHA-256: sha256:7e9596e7603a5b3f536d79ee62512def1ce39a45e429cb460712833ba19ea738
Task id: fc-e923379e-erdos11-erdos-11-7c0303029e-formalized-v1
Task commitment: sha256:1dfef7c5a8c2b30facabfc038bb00518c8a02e818ad6ab38be563261f68374e4

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.