Computers have changed the way that mathematics is done. The ability to do complicated calculations quickly has enabled humans to numerically solve differential equations, to check conjectures in number theory in billions of cases, and many many other examples. In applied mathematics in particular, the computer has revolutionised the subject. But there are some areas of pure mathematics where computers are essentially completely unused. People studying theoretical questions about infinite-dimensional objects might find that traditional uses of computers are of no help to them -- they are trying to prove theorems, not compute examples.
Computer proof verification software offers a new way of using computers, which might be more useful to mathematicians looking for proofs. I will demonstrate some of this software (the Lean theorem prover, being developed by Microsoft Research), talk about why most mathematicians don't use it, and speculate about whether this will change in the future. No advanced pure mathematics background will be necessary.
Registre-se com antecedência para este seminário: https://ide-fgv-br.zoom.us/j/99603042015?pwd=UFhqSVdISFIzbVFPMzZCMnRIY043Zz09
Após o registro, você receberá um e-mail de confirmação contendo informações sobre conexão no seminário.
*Texto informado pelo autor.
Kevin Buzzard is a professor of pure mathematics at Imperial College London. He was a PhD student of Richard Taylor and his traditional mathematical work is in algebraic number theory. More recently he has become interested in teaching modern mathematical proofs to computers.