论文标题
在Isabelle/HOL中正式化IMO问题和解决方案
Formalizing IMO Problems and Solutions in Isabelle/HOL
论文作者
论文摘要
国际数学奥林匹克运动会（IMO）也许是世界上最著名的心理竞争，因此是人工智能（AI）最大的巨大挑战之一。最近制定的IMO Grand Challenge需要建立一个可以在比赛中赢得金牌的AI。我们提出了一些初始步骤，可以通过在Interactive Theorem Prover Isabelle/HOL中创建一个机械检查的IMO问题解决方案的公共存储库来帮助解决这一目标。该存储库是由贝尔格莱德大学塞尔维亚大学数学学院的学生积极维护的。
The International Mathematical Olympiad (IMO) is perhaps the most celebrated mental competition in the world and as such is among the greatest grand challenges for Artificial Intelligence (AI). The IMO Grand Challenge, recently formulated, requires to build an AI that can win a gold medal in the competition. We present some initial steps that could help to tackle this goal by creating a public repository of mechanically checked solutions of IMO Problems in the interactive theorem prover Isabelle/HOL. This repository is actively maintained by students of the Faculty of Mathematics, University of Belgrade, Serbia within the course "Introduction to Interactive Theorem Proving".
