The Chase in Lean -- Crafting a Formal Library for Existential Rule Research — Lukas Gerlach | Kutubxona