Tactics & Keyframes: Visualizing Lean 4 Proofs in Blender

Can we make formal mathematics more fun to watch?

Links
proof animation: https://github.com/dwrensha/animate-lean-proofs
chess in Lean: https://github.com/dwrensha/Chess.lean
Natural Number Game: https://adam.math.hhu.de/#/g/leanprover-community/nng4
maze game: https://github.com/dwrensha/lean4-maze
Compfiles: https://dwrensha.github.io/compfiles/
Mathlib: https://github.com/leanprover-community/mathlib4

Chapters
00:00 - intro
01:09 - the plan
01:23 - the basics
02:12 - LSP and Infotree
03:09 - making it concrete
04:36 - animation: tutorial example
05:07 - animation: mul_pow
05:38 - animation: add_sq
06:14 - animation: gcd_eq_of_dvd_sub_right
06:47 - animation: chess
07:10 - animation: maze
07:28 - animation: IMO 2011 P3