> The tools are ready, it is just that doing the hard work going from a handwritten one to a computer-readable proof is not sufficiently appreciated.

Seems like a perfect task for an LLM trained on English and Idris/Coq/etc