PVSGym: A Proof Learning Environment

We introduce \pvsgym{}, a reinforcement learning (RL) gym environment tailored for the PVS (Prototype Verification System) theorem prover. \pvsgym{} includes an ML-friendly dataset of expert-level PVS formalizations drawn from the \nasalib{} library which span a number of mathematical and computational domains. Our aim is to catalyze research at the intersection of AI and formal methods, ultimately advancing proof automation and mathematical discovery. Both the environment and dataset will be publicly available.