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:20260425T075304Z
UID:1770825600@ist.ac.at
DTSTART:20260211T170000
DTEND:20260211T180000
DESCRIPTION:Speaker: Martin Dvorak\nhosted by Michael Sammler\nAbstract: Th
 is thesis documents a voyage towards truth and beauty via formal verificat
 ion of theorems. To this end\, we develop libraries in Lean 4 that present
  definitions and results from diverse areas of MathematiCS (i.e.\, Mathema
 tics and Computer Science). The aim is to create code that is understandab
 le\, believable\, useful\, and elegant. The code should stand for itself a
 s much as possible without a need for documentation\; however\, this text 
 redundantly documents our code artifacts and provides additional context t
 hat isn’t present in the code. This thesis is written for readers who kn
 ow Lean 4 but are not familiar with any of the topics presented. We manife
 st truth and beauty in three formalized areas of MathematiCS.We formalize 
 general grammars in Lean 4 and use grammars to show closure of the class o
 f type-0 languages under four operations\; union\, reversal\, concatenatio
 n\, and the Kleene star.Our second stop is the theory of optimization. Far
 kas established that a system of linear inequalities has a solution if and
  only if we cannot obtain a contradiction by taking a linear combination o
 f the inequalities. We state and formally prove several Farkas-like theore
 ms over linearly ordered fields in Lean 4. Furthermore\, we extend duality
  theory to the case when some coëfficients are allowed to take “infinit
 e values”. Additionally\, we develop the basics of the theory of optimiz
 ation in terms of the framework called General-Valued Constraint Satisfact
 ion Problems\, and we prove that\, if a Rational-Valued Constraint Satisfa
 ction Problem template has symmetric fractional polymorphisms of all ariti
 es\, then its basic LP relaxation is tight.Our third stop is matroid theor
 y. Seymour’s decomposition theorem is a hallmark result in matroid theor
 y\, presenting a structural characterization of the class of regular matro
 ids. We aim to formally verify Seymour’s theorem in Lean 4. First\, we b
 uild a library for working with totally unimodular matrices. We define bin
 ary matroids and their standard representations\, and we prove that they f
 orm a matroid in the sense how Mathlib defines matroids. We define regular
  matroids to be matroids for which there exists a full representation rati
 onal matrix that is totally unimodular\, and we prove that all regular mat
 roids are binary. We define 1-sum\, 2-sum\, and 3-sum of binary matroids a
 s specific ways to compose their standard representation matrices. We prov
 e that the 1-sum\, the 2-sum\, and the 3-sum of regular matroids are a reg
 ular matroid\, which concludes the composition direction of the Seymour’
 s theorem. The (more difficult) decomposition direction remains unproved.I
 n the pursuit of truth\, we focus on identifying the trusted code in each 
 project and presenting it faithfully. We emphasize the readability and bel
 ievability of definitions rather than choosing definitions that are easier
  to work with. In search for beauty\, we focus on the philosophical framew
 ork of Roger Scruton\, who emphasizes that beauty is not a mere decoration
  but\, most importantly\, beauty is the means for shaping our place in the
  world and a source of redemption\, where it can be viewed as a substitute
  for religion.
LOCATION:Office Bldg West / Ground floor / Heinzel Seminar Room (I21.EG.101
 ) and Zoom\, ISTA
ORGANIZER:
SUMMARY:Martin Dvorak: Thesis Defense: Pursuit of Truth and Beauty in Lean 
 4
URL:https://talks-calendar.ista.ac.at/events/6279
END:VEVENT
END:VCALENDAR