This question seems to always come up on Hacker News - figuring out how to even formulate the statement of theorems in theorem provers such as Lean is a massive

This question seems to always come up on Hacker News - figuring out how to even formulate the statement of theorems in theorem provers such as Lean is a massive research undertaking in itself, requiring much creativity and novel work. Let alone figuring out how to formulate the proofs. I’d recommend you have a look at some of the talks that Buzzard has given on this to understand the complications (both technical and social) and progress that has been made so far.