The manual part is writing out steps of the proof. Some times these steps can be automated. Usually they are guided by a user. They are typically not written ou

The manual part is writing out steps of the proof. Some times these steps can be automated. Usually they are guided by a user. They are typically not written out step by step by hand because it is very tedious. I doubt complicated ideas expressed in advanced mathematical papers can be easily or succinctly expressed formally. http://en.wikipedia.org/wiki/Theorem_prover http://en.wikipedia.org/wiki/Theorem_prover http://www.cs.ru.nl/~freek/100/ http://www.cs.ru.nl/~freek/100/ But more importantly, the objective of a mathematical paper is to get readers to understand the proof, a goal which is poorly achieved with formal verification.