Once upon a time, people published solo often. It's just harder to do things like that these days.

Thank you! This is the kind of comment I hoped to see.

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!

Natural proofs are a certain type of proof of the circuit complexity of boolean conditions. The barrier is that it has been proved that [1] natural proofs cannot be used for P vs NP.

I’m not sure that is a problem here given that as I understand it, natural proofs apply to circuit complexity approaches and they say the whole circuit complexity method has fundamental limitations which they describe thus:

   The circuit complexity approach seeks to establish lower bounds by proving that NP problems require super-polynomial circuit sizes. While achieving success for restricted models such as monotone circuits, this approach has faced insurmountable barriers in establishing non-linear lower bounds for general circuits.

So they take an entirely different approach using category theory. It may have a similar limitation as the natural proof barrier (as far as I know), but as they dismiss the whole circuit idea and do something different I wouldn’t say them not mentioning the limitation of a specific type of circuit-based approach is that much of a problem.

[1] assuming certain things which people generally believe to be true