The hypothesis class that the ML algorithm works within is proofs, checkable by something like Coq, so that can't actually be done.