As artificial intelligence (AI) gains greater adoption in a wide variety of applications, it has immense potential to contribute to mathematical discovery, by guiding conjecture generation, constructing counterexamples, assisting in formalizing mathematics, and discovering connections between different mathematical areas, to name a few. While prior work has leveraged computers for exhaustive mathematical proof search, recent efforts based on large language models (LLMs) aspire to position computing platforms as co-contributors in the mathematical research process. Despite their current limitations in logic and mathematical tasks, there is growing interest in melding theorem proving systems with foundation models. This work investigates the applicability of LLMs in formalizing advanced mathematical concepts and proposes a framework that can critically review and check mathematical reasoning in research papers. Given the noted reasoning shortcomings of LLMs, our approach synergizes the capabilities of proof assistants, specifically PVS, with LLMs, enabling a bridge between textual descriptions in academic papers and formal specifications in PVS. By harnessing the PVS environment, coupled with data ingestion and conversion mechanisms, we envision an automated process, called \emph{math-PVS}, to extract and formalize mathematical theorems from research papers, offering an innovative tool for academic review and discovery.

翻译：随着人工智能在各类应用中的广泛采用，它在数学发现方面展现出巨大潜力，例如指导猜想生成、构造反例、协助数学形式化以及发现不同数学领域之间的联系等。虽然先前的工作已利用计算机进行穷举式数学证明搜索，但近期基于大语言模型的研究致力于将计算平台定位为数学研究过程中的共同贡献者。尽管当前大语言模型在逻辑和数学任务方面存在局限性，但将定理证明系统与基础模型相结合的兴趣日益增长。本研究探讨了大语言模型在形式化高级数学概念中的适用性，并提出一个能够批判性审查和检验研究论文中数学推理的框架。鉴于大语言模型在推理方面的已知缺陷，我们的方法协同利用证明助手（特别是PVS）与大语言模型的能力，在学术论文中的文本描述与PVS中的形式化规范之间建立桥梁。通过借助PVS环境，结合数据摄取与转换机制，我们设想了一个名为\emph{math-PVS}的自动化流程，用于从研究论文中提取和形式化数学定理，为学术评审与发现提供创新工具。