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!

[Bjørn Kjos-Hanssen]

Is there any documentation on the chess syntax in Chess.lean? For example, if both rooks can move to a1 how do I specify which one?

[David Renshaw]

Hm... looking back at the code it looks like it is intended to be able to handle this. I think you can specify the starting square of the rook, e.g. "Ra4a1" would mean "the rook on a4 goes to a1".

[David Renshaw]

And it might even work to do "Raa1" to mean "the rook on the a-file goes to a1".

[Bjørn Kjos-Hanssen]

Thanks for the prompt response! I am having trouble moving the pieces on my own in Example218.lean.
For example:

def example_5 :=
    ╔════════════════╗
    ║▓▓░░▓▓♕]▓▓░░▓▓░░║
    ║♔}♕]░░▓▓░░▓▓♕]▓▓║
    ║▓▓░░▓▓░░♕]░░▓▓░░║
    ║♗]▓▓♕]▓▓░░▓▓░░♕]║
    ║♗]░░▓▓░░▓▓♕]▓▓░░║
    ║♘]▓▓░░♕]░░▓▓░░▓▓║
    ║♘]♖]▓▓░░▓▓░░♕]░░║
    ║♚]♝]░░▓▓♖]▓▓░░▓▓║
    ╚════════════════╝

set_option linter.hashCommand false
#widget ChessPositionWidget with { position? := example_5 : ChessPositionWidgetProps }

set_option maxRecDepth 1000
example :
    ForcedWin .white
      example_5 := by
  with_panel_widgets [ForcedWinWidget]
    move "Rb2b1"
    sorry

doesn't work, nor does move "Rb2×b1". The error is failed to make move

[David Renshaw]

It's possible that I never got around to actually implementing move disambiguation, beyond basic parsing support for it.

[Bjørn Kjos-Hanssen]

Hmm, Qb1 also doesn't work although it's unambiguous. Whereas for example Nc1 does work.
And Qh8 succeeds even though it's ambiguous.
(Maybe it's about whether the opponent has a legal move afterwards or something?)

[Bjørn Kjos-Hanssen]

The widget is really nice though!

[Bjørn Kjos-Hanssen]

I made a modification to ForcedWin etc. to no longer consider a stalemate as a win for one side; interested in a PR containing that?

[David Renshaw]

sure!