1 - 4 February 2020, Workshop "Mathematical Language & Practical Type Theory", Bonn, Germany

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. However, 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 workshop will bring together invited experts from linguistics, formal mathematics, type theory and the LEAN prover system. 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.

The Workshop  is able to offer five scholarships for PhD students and new PhDs with previous experience in formal mathematics. The workshop will cover local costs and give travel support. Apply before November 30, 2019.