Comment by QuesnayJr

There's a couple of problems that were solved that way a while ago, and they have been formalized, but not in Lean:

https://en.wikipedia.org/wiki/Four_color_theorem

https://en.wikipedia.org/wiki/Kepler_conjecture