Abstract:
Mathematics is currently mostly done by humans, and the published literature is mostly correct. Is this good enough? ArXiv enables mathematicians to distribute their unrefereed research around the world very effectively, and citations of ArXiv papers in other ArXiv papers is certainly acceptable in our culture. But we cannot be 100% sure that the latest paper in the p-adic Langlands Philosophy is correct. Such a paper will surely have no practical real-world application, so if it is also not correct, then one might argue that it is worthless. Computer proof checkers offer a completely different way of doing mathematics, which has no problems with accuracy but instead has a completely different set of problems. Computers can beat humans at chess and at go. Will computers one day be able to beat humans at theorem proving? Should we be teaching math undergraduates to use computer proof checkers? I am a number theorist by training, but have spent the last two years learning about computer proof checkers; I will give an overview of the area. No background in computer proof checkers or the p-adic Langlands philosophy will be assumed. The talk will be suitable for undergraduates.
Frick Fine Arts Building - Auditorium