在 Isabelle/HOL 中形式化 IMO 问题与解答
计算机科学中的逻辑
2020-11-02 v1
摘要
国际数学奥林匹克竞赛（IMO）或许是世界上最负盛名的智力竞赛，因此也是人工智能（AI）面临的最大挑战之一。近期提出的 IMO 大挑战要求构建一个能在比赛中赢得金牌的 AI。我们展示了一些初步步骤，通过在与定理证明器 Isabelle/HOL 中建立经机械检验的 IMO 问题解答的公共仓库，来帮助应对这一目标。该仓库由塞尔维亚贝尔格莱德大学数学系的学生在“交互式定理证明导论”课程中积极维护。
引用
@article{arxiv.2010.16015,
title = {Formalizing IMO Problems and Solutions in Isabelle/HOL},
author = {Filip Marić and Sana Stojanović-{\Dj}urđević},
journal= {arXiv preprint arXiv:2010.16015},
year = {2020}
}
备注
In Proceedings ThEdu'20, arXiv:2010.15832