Language and automation in mathematics

Add to your list(s) Download to your calendar using vCal

• Natarajan Shankar (SRI International); Leonardo de Moura (Microsoft (USA) ); Arnold Neumaier (Universität Wien); Cesare Tinelli (University of Iowa)
• Monday 24 July 2017, 11:00-12:00
• Seminar Room 2, Newton Institute.

If you have a question about this talk, please contact INI IT.

BPR - Big proof

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.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.