CMSA New Technologies in Mathematics: A Mathematical Language

CMSA EVENTS

Speaker:

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.

Zoom: https://harvard.zoom.us/j/99018808011?pwd=SjRlbWFwVms5YVcwWURVN3R3S2tCUT09