What Makes a Mathematician Tick? (Invited Talk)

Author Kevin Buzzard

Thumbnail PDF


  • Filesize: 154 kB
  • 1 pages

Document Identifiers

Author Details

Kevin Buzzard
  • Imperial College, London, U.K.

Cite AsGet BibTex

Kevin Buzzard. What Makes a Mathematician Tick? (Invited Talk). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


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.

Subject Classification

ACM Subject Classification
  • Mathematics of computing
  • Formalization of mathematics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail