BEGIN:VCALENDAR
VERSION:2.0
PRODID:icalendar-ruby
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:Europe/Vienna
BEGIN:DAYLIGHT
DTSTART:20260329T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:20251026T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260310T212833Z
UID:1770717600@ist.ac.at
DTSTART:20260210T110000
DTEND:20260210T120000
DESCRIPTION:Speaker: Marco David\nhosted by Maksym Serbyn\nAbstract: Abstra
 ct: Today’s gold standard for establishing new theoretical results in ma
 thematics is an accompanying formal computer-verification of the theorems 
 and their proofs. Interactive theorem provers (ITPs)—originally designed
  to verify computer algorithms—are now gaining significant traction in m
 athematical research. Systems such as Isabelle\, Coq\, and Lean provide pr
 ogramming languages that mechanize reasoning and thereby allow the verific
 ation of proofs. In 2024\, Google DeepMind used reinforcement learning in 
 such a formal language to win a silver medal at the International Mathemat
 ics Olympiad for the first time. The potential of formal methods in quant
 um theory remains under-explored. In this talk\, I will introduce a provoc
 atively titled list of the “top 100” quantum theorems\, aimed at gamif
 ying and popularizing the formal verification of quantum theory. Building 
 such a quantum library will provide a unified\, searchable and cross-linke
 d database of formalized mathematical knowledge. This can also allow train
 ing artificial intelligence models in an environment where precise details
  matter. https://marcodavid.net/top100/ 
LOCATION:Office Bldg West / Ground floor / Heinzel Seminar Room (I21.EG.101
 )\, ISTA
ORGANIZER:Stephanie.Dolot@ist.ac.at
SUMMARY:Marco David: QED. The Quest to Formalize Physics.
URL:https://talks-calendar.ista.ac.at/events/6265
END:VEVENT
END:VCALENDAR