Formalizing Possibly Infinite Trees of Bounded Degree

Talk by Lukas Gerlach

Location: APB 3027
Start: 6. March 2025 at 11:00 am
End: 6. March 2025 at 12:00 pm
Research group: Knowledge-Based Systems
Event series: Research Seminar Logic and AI
iCal

As Lean does not support coinductive types directly, formalizing infinite lists and infinite trees requires some "creativity". As a byproduct of one of our ongoing works, we formalized possibly infinite trees of bounded degree in Lean. In this workshop, we will reproduce this idea and present the definition from scratch (even without mathlib). We will work towards showing a special case of König’s Lemma: if each branch in such a tree is finite, then there are only finitely many branches. This is going to be an interactive talk so feel free to bring your machine with Lean installed!