HCM Workshop: Mathematical Language and Practical Type Theory

Date: February 1 - February 4, 2020

Venue: Lipschitz lecture hall, Mathematics Center, Endenicher Allee 60, 53115 Bonn

Organizers: Thomas Hales (Pittsburgh), Peter Koepke (Bonn)


Formal Mathematics aims at the complete formalization and formal checking of mathematical statements and proofs. In recent years practically efficient computer assisted systems have been developed and used to formally verify outstanding mathematical results like the proof of the Kepler conjecture by T. Hales et. al. Formalizations in the currently dominating systems are written in languages that resemble computer code and are neither accessible nor attractive to the wider mathematical community. The workshop will be looking into ways to overcome this barrier by using (controlled) natural language  input for proof systems. The Naproche (Natural Proof Checking) group at Bonn and the Formal Abstracts initiative have begun to develop a controlled natural language for the LEAN prover system, which is based on dependent type theory. The workshop will bring together invited experts from linguistics, formal mathematics, type theory and LEAN. After some invited talks on Saturday we envisage intense interactions of various groups with ample time for discussion and exploratory experiments. Participants will be asked to give brief contributed presentations of their research relevant to the conference topic.

A few applications from PhD students or from researchers who very recently finished their PhD may be accepted. In case you are intereste in participating, please send your CV, your motivation letter and a letter of recommendation to the email address mentioned below.


The workshop is able to offer five scholarships to PhD students (less than one year after completion) with previous experience in formal mathematics. Please send your informative application including CV, research statement and a letter of recommendation to  mlaptt(at)hcm.uni-bonn.de before November 30,2019.


Click here for the schedule