Comment by let_rec

To someone completely outside the field: why is creating a formal verification of an existing proof so hard?

1. Convert the natural language proof steps into formal language

2. Pass it to the solver to verify the steps

Genuinely curious!