> 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 lik

> 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