Combinatorics

Erdős 9

Is the upper density of the set of odd numbers that cannot be expressed as a prime plus two powers of 2 positive?

References

erdosproblems.com/9

No one has attempted this yet.

Formal statement

Lean type

True ↔ 0 < Erdos9.Erdos9A.upperDensity

What you must prove

import FormalConjectures.ErdosProblems.«9»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos9.erdos_9" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/9.lean

Source type SHA-256: sha256:92d78723b8eaef03950c32aabe1192376ff7d54c84570decbade87285ac69f6e
Task id: fc-379fc029-erdos9-erdos-9-782039329c-formalized-v1
Task commitment: sha256:f7b23bc705fcbc252edf26d1aee54c0f71064a02579be5612175dcf0cb7e1303

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.