2026 CONFERENCE A Formalization of the Ionescu-Tulcea Theorem in Mathlib Etienne Marion Lean Together 2026, Jan 2026 HTML Video Slides