SoME_Topics
SoME_Topics copied to clipboard
leios
The inner Workings of Computer-verified Proofs : Why every Function is a Proof and vice versa.
About Me
I recently finished my Masters in mathematics and am soon going to start a PhD in Computer Science focusing on verifying the correctness of software. To hint at how I've stumbled from one field into the other one: You could say that I was a bit more interested in the details regarding proofs than the average mathematician, and if you combine this with the burning interest in computer verified proofs that I developed at some point, you can pretty much guess how it went down ;)
I have now been doing computer verified proofs of mathematical and logical results in proof assistants for about two years, and whenever I sit back and think about it, I am still fascinated by the ingenious observation that stands behind their inner workings. And that is even though I am very much used to it by now.
It's not just that the observation is quite ingenious, but it is also surprisingly approachable, and it has always been on my mind that there is - as of yet - no video about this which targets a wide audience.
Goal and Content of the Video
On the one hand, the video will hopefully give a satisfying answer for all of the people who have ever wondered: How is it possible that computers can check mathematical proofs, which are usually complicated pieces of text with the occasional greek symbol sprinkled in between?
But the main goal of the video is to show that: If you know how to define, apply and compose functions, then you have all the knowledge in place which allows you to write detailed and correct mathematical proofs.
To make matters a bit more concrete, the teaser question which will be answered over the course of the video would be:
Why does the function which maps $(f,g,x) \mapsto f(x,g(x))$ (yes, it takes functions as input) represent a fully detailed proof (!) of the logical proposition $$(A \land B \to C) \land (A \to B) \land A \to C~?$$
It will be necessary to introduce one concept which will probably be new for the majority of viewers: function definitions using $\lambda$-terms. This can be presented in a very natural way, and apart from their usage here, there are generally a lot of situation where they present a much more convenient way to define functions then the usual options.
(To be honest I am quite often puzzled about the fact that they have not yet found their way into the bag of conventional notations that are used in mathematics.)
Content Creator
I am looking for someone who is versed in using Manim or similar software to do 2D animations, mainly involving animation of text or simple pictures and diagrams. This topic does not require anything in 3D to be presented.
I think an interactive blog-post would also be a possibility to present the material, but my ideas here are not very concrete.
I am looking forward to any questions or responses!
I agree that a nice explanation of this is somewhat lacking and am curious as to how you plan to make this accessible, especially from a high-level rather than technical point of view.
Also if it really is just text and simple diagrams moving around, then perhaps powerpoint would be simpler than manim. Can you give an instance of what the toughest animation you envision is?
At one point I made a 20 minute clip going along those lines. It's Unlisted but you may find it here. Maybe it helps getting some ideas what not to do. Good luck.
@finedesignvideos The toughest animations I am envisioning right now can indeed all be done in Powerpoint. I do think that doing it in Manim or some other software would produce slicker results. I am very glad that you pointed this it out though, because I only now considered that I should just get going in Powerpoint or anything else that can already productively use. Even if that will not end up to be the final version, it will be very helpful to have any draft at all.
@Nikolaj-K Thank you for sharing this! That will definitely help me. (Have also see some videos on your channel in the past and like what you are doing👍🏻)
Ooh yes, a plan in PowerPoint would be super helpful in any case.
I've actually made a video using manim before that touched on lambda calculus for a little bit. I'm including it here. I think the highlighting part was useful but apart from that the rest of it was honestly quite a pain for something so simple.
