# 2nd Colloquium of Research Area C3

Date: May 10, 2019

Venue: CS building, lecture room 0.016

## Program:

9:30 |
Coffee and Tee |

10:00 |
Matthias Mnich: New approximation algorithms for variants of TSP |

10:45 |
Coffee break |

11:15 |
Peter Koepke: The Naproche-SAD proof assistant |

## Abstracts:

#### Matthias Mnich: New approximation algorithms for variants of TSP

The Traveling Salesperson Problem (TSP) presents a cornerstone of combinatorial optimization. We look at this problem from the perspective of approximation algorithms, for variants of TSP whose approximability is still not fully understood. As results, we present new approximation algorithms which either improve the approximation factor, run time, or space usage of previously known algorithms.

#### Peter Koepke: The Naproche-SAD proof assistant

Automatic theorem provers and proof checkers have been used to construct completely formal proofs of deep mathematical results like the Kepler sphere packing conjecture. Large parts of the resulting proofs, however, read like computer code for proof procedures rather than like argumentative and explanatory mathematical texts.

The Naproche-SAD project, which is a recent amalgam of the Naproche project (Natural Proof Checking) at Bonn and the System for Automated Deduction (SAD) by Andrei Paskevich, aims to efficiently imitate the human checking of mathematics. Texts are accepted in a controlled natural language for mathematics, including symbolic phrases. Proofs are split up canonically into many smaller tasks which are within reach of modern automatic theorem provers. We are currently able to naturally formalize and check some chapter-sized texts at the level of undergraduate mathematics.

In my talk I shall present the Naproche-SAD proof assistant, give some background information, and discuss possible applications.