Invited Speakers

• Why the lingustic superstructure is needed?

  Andrzej Trybulec, University of Bialystok

  In principle, mathematics can be developed using a simple logic, e.g. pure predicate calculus. For practical usage, however, most of the computer formalization systems require a much richer language, where an external linguistic layer is built on top of the logical foundations. Some theoretical considerations suggest that this extension, sometimes called the linguistic superstructure, is not only a matter of convenience, but it is just necessity. We will examine selected linguistic constructs, such as expressions, adjectives, types and structures, and then describe the benefits of their use as well as the costs. Next, we will discuss the question whether some new linguistic mechanisms based on specific mathematical theories, e.g. sufficiently weak arithmetics, might also be introduced.

• Lessons learned in transforming an unreadable proof into a formalizable one.

  Thomas Hales, University of Pittsburgh

  One of the biggest surprises for me in the ongoing formalization of the Kepler conjecture has been that nearly all of my time has gone into transforming the proof into something that is capable of formalization. A day spent transforming a proof can often cut multiple days from the formalization.

• Mathematical Proofs Based on Geometric Intuition

  Krystyna Kuperberg, Auburn University

  There are proofs in the mathematical literature so strongly based on geometric intuition that the pictures seem to provide a proof. In reality, good visualization provides deeper insight and leads to a rigorous proof. Choosing the right approach may facilitate formalization, a natural next step. Adding more structure, such as a group acting on the space, often makes the formalization easier.
  We will discuss a visual approach to some breakthrough mathematical constructions in dynamics. The Brouwer Translation Theorem shows that a formal proof could prevent misconceptions. Morton Brown's proof of the Cartwright-Littlewood theorem shows that the correct choice of a proof for formalization plays a major role. Borsuk's acyclic continuum and a solution to the Scottish book problem 110 (Ulam) show that more structure on the space simplifies the construction, proof, and formalization. Wilson's symmetry, a crucial element in the solution to the Seifert conjecture concerning closed orbits of smooth dynamical systems on the three-dimensional sphere, should not be difficult to formalize.