Animate Lean Proofs
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.
more examples
| IMO 2024 Problem 2 |  |
| IMO 1987 Problem 4 |  |
setup
-
Install Blender. I've been using v4.0.2, but any recentish version should work.
-
Install Pygments:
$ pip install pygments
running
$ 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