Although large language models (LLMs) provide a new exploration path in the field of automated algorithmic theorem proving, existing methods fail to sufficiently improve the capability of automated theorem provers in proving intermediate propositions. Currently, labeled data for formal theorem proving in linear data structure algorithms is very scarce, which presents significant challenges when large language models are used for prediction. To address this issue, this study proposes a novel lemma-library-driven proof method, LDPM, for automated theorem proving of linear data structure algorithms, which integrates large language models with formalization techniques. The method constructs a lemma library composed of newly proven lemmas. By retrieving relevant lemmas from this library, the capability of the automated theorem prover in proving intermediate propositions can be effectively enhanced. The construction of the lemma library follows a three-stage progressive strategy. First, a joint request mechanism is adopted to generate multiple candidate lemma statements, thus enriching the library resources. Second, an iterative proof strategy is employed to prove the candidate lemmas one by one, gradually improving the reliability of the lemma library. Finally, a lemma reflection mechanism is introduced, leveraging LLMs to revise and optimize lemmas, achieving the dynamic expansion and continuous refinement of the lemma library. Through this method, the performance of theorem proving for linear data structure algorithms is significantly improved. Compared with the state-of-the-art methods, the success rate of theorem proving is increased from 44.00% to 82.00%. Ablation experiments further show that the lemma library plays a key role in improving the capability of automated theorem provers in proving intermediate propositions, increasing the success rate of theorem proving for linear data structure algorithms by 38.00%.