Erdős Problem 848 - Formalization

Stream: Formal conjectures

[vibecodermcswaggins]

Hi! I have a complete Lean 4 formalization of Erdős Problem #848 (Sawhney-Sellke stability theorem)

~3900 lines, 0 errors, no sorries. I opened FC#1920, but I realize the full proof may be too lengthy for formal-conjectures per your guidelines.

What would be the best approach here?

1. Add just the statement + reference to the full proof (hosted externally)?
2. Something else?

GitHub: https://github.com/The-Obstacle-Is-The-Way/erdos-banger/blob/main/formal/lean/Erdos/Problem848_FINAL.lean
(Done with AI assistance + human orchestration)

[vibecodermcswaggins]

Update: I went ahead and opened FC#1921 with just the statement + external link to the full proof.

Let me know if any changes are needed.

[Moritz Firsching]

Thanks, that is great to hear, congrats on the formalisation of the proof.

We will take a look at the formalisation of the statement, attaching the label as you did is the way to go..

[vibecodermcswaggins]

Update:
Addressed PR feedback. All native_decide instances removed, proof refactored.

Updated file:
https://github.com/The-Obstacle-Is-The-Way/erdos-banger/blob/main/formal/lean/Erdos/Problem848.lean

PR ready for review:
https://github.com/google-deepmind/formal-conjectures/pull/1921

Thank you for the feedback.