Formalizing Possibly Infinite Trees of Bounded Degree

Formalizing Possibly Infinite Trees of Bounded Degree

Vortrag von Lukas Gerlach

• Veranstaltungsort: APB 3027
• Beginn: 6. März 2025 um 11:00
• Ende: 6. März 2025 um 12:00
• Forschungsgruppe: Wissensbasierte Systeme
• Event series: Research Seminar Logic and AI
• iCal

As Lean does not sup­port coin­duc­tive types di­rect­ly, for­mal­iz­ing in­fi­nite lists and in­fi­nite trees re­quires some "cre­ativ­i­ty". As a byprod­uct of one of our on­go­ing works, we for­mal­ized pos­si­bly in­fi­nite trees of bound­ed de­gree in Lean. In this work­shop, we will re­pro­duce this idea and present the de­f­i­n­i­tion from scratch (even with­out math­lib). We will work to­wards show­ing a spe­cial case of König’s Lem­ma: if each branch in such a tree is fi­nite, then there are only fi­nite­ly many branch­es. This is going to be an interactive talk so feel free to bring your machine with Lean installed!