Fields Mathematical AI Seminar
by Heather Macbeth (Imperial College London)
In the last year, the scale of the computer-formalizations produced by AI has increased dramatically: from math contest problems to long recent research papers. The formalizations now being produced are enormous -- hundreds of thousands of lines of Lean code -- and opaque.
Can such a formalization be trusted as a certificate of correctness for a mathematical statement? I will outline some of the checks one can make, and some of the things that can go wrong.
I will also discuss some stylistic aspects of these large formalizations, and in particular of the fluid dynamics formalizations released last week.
