/animate-lean-proofs

tool for turning Lean proofs into Blender animations

Primary LanguageLeanApache License 2.0Apache-2.0

Animate Lean Proofs

Code from this video.

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

(I've been using blender v4.0.2.)