feat(ErdosProblems): 848

[The-Obstacle-Is-The-Way]

Closes #1920

fixes #974

Adds formalization of Erdős Problem 848 (Sawhney-Sellke 2025).

A complete Lean 4 proof (3887 lines, 0 sorries) is linked in the @[category research formally solved using lean4 at ...] attribute.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[felixpernegger]

The erdos problem asks if thus holds for all numbers, not just almost all.
What is the value of N0? that would be interesting.

[felixpernegger]

I didnt look at your proof in great detail, but I noticed it uses native_decide multiple times, which should heavily be avoided.

[felixpernegger]

There are also comments on your comment on the website, whuch need to be adressed first.

[The-Obstacle-Is-The-Way]

@felixpernegger Thank you for your feedback, I will do my best to address all issues as recommended.