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.

人工智能在数学领域发现引起了广泛关注，这项研究探索了大型语言模型与定理证明系统的结合，旨在提供一种从研究论文中提取和形式化数学定理的自动化工具。

math-PVS：一种大型语言模型框架，用于将科学论文映射到 PVS 理论

math-PVS: A Large Language Model Framework to Map Scientific  Publications to PVS Theories

Conjectures have historically played an important role in the development of
pure mathematics. We propose a systematic approach to finding abstract patterns
in mathematical data, in order to generate conjectures about mathematical
inequalities, using machine intelligence. We focus on strict inequalities of
type f < g and associate them with a vector space. By geometerising this space,
which we refer to as a conjecture space, we prove that this space is isomorphic
to a Banach manifold. We develop a structural understanding of this conjecture
space by studying linear automorphisms of this manifold and show that this
space admits several free group actions. Based on these insights, we propose an
algorithmic pipeline to generate novel conjectures using geometric gradient
descent, where the metric is informed by the invariances of the conjecture
space. As proof of concept, we give a toy algorithm to generate novel
conjectures about the prime counting function and diameters of Cayley graphs of
non-abelian simple groups. We also report private communications with
colleagues in which some conjectures were proved, and highlight that some
conjectures generated using this procedure are still unproven. Finally, we
propose a pipeline of mathematical discovery in this space and highlight the
importance of domain expertise in this pipeline.

本文提出了一种利用机器智能在数学数据中找到抽象模式生成数学不等式的猜想的系统方法，以 < f<g 类型的严格不等式为重点研究对象，并将它们与一个向量空间相关联，并在这个称为猜想空间的空间中执行几何渐进式下降算法，生成了有关素数计数函数和非阿贝尔简单群的 Cayley 图直径的新猜想，并突显了该空间中数学发现的重要性和领域专业知识的必要性。