We may get as little mathematical insight from an actual formal proof as from an actual Turing-machine computation; rather, mathematical insight comes from understanding a mathematical argument or a computational algorithm at a much higher level of abstraction.
