Comment by momentoftop

Converting natural language steps to a formal language isn't too challenging. But basically none of those steps will follow directly from the previous steps by any primitive deduction rule of any formal system. From the perspective of formal logic, there are massive gaps in the reasoning, and these need to be filled to pass the verifier. And they are absolutely massive, so massive that it would be completely intractable to fill them in manually.

That's where most of the tech in a theorem prover exists: its tooling to automatically fill in the gaps so your proof can pass the verifier. The tools and automation here are genuinely great, but you still end up having to write way more steps and inferences than you'd see in any maths textbook, and the details are far more fiddly because the formal verification is not very forgiving.

As an illustration, consider how you get from:

  X = (x + y)(z + w)

to

  X = xz + xw + yz + yw

The second equation doesn't follow directly from the first in any logical system. Instead, it follows by the distributive law, commutativity and associativity of addition, commutativity of multiplication, symmetry and transitivity of equality, and you'll need to have some means to specialise these universal statements and reason about term substitution.

A modern prover will do simple algebra like this for you, but the tooling had to be built to do it. In other domains, the tooling just dies trying to connect what an average working mathematician or even a mathematics undergraduate would consider obvious, and you're stuck either having to elaborate massive tedium, manually guiding the automation, or having to write new bespoke tooling to fill the gaps.