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.

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.