SMS Spring Meeting : Formalization and Proof Assistants

The formalization of mathematical proofs refers to translating mathematical statements written by humans into a precise, formal language system. This allows computers to verify the correctness of mathematical proofs. However, translating mathematical statements into this language is a complex process that requires a deep understanding of both the underlying mathematics and the respective formal system. Software systems that support this process are known as proof assistants.

In recent years, the field has made remarkable progress – not least because prominent mathematicians such as Terence Tao and Peter Scholze have begun to use proof assistants in their work, thereby attracting the interest of a broader academic community. At the same time, proof assistants themselves have become significantly more powerful and accessible. Meanwhile, AI systems are opening up new possibilities for partially automating the formalization process.

Recently, a team of experts from Switzerland, the United Kingdom, and the United States succeeded in formally verifying Viazovska’s sphere packing theorems using the proof assistant Lean. A novel aspect of this breakthrough is that a significant portion of the formalization work was carried out with the help of artificial intelligence: many steps of the formalization were automatically generated by “Gauss,” a large language model for producing formalized proofs developed by the mathematical AI company Math, Inc.

At the workshop organized by Professor Dr. David Loeffler, experts from the field will report on current developments. UniDistance Suisse is particularly pleased to welcome Fields Medalist Maryna Viazovska among the speakers. The event will take place in conjunction with the spring meeting of the Swiss Mathematical Society.