ICM大会报告——The rise of formalism in mathematics
报告人：Kevin Buzzard (Imperial College London)
时间：2022-07-09 16:15-17:15
地点：Room 1560, Sciences Building No. 1
Lecture on proof formalisation for ordinary mathematicians
Abstract: Formalism is the art of writing down what you actually mean. Mathematics has a rich history of formalisation: Euclid, Russell–Whitehead and Bourbaki all tried it. This century Avigad, Hales and Gonthier have shown us that there is another way. Now a new generation of young people are formalising algebra, analysis, category theory, combinatorics, geometry, number theory, topology and more at Masters level and beyond, this time using a computer. Lean’s mathematics library mathlib contains nearly a million lines of free and open source code corresponding to proofs of over 80,000 theorems such as the fundamental theorem of Galois theory, and it is growing fast. AIs trained on the library have solved IMO problems by themselves. What is happening? This is not about making sure the papers are right. This is not about making a computer program which will print out a one billion line proof of the Birch and Swinnerton-Dyer conjecture using only the axioms of mathematics. This is not about extracting the beauty from a proof and leaving only the directed acyclic graph. This is about developing computer tools which have the potential to help researchers and PhD students in new ways. Much remains to be done. I will give an overview of the area.
