Sadly, probably a crackpot paper. The link to the proof in lean 4 leads to a 404, the user doest exist, and the docker image also doesnt exist.
Also, the paper claims that its been verified by INRIA, Carnegie Mellon University, and the University of Cambridge, using their lean code. How can this be when the code isnt publicly accessible? Did they send it by email instead of fixing their repo? Why would they do that?
I somehow doubt that those three universities confirmed this proof and then sat on it, telling no one that one of the most important questions in CS has been solved.