I'm not sure if this is real, but the abstract says machine-verified.
Lean uses Curry-Howard correspondence, so how proofs work is you declare your propositions as types and then your proof is actually a recipe that goes from things that have already been established and finishes by instantiating that type. The guarantees there are very strong - if you succeed in instantiating the type you have definitely proved something. The question is whether you have proved the thing you said you have. So here scanning the proof (it’s like 100 pages and I am sick so definitely sub-par intellectually) they use category theory to embed the problem, so the proof is actually a proof of the properties of this embedding. So if there is a problem with the proof, my guess would be that it would lie in the embedding not being exactly representative of the problem somehow.
It seems a pretty serious attempt though- it’s not just some random crank paper.
I'm betting it was published in a hurry. I know I would hit "publish" within 24 hours of creating such a result, and would hope it would go wide. I'd publish to arxiv before getting clearance to release the code. I bet that's what happened here.
I appreciate your explanation of the Curry-Howard correspondance. I was familiar with it, but not with Lean in particular. I'd heard of Lean, but didn't know how it worked.
Thank you again!
I don't know homological algebra at all and only the very basics of category theory and while the (107-page) proof gives a lot of background it would take more time for me to get myself up to speed than I can really afford to spend right now. But that's the gist.
The fact that they have formalized the proof should mean it will be quicker to verify whether or not this is indeed it.
[1] which they call "contractible computational complexes (Hn(L) = 0 for all n > 0)."
[2] which they call "non-trivial homology (H1(SAT)̸ = 0)"