This site presents an ongoing MSc thesis experiment by Sam Ritchie: using Claude Code to build a scaffold that automates formalising the lecture notes of the Causality course (Forré & Mooij) into Lean 4. Each definition and claim is shown side-by-side: the lecture-notes statement on the left, its Lean formalisation on the right.