Summer of Math Exposition

I really like the animation style you’ve used, and the exposition/introduction was well done. It does require some background in programming (and perhaps chess), but I think it is accessible overall.

Nice video, the animation are very nice, but it goes too fast, sometimes I did not even have the time to read the text. Also I am not sure the analogy with chess is really that enlightening, it confused me more than anything.

Good one but not much useful for students, especially for high school or undergraduate students.

This video is very successful in leading up to the Curry-Howard correspondence without using scary words and concepts. The analogies with the chess positions and the landscape give a way to intuitively understand how proof works. Ideas around proof being made intuitive is honestly impressive.

The topic is something that I haven’t heard in detail before, but I keep returning to thinking of the implications of the correspondence. I don’t think I will forget this in a long time. The animation is not only high quality but also quite unique (and the inclusion of a character makes it memorable)

One of the upsides of the video is that it is accessable with no background. However, it would be nice to throw out some more formal language in the end to even further enhance the “click” for more experienced people.

The only only problems I have with the video are the example section and the title. A lot of examples were shown but they felt too quick and too fast. I think less cases but more thoroughness would work better. The title of the video wasn’t really justified or covered in the video. I understand that it is a great attention grab, but this might cause people to click off as they are not getting what they expected. My suggestion for the title would be something like “Proof are programs” or “To prove is to code” (those might not be too good as I haven’t thought about the names much).

Overall, great introduction to a deep topic through familiar concepts. The finale and the style make it memorable. Very few flaws.

The video is credible and accurate. It is easy to follow and the work shown is clear. I think that the video could be improved for a student viewer, by framing the learning of how proofcheckers through a goal. It feels often like a list of cool things and not a list of cool things that are helping me solve a problem I have.

This is a very nice introduction to proof-checking. The chess analogies work well, and the code makes everything concrete.

Really awesome, entertaining and unique video!

There was a lot I liked about it:

• The topic was interesting and you motivated the viewer to want to keep watching. It got me thinking and wanting to learn more.
• You did a really great job at showing the viewer the idea step-by-step, it felt like you were taking viewers on a learning journey which was engaging and fun.

One piece of advice I had was to add more weight to WHY this is a useful idea. For example, you showed smaller proofs and their verification - but I believe showing a larger proof example and how the tool verified it, or even showing a common incorrect mistake people make in proofs and how the tool picks up on it, could have enhanced the video.

Great work, thanks a lot!

As someone with background in the area, the video is very clear and understandable. Yet, if I was to show it to someone with no experience in the field, I would probablly get a confused induvidual. The jump from just mathematical talk to Lean is a bit sudden and deserves more explenation on how such a language is written and what are proofs in the context of argument to a function.

What I liked:

• Excellent visuals! Overall a clean, cozy, unique style, and I like the drawings and overall design.
• Good analogies using chess and math as a game.
• Good discussion of LEAN and the rising importance of proof assistants. A relevant topic in math and the future of programming in math.

Suggested improvements:

• When mentioning proof assistants at 0:40, perhaps exclusively mention LEAN, since that’s what you discuss in length from 3:15 onwards. To help the audience have some idea/stake in the discussion, you could even mention some cool applications or interesting highlights in recent months/years, such as mathematicians like Terence Tao using them to formalize papers and even discovering logical mistakes in their own work, which helps them catch important details.
• I think the transition around 2:06 (to Chapter 2) could be a little better. It was a bit quick, and the list of symbols at 2:09 could be a bit dense (although understandable by most math audiences). Since we just talked about chess in Ch. 1, maybe we could transition to Ch. 2 by further talking about the idea of math as a bunch of rules, like a game, and we “create new things” formally by connecting them using logic. At 3:03, it’s good you mention that we need not understand all of this. Maybe explain in layman terms, what these symbols roughly do and why we need them.

Final remarks: Your perspective is valuable as there aren’t as many math videos that fuse together the programming and computer science aspects. For example, you spent a few minutes showing actual code in Lean. This is excellent if your intended audience is people who will be interested in this (like both math and programming). It might turn off some people who are not really interested in seeing the actual code (or who might like the code but maybe get overwhelmed by the math), but then again, you can’t please everyone. And of course, the video title is pretty clear that it involves the intersection of math and programming. Overall a good angle and niche, and presented in a unique style!

The pacing of logic exposed to student is very good and the visual communication is excellent. The false propositions being “dry and empty” on a lush green landscape was a slight visual mistake, however that’s a small nitpick in a very very solid video. That structure will be very helpful for students to stick to, and even attempt to recreate themselves. The most helfpul parts of this video are the pacing, the visuals, and the constant construction of insight over previous information. No “aha” moment in it except perhaps the proof to type link. The instruction could be really well paired with Velleman’s “How to prove it”. Recap of insights and wrapping up in a satisfying way over a bit more time could also help truly soak them in. Great job to the presenter!

I think this video is good. It tries to introduce a difficult subject in a short time, and I could follow it. I didn’t find the subject interesting.

It’s a nice and interesting introduction to a topic I have never payed much attention to. The presentation was good and suitable for people of various backgrounds in math and programming. The introduction and motivation was laid out clearly in the beginning and the analogy with chess was good.

The reasons why I am not giving more points are the following: Although the video content is relatively novel to my knowledge it left some of my main questions unanswered. It would have been nice to include a broader perspective on the subject and how people can really benefit from it. Right now you’re just introducing the very basics, but I don’t have a lot of motivation to go deeper into the subject, I’m missing a bit the “why should I care?”, “How can I apply these things in my own work?” or “how does that change the life of mathematicians and how proofs are performed or checked in the future?”.

This was a nice teaser about the capabilities of theorem-provers and the Curry-Howard correspondence.

Formal verification seems like one of those things that you really have to try yourself to get many feelings for. And it’s really hard to see the point without diving into real meaningful non-toy examples. But I think this could’ve benefited from an example of a nontrivial theorem being represented in Lean, and a glimpse into how its proof is laid out.

I might avoid the term “dependent product type” for Sigma types given the two potential meanings.

Really good analogy, clear explanation, nice visuals, presenting real examples in LEAN is great too. Really good way of explaining such an abstract subject

I like the animation you used to storytell and teach the prevalence of computer use in computing the accuracy of proving theorems. For the next set of videos you make, perhaps consider breaking content down into component parts drawing out more depth in the math and computer science disciplines discussed in this video. For e.g. you used some quantifiers and conditional statements to describe how a computer digests this programming to formulate proof. This can be a separate episode breaking down how the computer qualifies for a proof to be a tautology. The Ranking score is an average between these individual scores, good luck: Motivation: 9 Clarity: 5 Novelty: 7.5 Memorability: 5

I’m really tired right now but I liked this, it had good motivation and I enjoyed the drawings

This is a good beginner’s introduction to Lean. I like the chess analogy and the code examples of the Types. I would have liked the video to culminate in a proof using Lean, such as “there is no greatest prime number” which was used as an example throughout the video. It was not explained how proofs can be generalized; the function used to prove “Even 14” cannot prove “Even 12”. In the section where a nearby step is assumed to be true when proving the next step, you did not mention the Principle of Mathematical Induction, where to prove a statement is true for all natural numbers n≥x you prove it for n=x and then prove k+1 while assuming the statement is true for k. Related is Strong Mathematical Induction where you assume the statement is true for all natural numbers between n and k, inclusive, when proving it for k+1.

Really really interesting! I think this is a great introduction to the idea of proof checkers. Using chess as an analogy I think was great and demonstrating how proof checkers work by considering parts of proofs to be certain types is an idea that I had not heard but there should be a video about. So thank you for making it!