Formal theorem proving provides executable verification signals from proof assistants, making it a key domain for improving the reliable reasoning ability of large language models through reinforcement learning (RL). However, RL-based prover training is increasingly bottlenecked by the scarcity of high-quality hard tasks: many existing Lean instances are either already solvable by current provers or too uninformative to drive further improvement. We propose ProofFrontier, a proof-structure-guided method for generating statement-preserving boundary-hard training tasks from verified Lean proofs. Instead of synthesizing open-ended problems that may be ill-posed or unverifiable, ProofFrontier starts from existing theorems with Lean-certified proofs, preserving task completeness and formal verifiability. It selectively withholds proof-structural guidance around important local nodes, encouraging the prover to rediscover nontrivial intermediate reasoning while keeping the original theorem statement unchanged. We further introduce capability-aware filtering to retain tasks that are solvable in principle but not easily solved by the base prover, yielding hard yet rewardable RL data. Training with GRPO on ProofFrontier-generated tasks consistently improves DeepSeek-Prover-V2 and Goedel-Prover-V2 on miniF2F, ProofNet, and PutnamBench. Notably, these gains are achieved using only hundreds of synthesized tasks, showing that complete boundary-hard tasks can be more data-efficient than simply scaling weak or already-solved proof data for theorem-proving RL.