Ah, thanks! That particular idea had not occurred to me. I would like to add standard syntax coloring to the Lean code, and I have also imagined maybe highlighting hypotheses when they get used (e.g. `rw [hab]` would highlight the hypothesis `hab` in addition to transforming the target).
This video made me look up Lean, and now I've completed all the Games on the site that you showed, and i really liked them! Wish there were more of them or something like them. The only idea I've had was formalizing some of the proofs that we have at the uni for fun, but not much else, which is unfortunate. Maybe I can now rewatch some of the other videos on your channel where you prove theorems from olympiads or something, since that went way over my head on the first watch
excellent video! a few suggestions if I may, as a reaction and not having not having tried yet your library first hand. - Colors for animation and syntax, as suggested below. - Also a way of tracing the tree backwards. - Ideally, a verbose way of describing the steps, maybe with a LLM specifically designed for this scope
Cool video. Somewhere in the elaboration of rewrite to an actual call to the eliminator for equality, you should have the motive i.e. precisely the context pointing out the locations being rewritten that your greedy matcher is trying to reconstruct.
That's good to know! Not all goal transitions are rewrites, but maybe other kinds of transitions have similar ways to get the precise correct matching.
I was thinking of doing a project like this, this is super cool. There's another project called Lean Widgets that lets you embed visualizations directly in the proof state, it could be fun to have an interactive version of this in there.
An amazing idea and great execution! It would be cool to add a visual grammar of animations for the different tactics so it's instantly obvious what's happening: for `rfl` for instance you could make the symbols jump in sync on either side of the expression as they disappear, for proof by assumption the respective assumption can be briefly highlighted etc.
I have been thinking about trying to make a videogame around the calculus of inductive constructions to spoonfeed theorem proving to people but where the expressions already in your environment are like cards in your hand with different abilities and where you also have a few contextual tactics you can apply to the goal
@@dwrensha I have looked at it a little bit but I should play more, I'm always so impressed with the whole Lean community. What I really want to do is make something that doesn't scare off people who are afraid of notation or maybe the idea of it even really being a math activity rather than just a puzzle game. I have lots of friends who really enjoy games like Magic The Gathering but who believe that they could never be good at math, even though the way they think through their strategy in-game is no less deductively sophisticated than a math proof. So I was hoping that presenting it all in a more familiar format (and putting it on a platform like Steam or for the Switch) would make it more accessible to people, but so far I've spent most of my development time over the past couple weeks just messing around with font rendering and not even making a start with the core systems. I wasn't sure whether I would want to build it off of Lean or just make my own bespoke less sophisticated thing, since trying to build a game around actual Lean itself seems like it could be challenging. But this video has made me think that I should consider it more.
Yes, Manim would work too! I'm in fact using Manim in this video for almost everything that isn't a Blender animation. Although it's not strictly needed here, one thing I have found to be tricky in Manim is drawing an animation that has multiple independent things happening simultaneously.
@@dwrensha I believe, and don't quote me on that, there is a way to assign with indices which symbol in an original line if text corresponds to which symbol in the resulting line of text when animating one line of text transforming into another
Incredible video! What I’m wondering is if the code for the chess puzzles could be reworked/extended to a sudoku game? Someone did make sudoku in lean before but it required you to know the solution beforehand/get a computer to solve it first. I feel like with your method, that wouldn’t be necessary.
Yes, encoding sudoku in a similar manner should be quite possible. I expect it would be a fun exercise, if you wanted to try it. Note also that Lean 4 has "user widgets" that support arbitrary visualization, but I still think there's a strong appeal to encoding everything directly in Lean syntax.
It seems that RUclips removes my reply if I include a link to my code, but it works! It's very much a prototype right now, but I was able to solve a *very* simple sudoku (i.e. only one number was missing). I think this could be really cool.
It seems that RUclips is so trigger happy with this that I can't even put the name of the repository here, so I guess I'll have to give it in the form of a riddle. It's on Github. I'm the person who added the BMO questions to Compfiles.
Software I used for this video: Manim, Blender, OBS, GIMP, Final Cut Pro, and Apple Motion. It took me about a month to do all the animation, video editing, and audio recording.
I should clarify that the Blender animations took only a couple days, because now that I have automatic tools to create them, those are straightforward to crank out. It's all the lead-up that took so long.
I think you should change the color of the text you are about to transform, so people are looking at that part when the animation begins.
Ah, thanks! That particular idea had not occurred to me. I would like to add standard syntax coloring to the Lean code, and I have also imagined maybe highlighting hypotheses when they get used (e.g. `rw [hab]` would highlight the hypothesis `hab` in addition to transforming the target).
“end of proof, end of video” nice and succinct
I didn't say it in the video, so I'll say it now: thanks for watching!
This is really making me want to learn Lean, thanks for the superb video!
You should do it!
That's incredibly creative, especially the animated chess demo. I knew that Lean had meta programming, but this took it to a new level!
This video made me look up Lean, and now I've completed all the Games on the site that you showed, and i really liked them! Wish there were more of them or something like them. The only idea I've had was formalizing some of the proofs that we have at the uni for fun, but not much else, which is unfortunate. Maybe I can now rewatch some of the other videos on your channel where you prove theorems from olympiads or something, since that went way over my head on the first watch
excellent video! a few suggestions if I may, as a reaction and not having not having tried yet your library first hand.
- Colors for animation and syntax, as suggested below.
- Also a way of tracing the tree backwards.
- Ideally, a verbose way of describing the steps, maybe with a LLM specifically designed for this scope
See my more recent two videos for syntax coloring!
Cool video. Somewhere in the elaboration of rewrite to an actual call to the eliminator for equality, you should have the motive i.e. precisely the context pointing out the locations being rewritten that your greedy matcher is trying to reconstruct.
That's good to know! Not all goal transitions are rewrites, but maybe other kinds of transitions have similar ways to get the precise correct matching.
oh my GOD this is so cool wow
I was thinking of doing a project like this, this is super cool. There's another project called Lean Widgets that lets you embed visualizations directly in the proof state, it could be fun to have an interactive version of this in there.
Great Work🎉 You have inspired me to try to recreate this using MANIM
good job i like how the exposition finally came out. I remember you demoing this in the lean immunity meeting and wondering how you were going to use
nice Ben Eater voice
Wow! Great work
An amazing idea and great execution! It would be cool to add a visual grammar of animations for the different tactics so it's instantly obvious what's happening: for `rfl` for instance you could make the symbols jump in sync on either side of the expression as they disappear, for proof by assumption the respective assumption can be briefly highlighted etc.
I agree that would be cool!
I didn't understand anything but it looked like a fabulous project!
This makes Lean way more accessible (at 0.5x speed)
It’s so cool right? But yeah I could _not_ figure out what was going on so there was a lot of pausing and rewinding for me lol
wow, great work
bro, only one question. from which planet are you? nice work
oh my god I have been thinking about trying to do this exact thing for the last couple weeks and you have already done it
I have been thinking about trying to make a videogame around the calculus of inductive constructions to spoonfeed theorem proving to people but where the expressions already in your environment are like cards in your hand with different abilities and where you also have a few contextual tactics you can apply to the goal
@@connemignonne Have you tried the Natural Number Game? It does a pretty good job at presenting a non-overwhelming set of possible next moves.
@@dwrensha I have looked at it a little bit but I should play more, I'm always so impressed with the whole Lean community.
What I really want to do is make something that doesn't scare off people who are afraid of notation or maybe the idea of it even really being a math activity rather than just a puzzle game. I have lots of friends who really enjoy games like Magic The Gathering but who believe that they could never be good at math, even though the way they think through their strategy in-game is no less deductively sophisticated than a math proof. So I was hoping that presenting it all in a more familiar format (and putting it on a platform like Steam or for the Switch) would make it more accessible to people, but so far I've spent most of my development time over the past couple weeks just messing around with font rendering and not even making a start with the core systems. I wasn't sure whether I would want to build it off of Lean or just make my own bespoke less sophisticated thing, since trying to build a game around actual Lean itself seems like it could be challenging. But this video has made me think that I should consider it more.
This looks really good. Maybe using Blender for the animation is a bit overkill. Have you thought about using manim since you are using python anyway?
Yes, Manim would work too! I'm in fact using Manim in this video for almost everything that isn't a Blender animation.
Although it's not strictly needed here, one thing I have found to be tricky in Manim is drawing an animation that has multiple independent things happening simultaneously.
@@dwrensha I believe, and don't quote me on that, there is a way to assign with indices which symbol in an original line if text corresponds to which symbol in the resulting line of text when animating one line of text transforming into another
Incredible video! What I’m wondering is if the code for the chess puzzles could be reworked/extended to a sudoku game? Someone did make sudoku in lean before but it required you to know the solution beforehand/get a computer to solve it first. I feel like with your method, that wouldn’t be necessary.
Yes, encoding sudoku in a similar manner should be quite possible. I expect it would be a fun exercise, if you wanted to try it. Note also that Lean 4 has "user widgets" that support arbitrary visualization, but I still think there's a strong appeal to encoding everything directly in Lean syntax.
It seems that RUclips removes my reply if I include a link to my code, but it works! It's very much a prototype right now, but I was able to solve a *very* simple sudoku (i.e. only one number was missing). I think this could be really cool.
Nice!
Yeah, RUclips really doesn't like links in comments.
It seems that RUclips is so trigger happy with this that I can't even put the name of the repository here, so I guess I'll have to give it in the form of a riddle. It's on Github. I'm the person who added the BMO questions to Compfiles.
It won't even let me describe where I put the code.
Amazing video! How did you animate your visuals and how long does it usually take?
Software I used for this video: Manim, Blender, OBS, GIMP, Final Cut Pro, and Apple Motion.
It took me about a month to do all the animation, video editing, and audio recording.
@@dwrensha wow, that is a crazy amount of dedication! love to see it!
I should clarify that the Blender animations took only a couple days, because now that I have automatic tools to create them, those are straightforward to crank out. It's all the lead-up that took so long.
@@dwrensha oh i see
nice
great video! are you using lean in emacs?
Affirmative!