Sure, but to clarify the article is describing formalization (writing a correct program), not verification (compiling said program). The author is not making the same comparison.

Verification is also open ended (not sure about lean specifically) - you could in theory give just the Navier-Stokes problem definition to an ATP and let it run.