Formal theorem proving with large language models (LLMs) remains a significant challenge due to the inherent complexity of structured reasoning and the scarcity of formal proof data. While recent efforts have focused on addressing the limited availability of formal proof data through techniques such as data augmentation and automatic formalization, these approaches continue to face substantial challenges, leaving the problem of data scarcity unresolved. Therefore, to better leverage existing formal data, we propose FrameProver, a whole-proof generation model that first constructs an intermediate formal framework to guide the generation of complete proofs. To support this, we analyze proof patterns in Lean 4 and design formal framework templates, which are used to generate training data with the help of our tool, REPL4Framework. Based on the Lean-workbook-proofs dataset, we construct a balanced dataset of 21.3k examples, including 10.6k examples with formal frameworks. FrameProver is fine-tuned from DeepSeek-Prover-V1.5-Base on this dataset and achieves 40.2% accuracy (pass@128, from 37.3% without the framework) on the MiniF2F-Test benchmark.