Speaker: Thomas Hales, Univ. of Pittsburgh Dept. of Mathematics

Title: A Mathematical Language

Abstract: A controlled natural language for mathematics is an artificial language that is designed in an explicit way with precise computer-readable syntax and semantics.  It is based on a single natural language (which for us is English) and can be broadly understood by mathematically literate English speakers.  This talk will describe the design of a controlled natural language for mathematics that has been influenced by the Lean theorem prover, by TeX, and by earlier controlled natural languages. The semantics are provided by dependent type theory.