For­mal­iz­ing Pos­si­bly In­fi­nite Trees of Finite De­gree

PublikationenPublications

• Nach AutorBy Author
  • Lukas GerlachLukas Gerlach
• Nach ForschungsgruppeBy Research Group
  • Wissensbasierte SystemeKnowledge-Based Systems

Toggle side column

For­mal­iz­ing Pos­si­bly In­fi­nite Trees of Finite De­gree

Lukas GerlachLukas Gerlach

• Slides

Lukas Gerlach
For­mal­iz­ing Pos­si­bly In­fi­nite Trees of Finite De­gree
Talk at Workshop: Leaning In!, March 2025

• Details
• Bibtex

• KurzfassungAbstract
  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 finite 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.
• Weitere Informationen unter:Further Information: Link
• Projekt:Project: CPEC
• Forschungsgruppe:Research Group: Wissensbasierte SystemeKnowledge-Based Systems

@misc{G2025,
  author = {Lukas Gerlach},
  title  = {For{\-}mal{\-}iz{\-}ing Pos{\-}si{\-}bly In{\-}fi{\-}nite Trees of
            Finite De{\-}gree},
  year   = {2025},
  month  = {March}
}