描述了 mathlib，这是一个社区推动的工作，旨在构建在 Lean 证明助理中正式化的统一数学库。它在依赖类型基础、集中于经典数学、结构的广泛层次结构、大规模和小规模自动化以及分散的组织方面与其他证明助理库有所不同。

Oct, 2019

MathGloss 项目旨在使用现有的现代自然语言处理（NLP）工具和网络资源，自动创建一个用于本科数学的知识图谱（KG）。MathGloss 是一个链接数据库，已整合五个资源，目标是为数学学习资源进行整合，并允许每个数学家根据自己的偏好进行学习。此外，将不同的本科数学学习资源与学习正式数学的资源组织在一起，希望能够促进数学家和正式工具专家（定理证明器、计算代数系统等）之间的相互理解，并消除一些形式数学方面的障碍。

Nov, 2023

该研究利用生成式人工智能、数学代理、数学嵌入等方法解决信息系统生物学领域的老化问题，并应用多尺度物理数学和基因组数据来分析疾病模型和基因组数据，以探索未解决的阿尔茨海默病问题。

Jul, 2023

数学推理是评估人类智能基本认知能力的基石。该研究调查了大型语言模型在解决数学问题方面的真正进展、障碍、数学问题类型和相关数据集、解决数学问题的 LLM 技术范围、影响 LLMs 解决数学问题的因素和问题，并提供了这一快速发展领域中的现状、成就和未来挑战的整体观点。

Jan, 2024

该研究追踪了近年来非正式数学语言处理方法在五个战略子领域中的发展情况，重点突出了卓越的方法论要素以及现有的限制。

May, 2022

本论文提出一种数学知识图谱（Math-KG），通过自然语言处理技术利用百度百科和维基百科构建，旨在解决在线教育平台上的信息过载和知识跟踪问题，并提供了一个简单的应用系统进行实验验证。

May, 2022

本文对非洲地区机器学习研究的最新进展和相关应用进行了大量文献调查和关键的计量分析，以获取 2761 份机器学习相关文献，并通过科学引文索引扩展检索出发表于 903 种期刊的 482 项引用至少的文章。结果显示出当前机器学习研究的现状和未来趋势，并促进在非洲各地的不同研究机构之间的共同研究和知识交流。

Apr, 2023

本文探讨了在 STEM 类学术文献检索中，应用机器学习的一些挑战，以及目前普遍使用的文本 embedding 技术对于数学文档的不足，同时研究出一些让计算机更好地理解和学习数学的方面。

May, 2019

本文介绍了一个形式化的模型，用于在开放链接数据云中表示自然语言的数学事实，该模型用于 OntoMath PRO 专业数学本体论的开发，OntoMath 数字生态系统的语义出版平台是一个中心组件，用于数学知识管理，包括数学公式的语义搜索和数学论文的推荐系统。

Mar, 2023

为 mathlib4 设计了一个语义搜索引擎，可以接收非正式查询并找到相应的定理，同时还建立了一个用于评估各个搜索引擎性能的基准。

Mar, 2024