animating Lean proofs in Blender: a video and github repo

Stream: general

[David Renshaw]

I released a new video about automatically animating Lean proofs:
https://youtu.be/KuxFWwwlEtc

You can try it yourself by downloading the code:
https://github.com/dwrensha/animate-lean-proofs

[David Renshaw]

As part of this project, I implemented chess (well, most of the rules), including a syntax embedding so that you can do stuff like:

theorem morphy_mates_in_two :
    ForcedWin .white
      ╔════════════════╗
      ║░░▓▓░░▓▓♚]♝]░░♜]║
      ║♟]░░▓▓♞]▓▓♟]♟]♟]║
      ║░░▓▓░░▓▓♛]▓▓░░▓▓║
      ║▓▓░░▓▓░░♟]░░♗]░░║
      ║░░▓▓░░▓▓♙]▓▓░░▓▓║
      ║▓▓♕]▓▓░░▓▓░░▓▓░░║
      ║♙]♙]♙]▓▓░░♙]♙]♙]║
      ║▓▓░░♔}♖]▓▓░░▓▓░░║
      ╚════════════════╝ := by
  move "Qb8"
  opponent_move
  move "Rd8"
  checkmate

[David Renshaw]

check it out in Chess.lean in the above-linked repo

[David Renshaw]

(cc @Julian Berman @Yakov Pechersky )

[Kim Morrison]

What is opponent_move doing?

[David Renshaw]

It creates a new subgoal for each possible move.

[David Renshaw]

It could be rolled into the move tactic, but then the animation would show the two pieces moving at the same time.

[David Renshaw]

If pos1 is a position with white to move, then:

• the way to prove ForcedWin .white pos1 is by showing that there exists a move to a position pos2 such that ForcedWin .White pos2.

• the way to prove ForcedWin .black pos1 is by showing that for all legal next positions pos2, we have ForcedWin .black pos2.

[David Renshaw]

I published a new video, animating a solution to IMO1987P4: https://youtu.be/gi8ZTjRO-xI

[David Renshaw]

Now it has basic syntax highlighting, thanks to Pygments.

[David Michael Roberts]

Visually nice, but too fast for my eyeballs. The speaking pace is fine that fast (for me at least), but when something appears on screen for a fraction of a second and is changing size and moving, it might as well not be there from a visual representation standpoint. So I feel it defeats the purpose of the video somewhat.

[David Renshaw]

Thanks for the feedback!