วีดีโอ

Way too many cuts and too much jumping around to be able to follow. A slower pace would make this more helpful, given how much information one needs to absorb, both from the lean file and from the info view.

interesting cool Thanks !

very nice!

nice Ben Eater voice

I don't understand y tbh but it's impressive and cool. The editing looks great btw.

It is unbelievable that the author doesn't dwell on the characterization of the definition of the set which is the main difficulty for humans.

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

man am i glad im not doing math anymore

Here's how the proof works in simple terms: We must prove that there "does not exist a function on such that a nested function with of a unknown non-negative number that equals to number that adds up to 1,987 for all N" However we can this to saying that: We must prove that there "does not exist a function on such that a nested function with of a unknown non-negative number that equals to number that adds one to a multiple of two for another number M. Braces are use to identify tactics, brackets mean theorems We first use {intro} that changes the inductive goal into a assumption. We need a contradiction to support the proof. We first need to prove that the function is injective, meaning it has a one to one relationship. This means is that need to show that if the function with variable X is equal to the function with variable Y, it means that x is equal to Y. We create a hypothesis similar to one of hypothesis (the function with variable x is equal to the function with variable Y) using {have} but we replace N with X Next we use {rw} (a tactic that rewrite values based theorem or assumption) to change all X's to Y's. Then we can use the theorem from Nat [Nat.add_right_cancel] to cancel the two values. y + (2 * m + 1) = x + (2 * m + 1) -> x=y We finish the proof of the injective function by using {symm} to flip and {rw} to replace the values finish this sub-goal. Now we can create a contradiction. *Lean is a functional language. People who come from functional programming languages like Haskell will know what is happening. Graph theory is intertwined with functional programming because Functions are like a set of inputs and outputs. When you put a set inputs in the function you ger a set of outputs. That's how functions work when your are taught about the in middle school. Lean forces you to use this knowledge of functional programming to prove theorems. So for right now let's think about functions as sets and elements as values.* It's time for the hard part. Comment if I get something wrong. In any proof you must prove in every case the proof contradicts or not. So we have to do that for both cases. Lets create two sets or function cases. with the set or function that is not in the range (meaning it does not have a pair) of the function and another function function case of a function pair of A under the function. This is the foundation of our contradiction. We will have to prove that contradiction. We know that both of the cases contain numbers that are not greater than two M plus one. To prove that we need a two step calculation using the {calc} tactic: To prove that the cases are the range of the non-pair nested function. We use {unfold_let} (that extracts the value but {simp} can be used as an alternative) and the difference between the injective functions we proved. We need to cancel the arguments next, that which requires us to prove even more cases. Remember you must prove in every case the proof contradicts or not. The first can be solved using a subset and the second can have its goal canceled using the [set.image.mono] theorem. Next we have to prove that the numbers that are not in the range that are less than two M plus one. We use the {ext} tactic that uses extensionality theorems. Meaning that "two things are the same if they are built up with the same things." So we have to show that X that it exists in both sets. After many {rw} and a {simp} tactic that tries to simplify the value. We can use {simp_rw} with [eq_comm](equal_comminality) to close the proof. With this we know its cardinality as two M plus one. We also know that the function or set is disjoint as seen as what we proved, that can be resolved using the {aesop} tactic that will recursively resolve the current goal if it works at first. Now let's think about the function itself. We know that that the function cases are limited because both of them have a limit of two m plus one. Using that and being that it's disjointed we can prove that union is the sum of the cardinality of A and B. With that we know that the the function is injective and one of the case that does not have a pair. Now we can {rw} B in B.ncard to A. Making one side even and the other odd. An even cannot equal to an odd. That's a contradiction, so we use the {omega} tactic that checks if there's a contradiction and if it does finishes the proof. This finishes the proof. End of proof End of comment

I see theorem prover I subscribe

Great video, the animations are really nice. It seems like it would be kinda hard to follow without knowledge of lean. Even though I understood every step I still have no idea what the big picture of the proof is

Beautiful video! I hope for more content in the same style in the future!

Great work! Your exposition is solid, I expected this to be a much bigger channel.

Great Work🎉 You have inspired me to try to recreate this using MANIM

Amazing video. I only would slow down both the pace of exposition and animation, with some different use of color. Nonetheless amazing

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.

when you showed the problem I paused the video and tried to solve the problem myself, and 40 minutes later I had solved my first IMO question ever without help in the same way you did

awesome

Also I think it'd be useful during each frame to show how the current "proving goal" fits into the bigger picture. Like a small visualization of the proof tree next to the main visualization.

Nice! Please make more. It's very cool seeing how Lean can prove different theorems in practice, such as IMO ones.

amazing video will wait for more lean prover content!

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

bro, only one question. from which planet are you? nice work

Amazing video! How did you animate your visuals and how long does it usually take?

Wow! Great 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 didn't understand anything but it looked like a fabulous project!

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 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.

wow, great work

That's incredibly creative, especially the animated chess demo. I knew that Lean had meta programming, but this took it to a new level!

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

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?

This is really making me want to learn Lean, thanks for the superb video!

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.

This makes Lean way more accessible (at 0.5x speed)

oh my GOD this is so cool wow

great video! are you using lean in emacs?

woahhhh

“end of proof, end of video” nice and succinct

nice

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.

Gold, real gold. Thank you so much for this videos.

Impeccable content!!! This editing style fits this kind of video so well.

How many times can you acronym the same word while retaining that all parts of the string have some relevance to the original meaning?

Took me a surprisingly long time to figure out that the thumbnail puzzle’s solution was “First”

I think the real thing to fix about Lean is that it should play the explosion sound whenever you use well-founded induction!

ive never been more confused 😅

woah!!! super cool :> i remember having a similar max_heartbeats error when trying to use the continuity tactic a while back. maybe i should pop by the zulip chat and say hi to everyone there