Corroborate

Claim in Erdős problems that formal-conjectures marks solved

A published paper or arXiv preprint answers the main question of Erdős Problem #848 (theorem erdos_848 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

Problem as stated at github.com/google-deepmind/formal-conjectures/blob/34ee0e3c5fd52d202d62a71094a37970cb5fb870/FormalConjectures/ErdosProblems/848.lean. The claim text is written by Corroborate; that site has not reviewed or endorsed it.

The problem, as stated in formal-conjectures (Apache 2.0):

Is the maximum size of a set A ⊆ \{1, \dots, N\} such that ab + 1 is never squarefree (for all a, b ∈ A) achieved by taking those n ≡ 7 \pmod{25}? This asks whether `Erdos848 N` holds for all N (formulated using `A ⊆ Finset.range N`). This was solved for all sufficiently large N by Sawhney in this note. In fact, Sawhney proves something slightly stronger, that there exists some constant c>0 such that if \lvert A\rvert \geq (\frac{1}{25}-c)N and N is large then A is contained in either \{ n\equiv 7\pmod{25}\} or \{n\equiv 18\pmod{25}\}.

Verdict: no verdict yet

formal-conjectures marks problem #848 as solved. Those pages say who settled it and how.

Evidence for

None yet.

Evidence against

None yet.