Four Color Theorem

Stream: general

[Jason Rute]

I wonder what it would take to formalize this (or to find the error). https://mobile.twitter.com/VinceVatter/status/1605528265288028160

The long-awaited enumerative proof of the four color theorem, by David Jackson and Bruce Richmond, is here! Jackson announced this proof in May and it made big news, but then there were apparently some issues that needed to be fixed. Now on arXiv! https://arxiv.org/abs/2212.09835

- Vince Vatter (@VinceVatter)

[Jason Rute]

HN: https://news.ycombinator.com/item?id=34082022

[Jason Rute]

Reddit: https://www.reddit.com/r/math/comments/zruc58/221209835_a_nonconstructive_proof_of_the_four/

[Anatole Dedecker]

New speedrun category: formalize a proof of the Four Color Theorem, any%

[Jason Rute]

Mastodon: https://mathstodon.xyz/@tao/109554420101377184 I think the skepticism is increasing on this “proof”.

[Yaël Dillies]

Formalising this was actually discussed on Xena yesterday!

[Yaël Dillies]

Current conclusion is that we have enough people understanding the combinatorics but not enough people understanding the complex analysis.

[Martin Dvořák]

I had no idea that this proof exists! However, the old proof was successfully formalized in Coq.
https://www.ams.org/notices/200811/tx081101382p.pdf

[Yaël Dillies]

Yes, which is why we're talking about speedrunning :smile:

[Patrick Massot]

Frankly, the comments on internet suggest there is nothing to formalize here.

[Martin Dvořák]

What do you mean?

[Yaël Dillies]

The community hasn't yet reached a consensus that the proof is correct. And it might reach the opposite consensus instead.

[Yaël Dillies]

However, some of the prerequisites (Tutte and chromatic polynomials) for the proof are in sight for my LeanCamCombi project, so I might tick them off in case the proof becomes formalisable in the future.