
research note
ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
The paper addresses a critical bottleneck in neural theorem proving: the excessive length and complexity of formal proofs generated by state-of-the-art reinforcement learning (RL) trained language …










