diff --git a/podcast/55/index.markdown b/podcast/55/index.markdown
new file mode 100644
index 00000000..d38f185e
--- /dev/null
+++ b/podcast/55/index.markdown
@@ -0,0 +1,8 @@
+---
+title: Sebastian Ullrich
+episode: 55
+buzzsproutId: 15595231
+recorded: 2024-07-15
+published: 2024-08-16
+---
+In this episode, Niki and Andres talk with Sebastian, one of the main developers of Lean, currently working at the Lean Focused Research Organization. Today we talk about the addictive notion of theorem provers, what is a sweet spot between dependent types and simple programming and how Lean is both a theorem prover and an efficient general purpose programming language. 
diff --git a/podcast/55/links.markdown b/podcast/55/links.markdown
new file mode 100644
index 00000000..8c0601f9
--- /dev/null
+++ b/podcast/55/links.markdown
@@ -0,0 +1,14 @@
+* [Sebastian Ullrich](https://functional.cafe/@kha)
+* [Isabelle](https://isabelle.in.tum.de/)
+* [Jeremy Avigad](https://www.andrew.cmu.edu/user/avigad/)
+* [Sebastian's Masters thesis (on verifying Rust programs)](https://pp.ipd.kit.edu/uploads/publikationen/ullrich16masterarbeit.pdf)
+* [Leonardo de Moura](https://leodemoura.github.io/)
+* [Lean](https://lean-lang.org/)
+* [Sebastian's PhD thesis (on Lean 4)](https://lean-lang.org/papers/thesis-sebastian.pdf)
+* [Racket](https://racket-lang.org/)
+* [Verso](https://github.com/leanprover/verso)
+* [Helium](https://github.com/Helium4Haskell/helium)
+* [Lean use in Cedar at AWS](https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/)
+* [Lean Together Conference](https://leanprover-community.github.io/lt2024/)
+* [Reference Counting in Lean](https://arxiv.org/pdf/1908.05647)
+* [Lean FRO](https://lean-fro.org/)