The formalization of existing mathematical proofs is a notoriously difficult process. Despite decades of research on automation and proof assistants, writing formal proofs remains arduous and only accessible to a few experts. While previous studies to automate formalization focused on powerful search algorithms, no attempts were made to take advantage of available informal proofs. In this work, we introduce Draft, Sketch, and Prove (DSP), a method that maps informal proofs to formal proof sketches, and uses the sketches to guide an automated prover by directing its search to easier sub-problems. We investigate two relevant setups where informal proofs are either written by humans or generated by a language model. Our experiments and ablation studies show that large language models are able to produce well-structured formal sketches that follow the same reasoning steps as the informal proofs. Guiding an automated prover with these sketches enhances its performance from 20.9% to 39.3% on a collection of mathematical competition problems.

翻译：摘要：对现有数学证明进行形式化是一个公认的困难过程。尽管在自动化和证明助手方面已有数十年的研究，但编写形式化证明仍然是一项艰巨的任务，且只有少数专家能够完成。以往致力于自动形式化的研究主要关注强大的搜索算法，却未曾尝试利用已有的非形式化证明。在本工作中，我们提出了“草稿、草图与证明”（DSP）方法，该方法将非形式化证明映射为形式化证明草图，并利用这些草图通过将搜索导向更易于解决的子问题来指导自动化证明器。我们研究了两个相关场景：非形式化证明分别由人类编写或由语言模型生成。我们的实验和消融研究表明，大语言模型能够生成结构良好的形式化草图，这些草图遵循与非形式化证明相同的推理步骤。利用这些草图指导自动化证明器，使其在一组数学竞赛问题上的性能从20.9%提升至39.3%。