You are most welcome. Reading it a little more, the summary of the proof is they embed computations as a particular sort of category and then use homological algebra to show that computations in P have a certain property[1] and computations in NP have a different property[2], and they say they go on to demonstrate these properties are mutually incompatible, thus proving P != NP.
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)"
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)"