That would also require re-doing all of mathematics in a constructive setting, which is a great idea as far as constructivists are concerned but it has both pol

That would also require re-doing all of mathematics in a constructive setting, which is a great idea as far as constructivists are concerned but it has both political and technical opposition. It's also the case that a proof in Coq doesn't have to be enlightening, especially if you discharge it with some inscrutable hammer-like custom-written pile of LTAC.