Peano Player: Interactive Theorem Proving as a Constrained MDP

Reinforcement learning with verifiable rewards is frequently used for neural theorem proving and typically trains on a single binary signal indicating whether a complete generated proof verifies. However, proof assistants are interactive systems: after each tactic, they return an updated proof state and report whether the tactic failed. Prior methods that use tactic-failure signals treat failure as a minor penalty and allow generation to continue after a tactic fails. We introduce Peano Player, a tactic-level theorem prover formulated as a constrained Markov decision process, where the agent observes the verifier-produced proof state, receives reward for closing proofs, and incurs a terminal cost of equal magnitude for failing a tactic. We evaluate in a controlled equational-theory environment over the Peano numbers that generates unlimited provable theorems at controlled difficulty. An ablation over proof-state observation and tactic-failure cost shows that each improves solve rate independently, and their combination more than quadruples overall solve rate relative to the strongest baseline, with a tenfold difference at the greatest difficulty level. These results suggest that theorem-proving agents would benefit from learning from errors during interaction---not only from whether a completed proof verifies---because any tactic-level proof assistant exposes the same per-step signals.