Mardi

新方法将非正式数学陈述与形式化库对齐

研究人员开发了一种方法，可以将非正式的数学陈述与其在 Lean 的 mathlib 等库中的形式化对应项进行对齐。这项工作构建了一个数据集，将 Stacks Project 中的非正式陈述与 mathlib 中的形式化内容联系起来，并利用了专家注释。该研究评估了检索、基于 LLM 的重新排序以及 LLM 辅助验证，以发现新的非正式到形式化的链接，并将这些发现整合到 MaRDI 知识图中，以增强对形式化数学知识的可访问性。