Abstract

Arnold Neumaier will give a short talk on “The communication of mathematics”. 
This will be followed by a discussion of the interaction between language and
automation in current proof assistants.   The seminar will actually run from 11 to 12.30.

Abstract for Neumaier's talk:
We discuss – from a mathematician's point of view – the characteristic features that make mathematics communicable between people, between people and software systems, and between software systems with different semantic foundations.

This talk has a strong philosophical component, complementing the views presented during the Big Proofs program so far. It exposes important issues that I believe are essential for bridging the gap between the mathematics community and the formal theorem proving community.

One of the main points made and illustrated is that the natural mathematical language is a highly optimized language for the efficient communication of precise concepts and their relations, whose main features are completely lost in the current generation of formalizations of mathematics.

The insights obtained are the basis of my vision for a joint future of mathematics and formal verification, and provide a background for the design choices discussed in the lecture on Wednesday.