A dataset and RL-zero pipeline for advanced mathematical reasoning of informal theorem proving.