Formal verification with interactive theorem provers such as Coq is an effective approach to guarantee software correctness. However, it requires significant human effort to craft theorems and proofs. Large Language Models (LLMs) have shown promise in generating informal proofs in natural language. However, applying LLMs to generate formal proofs remains challenging. In this paper, we conduct a formative study to identify common errors made by LLMs in proof generation. By analyzing 520 errors made by GPT-3.5 when generating Coq proofs, we found GPT-3.5 can effectively outline high-level proof steps but often struggles with low-level details. Based on this insight, we propose PALM, a novel generate-then-repair approach that prompts an LLM to generate an initial proof and leverages targeted symbolic methods to repair the generation errors iteratively. We evaluate PALM on a large dataset with more than 10K theorems. The results show that PALM significantly outperforms existing approaches by successfully proving 76.6% to 180.4% more theorems. Moreover, PALM proves 1270 theorems that none of the other approaches can prove. We also demonstrate the generalizability of PALM across different LLMs.