License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.2
URN: urn:nbn:de:0030-drops-110576
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11057/
Go to the corresponding LIPIcs Volume Portal

Buzzard, Kevin

What Makes a Mathematician Tick? (Invited Talk)

pdf-format:
LIPIcs-ITP-2019-2.pdf (0.2 MB)

Abstract

Formalised mathematics has a serious image problem in mathematics departments. Mathematicians working in "mainstream" areas such as modern algebra, analysis, geometry etc have absolutely no desire to work formally, it slows them down and they cannot see the point. The mathematical community has its own methods for deciding whether a proof (in pdf format) is correct or not; these methods rely on the views of a cabal of experts - our high priests. Our proof of the odd order theorem is "John Thompson got a Fields Medal for the work". This proof is of a rather different nature to the formalised proof of Gonthier et al. Our methods are arcane and mysterious; there is also ample evidence that they are, in general, extremely accurate when it comes to the important stuff.
I will talk about my attempts, as a "mainstream mathematician", to introduce formalised mathematics to my community.

BibTeX - Entry

@InProceedings{buzzard:LIPIcs:2019:11057,
  author =	{Kevin Buzzard},
  title =	{{What Makes a Mathematician Tick\l{} (Invited Talk)}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11057},
  URN =		{urn:nbn:de:0030-drops-110576},
  doi =		{10.4230/LIPIcs.ITP.2019.2},
  annote =	{Keywords: Formalization of mathematics}
}

Keywords: Formalization of mathematics
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI