Proof Artifact Co-training for Theorem Proving with Language Models

Jesse Michael Han, Jason Rute, Yuhuai Wu +2

Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specia…