ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations - Gu, Alex; Piotrowski, Bartosz; Gloeckle, Fabian; Yang, Kaiyu; Markosyan, Aram (International Conference on Learning Representations, 2026)