Mechanising (Graphical) Mathematical Proofs - Computerphile

A graphical problem seems intuitive to a human, but how do you explain something formally to a machine? Dr. Mohammad Abdulaziz, Lecturer in Artificial Intelligence, King's College London
This video was initially titled "Mechanizing Mathematical Proofs"
/ computerphile
/ computer_phile
This video was filmed and edited by Sean Riley.
Computer Science at the University of Nottingham: bit.ly/nottscomputer
Computerphile is a sister project to Brady Haran's Numberphile. More at www.bradyharanblog.com
Thank you to Jane Street for their support of this channel. Learn more: www.janestreet.com

[@sanderbos4243]

Great introduction to why turning ideas into code is so hard in general!

[@couldhaveseenit]

That introduction was rough! This lecturer might have needed a few more takes to get this sounding coherent

[@elrikcourtemanche2281]

Thanks for using more colorblind friendly colors in the animations than the drawings :')

[@salmiakki5638]

If you have contatcs at Imperial College, please try to do another Video on this topic (formalizing Maths) with Kevin Buzzard! great personality and i think a bit better at getting the gist of the problem across

[@omri9325]

I'm 9 minutes in and I have no idea what I'm watching

[@PRIMARYATIAS]

In a nutshell: Formalizing a proof for some algorithm in a proof assistant.

[@Adamreir]

The guy really needs to slow down and motivate his stuff. This is really unclear.

[@charlieangkor8649]

@@Adamreir The speed and loudness of his speech varies so quickly and so intensely that I have problem adapting or his words are being pronounced incompletely. I cannot understand all he is saying.

[@dickybannister5192]

oh, very nice. having watched Tao's JMM video on here, I had some thoughts. it is nice to see how this works. it was one of my thoughts. but, going forward, he was talking about using LLMs and other tools blended to "backport" prover proofs into "human readable" ones. which is also cool, I mean, you'd get a "standardised" thing. but, I still think about how we might lose intuition. I mean, no LLM++ is going to "backport" this into a graphical proof? which surely implies, going forward, we might lose that skill unless we can replicate it? I mean, could/would a human be able to spot the graphical angle of a human readble version of the backported version of the Lean proof? (sigh! never mind!!)

[@Smogshaik]

Feels like a title mismatch and his presentation skills could be improved.

[@alegian7934]

I would enjoy more logic content!

[@TheIncredibleAverage]

I happen to be a professor of logic. Tell me, do you own a dog house?

[@jasontrunk9082]

Fantastic!

[@skunkwerx9674]

For a lecturer this was surprisingly uncoordinated

[@glenm9376]

I lasted 46secs before I realised I was never going to follow this.

[@steubens7]

nostalgic for trade, that's the flow for automated ad sales though. boo 😎

[@vicheakeng4884]

9:41

[@edwardmacnab354]

what if a computer can prove something but we as humans can't understand the proof ?

[@charlieangkor8649]

Slow down the video to 25%, then maybe we will be able to understand the proof.

[@charlieangkor8649]

Pressure of Speech - Wikipedia.

[@Lion_McLionhead]

All lions can do is bask in someone's genious when nothing is intelligible.

[@zoltantoth1566]

The video said nothing about the topic in the title [formal math [Lean]].

[@trevinbeattie4888]

Why weren’t any buyers interested in seller #6? Seller #6 ought to get out of the business if they’re not offering anything the customers want. And why do the other sellers only take a single buyer each? What’s the point of arranging sellers randomly? At first I thought that was going to be just a starting point for optimizing matches between buyers and sellers, but I didn’t see any effort to re-arrange the matches after buyer #6 was excluded.

[@spookylilghost]

This video is about the difference between showing graphical proofs to a human and getting the correct output vs needing to use extremely precise language to understand exactly what you need to tell the computer to do and get the same output. The buyers and sellers algorithm was just an example of this.

[@jeromethiel4323]

@@spookylilghost Indeed. Humans can be intuitive, but computers need the instructions to be completely clear and unambiguous, or the code doesn't work reliably. The problem is silly, but the point demonstrated is important. For instance, writing an algorithm to solve Sudoku's might sound simple, but it is anything but. Once you really start looking at it, the edge cases become increasingly important, and solving them exponentially harder. Do we really need a Sudoku solving algorithm? No, we don't. But we need algorithms that work every time for even more complex problems, and we need to know how to write them correctly so that the results can be trusted.

[@dearmash]

tl;dr: they're trying to describe using a computer to prove a behavior about a specific "suboptimal" algorithm, not trying to come up with the most optimal one.

[@georgesos]

​@@spookylilghostthis should be pinned(your comment). It explains what the video is about clearly.

[@RiXonStaR]

@@dearmash the algorithm in question is in fact the optimal algorithm for the stated problem

[@pjmmccann]

Wow, sad to have to say it, but that was a pretty awful presentation. Not sure if the Prof is excessively nervous, but slower, more carefully chosen expressions would have helped enormously, instead of incessantly cajoling the poor listener via the use of "RIGHT?", when the idea hasn't been well explained. Or maybe just less coffee??

[@charlieangkor8649]

less meth

[@PoorlyWindow549]

First that says first