This is a tool that accepts as input any Lean 4 theorem, and produces as output a Blender animation showing the steps of the proof smoothly evolving in sequence.

This video provides some more background and shows some examples.

IMO 2024 Problem 2
IMO 1987 Problem 4

1. Install Blender. I've been using v4.0.2, but any recentish version should work.

2. Install Pygments:

$ pip install pygments

$ lake exe cache get
$ lake exe Animate Input/NNG.lean NNG.mul_pow > /tmp/mul_pow.json
$ blender --python animate_proof.py -- /tmp/mul_pow.json