I'm a little surprised the article stresses Lean programs so much, without ever stating what that is or why it somehow proves something. Maybe that's expected knowledge for this sort of thing.
It is because people take lean proofs at face value and you don't have to actually explain it. I have some math problems I am working on and while I had code showing it does the right stuff, the prose was taking a lot longer, but now I realize I can just mass convert it to lean and put it out there.