[本文来自 Francesco Maggi 的客座文章。该博客文章最初以不同的文件格式撰写，并使用 AI 进行了转换。— T.] 大型语言模型（LLMs）以及围绕其构建的研究系统（通常被称为“人工智能”）在生成数学证明方面已展现出非凡的能力。尽管其质量与局限……