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

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

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

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

@PRIMARYATIAS

3 ай бұрын

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

@Adamreir

3 ай бұрын

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

@charlieangkor8649

2 ай бұрын

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

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

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

I would enjoy more logic content!

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!!)

Fantastic!

For a lecturer this was surprisingly uncoordinated

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

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

Not only is it hard for computers to understand maths but it is also hard for humans to understand what is going on in this video😂

9:41

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

@charlieangkor8649

2 ай бұрын

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

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

@1:05 "Aristotle is a man" Nooo DoN't AsSuMe HiS gEnDeR!!!

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

Pressure of Speech - Wikipedia.

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

3 ай бұрын

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

3 ай бұрын

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

3 ай бұрын

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

3 ай бұрын

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

@RiXonStaR

3 ай бұрын

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

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

2 ай бұрын

less meth

First that says first