CMSA New Technologies in Mathematics: A Mathematical Language


View Calendar
February 24, 2021 3:00 pm - 4:00 pm
via Zoom Video Conferencing

Thomas Hales - University of Pittsburgh

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.