Joachim Breitner's Homepage

During the last week I was attending the first Heidelberg Laureates Forum as one of the lucky 200 accepted young scientists. The HFL is a (from now on hopefully yearly) event that brings together Fields Medalists, Abel Prize laureates and Turing Award winners with young scientists (undergraduates, Ph.D. students and postdocs) from both fields in the city of Heidelberg. The extremely well organized week consisted of lectures from the laureates, some workshops held by postdocs, excursions and plenty of good food. Videos of the lectures are available (but don’t work on Linux, at least not for me ☹), and I have shot a few pictures of the event as well. I believe that my favourite lectures where Michael Atiyah’s “Advice to a Young Mathematician”, Vladimir Voevodsky’s “Univalent Foundations of Mathematics”, William Morton Kahan’s “Desperately Needed Remedies for the Undebuggability of Large-Scale Floating-Point Computations in Science and Engineering” and Alan Kay’s “Putting Turing to Work”.

Where are all the functional programmers?

During that event, one gets to talk to many other math and computer scientists researchers; sometimes just “Where are you from?” and “What do you do?”, sometimes long discussions. Unfortunately, I hardly found one who is into functional programming language research – is that only because the event was parallel to ICFP (which I really would have liked to attend as well), or is functional programming really just about 1% of all computer science?

What is a proof?

My other research interest lies in interactive theorem proving, especially using Isabelle. Of course that is a topic that one can discuss with almost everyone at that event, including the mathematicians. The reactions were rather mixed: On the one end of the spectrum, some mathematicians seriously doubt that they would ever trust a computer to check proofs and that it would ever be efficient enough to use. Others would not mind having “a button that tells whether their paper written in LaTeX is correct”, but were not keen to invest time or thought into making the proof readable by the computer. And then there were some (but very few!) who had not heard of theorem proving before and were very excited by the prospect of being able to obtain certainty about their proofs immediately and without having to bother other scientists with it.

During the mathematician’s panel discussions, where I posed the question “Do you see value in – or even a need for – machine-checked proofs in mathematics.”, Efim Zelmanov (Fields Medal 1994) said “a proof is what other mathematicians see as a proof”. I found this attitude a bit surprising – for me, a proof has always been a rigorous derivation within a formal system (say, ZFC set theory), and what we write in papers is a (less formal) description of the actual proof, whose existence we believe in. Therefore I was very happy to see Vladimir Voevodsky give a very committed talk about Univalent Foundations and how using that as the language for mathematics will allow more of mathematics to be cast in a formal, machine-checked form.

I got the chance to discuss this with him in person, as I wanted to hear his option on Isabelle, and especially on the usefulness of the style of structured proof that Isar provides, and which is closer to the style of proofs that mathematicians use in papers. He said that he enjoyed writing his proof in the style required in Type Theory and in Coq, and that maybe mathematicians should and will adjust to the language of the system, while I believe that a structured proof languages like Isar, independent of the underlying logic (HOL in this case; which is insufficient to form a base for all of abstract mathematics), is a very useful feature and that proof assistants should adjust to the mathematicians.

We also briefly discussed the idea of mine to work with theorem provers already with motivated students in high schools, e.g. in math clubs, and found that simple proofs about arithmetic of natural numbers could be feasible here, without being too trivial.

All in all a very rewarding and special week, and I can only recommend to try to attend one of the next forums, if possible.