Isabelle/HOL 中无穷级数的无理性与超越性判据
计算机科学中的逻辑
2022-10-14 v2 逻辑
摘要
我们概述了在证明助手 Isabelle/HOL 中对来自三篇不同研究论文的某些无穷级数无理性与超越性判据的形式化：分别由 Erdős 与 Straus（1974）、Hančl（2002）以及 Hančl 与 Rucki（2005）提出。我们在 Isabelle/HOL 中的形式化可在形式证明档案（Archive of Formal Proofs）中找到。在此我们描述了形式化的若干选定方面，并讨论了这揭示了 Isabelle/HOL 在形式化现代数学研究（尤其是数论与分析的这些部分）中的使用与潜力。
引用
@article{arxiv.2101.05257,
title = {Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL},
author = {Angeliki Koutsoukou-Argyraki and Wenda Li and Lawrence C. Paulson},
journal= {arXiv preprint arXiv:2101.05257},
year = {2022}
}
备注
23 pages. Submitted for publication