ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations

Alex Gu, Bartosz Piotrowski, Fabian Gloeckle +2

Neural theorem proving has advanced rapidly in the past year, reaching IMO gold-medalist capabilities and producing formal proofs that span thousands of lines. Although such proofs…