应用介绍
陶哲轩: 所以我开始发表一些演讲，认为既然我组织了这次会议，我们（更多的人）就应该开始关注这个问题了。然后ChatGPT问世了，人工智能突然间无处不在。因此我经常就这个话题接受采访，特别是关于人工智能与存在性形式化证明之间的互动。我说，是的，它们应该结合起来。这将是完美的协同效应。后来我意识到，我必须言出必行，而不仅仅是纸上谈兵。我不从事机器学习，也不从事证明形式化。我不能仅仅依靠权威，说“哦，我是一个著名的数学家，请相信我说的这会改变数学”，而我自己却不亲自参与其中，这种做法是有限度的。所以我我觉得我必须亲自证明其合理性。实际上，我参与的很多事情，在得到建议时，我并没有完全预见到会投入多少时间。只有当我深入某个项目时，我才意识到，到那时，我已经全身心投入了。
