在 Isabelle 中形式化新数学：对角 Ramsey 数
计算机科学中的逻辑
2025-01-22 v1 组合数学
摘要
数学的形式化开始变得标准化，但该技术对数学家的价值仍需进一步展示。目前仅有少数示例表明如何使用证明助手来验证全新的工作。本文报告了关于 Ramsey 数的主要新结果（arXiv:2303.09521）的形式化，该结果于 2023 年被宣布。一个意外发现是需要大量的计算机代数技术。
引用
@article{arxiv.2501.10852,
title = {Formalising New Mathematics in Isabelle: Diagonal Ramsey},
author = {Lawrence C Paulson},
journal= {arXiv preprint arXiv:2501.10852},
year = {2025}
}
备注
22 pages, 2 figures