Theoretical Physics Seminar: Marco David

  • Date: –15:00
  • Location: Ångströmlaboratoriet, Lägerhyddsvägen 1 90101 or Zoom
  • Lecturer: Marco David (ENS Paris & Uppsala U.)
  • Contact person: Luca Cassia
  • Seminarium

Title: QED. The Quest to Formally Verify Mathematics

Abstract: Mathematics prides itself as the most fundamental of sciences, constructed as a pyramid of proven truths. Yet, the proof style of most mathematicians is strikingly different from an ideal, fully rigorous argument. At the same time, mathematical proofs are becoming increasingly sophisticated, stretching the boundaries of what is humanly comprehensible. Inevitably, mistakes will go unnoticed, putting the unique status of mathematics as exact science into peril. Now may be the time to reconcile the intuitive with the correct through the advent of "computer proof assistants". For the most time, this has been a topic for experts in specialized communities. More recently, major theorems in mathematics have been computer-verified by people from outside of these communities, even by students. This talk presents a journey through the field of interactive theorem proving with particular emphasis on mathematics. Challenging well-known preconceptions and exploring new perspectives, we give an outlook on future applications, including in mathematical physics.