* 概述
ucla的ipam在今年二月份组织了一场同名研讨会,二十余名来自不同领域的专家做了报告,绝大部分都有录像.主要集中在两个领域:

** 辅助证明(proof assistants)
把数学定理过程用代码写出来,然后交给程序来验证有无缺陷.
目前比较主流的语言有Coq, Isabelle, Lean等.

** 自动证明(automated theorem proving)
程序自动判断命题的正确性,甚至给出推理过程.
我国的吴文俊先生做了很多平面几何定理的相关工作.

* 网址
- 官方: https://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/
- 油管: https://www.youtube.com/playlist?list=PLHyI3Fbmv0Sc5XovavCUqSfq-6K9WfBoT

* 感想
根据个人观察,参会的数学家们对于时下的热门技术(大语言模型,深度强化学习等)是一种很开放和好奇的态度,希望它们能对自己的研究有所帮助,而不担心自己的工作会被取代.
--
FROM 59.36.211.201