isaacfrond

It is nor far-fetched to suppose else is a translated German word because that is exactly what happened. The only question is which German word was is it.

Right. To be clear: the halting problem is not in the class NP. Any problem in NP can trivially be reduced to the halting problem and so the latter is NP-hard.

Which is exactly why you want a Lean proof in the first place!

NL proofs rely on not-entirely-correct prior art, and contain countless holes both big and small. When formalizing human NL proofs it is probably very normal that the Lean proofs doesn't quite follow the NL proof.

I'd say it's totally immaterial how it was written

> Surely researchers like this have the processing power to run them at home,

Nobody has that power. Certainly not mathematicians.

The paper does not resolve P versus NP, but it does make an important advance in a closely related area. To prove that P ≠ NP, it would be enough to show that every algorithm for an NP-complete problem requires superpolynomial time. We cannot prove anything remotely that strong. For explicit NP-complete problems in unrestricted computational models, we cannot even prove superlinear lower bounds. There is therefore an enormous gap between the lower bounds we can prove and the superpolynomial bounds we would need.

VP and VNP are closely related algebraic analogues of P and NP. Here the paper proves new lower bounds for computing the permanent, a VNP-complete polynomial, in particular models of arithmetic computation: roughly (n^2\log\log n) arithmetic gates for unrestricted division-free circuits, and (n^4/\log n) size for the more restrictive formula model. These are still polynomial bounds, so they do not separate VP from VNP. But lower bounds on the resources needed to compute explicit functions are exactly what would ultimately be required for such a separation, and meaningful lower bounds of this kind are exceptionally rare.