01.02.2020 - 04.02.2020

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

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

Description: 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.

Click here for the schedule

Click here for the abstracts

Participants: