video tutorials

Stream: general

[Kevin Buzzard]

Inspired by @Victor Ahlquist 's question in #new members I made a video tutorial on how to solve the basic logical proposition he was asking about in both tactic mode and term mode:

https://www.youtube.com/watch?v=POHVMMG7pqE

Comments, especially constructive criticism, most welcome. It has taken me months to get round to start doing this kind of thing, but now I finally have all the hardware and software and knowledge I need, so in some sense the learning can start now.

One thing I've learnt from talking to people who know a lot more about this stuff than I do, is that apparently 10 minutes is the absolute max for stuff like this, and 5 minutes is better. I was aiming for 5 but over-ran. Still under 10 though. What am I supposed to say at the end? "Like and subscribe"?? :-)

[Victor Ahlquist]

Very nice video! I thought length was good for tactic mode, but for term mode it went slightly too fast for me at least. That might be because I haven't fully understood the lambda stuff yet though. The bracket way of proving an iff was also new to me which might have contributed to my confusion.

[Kevin Buzzard]

I was very keen on keeping it short.

[Jason KY.]

Kevin Buzzard said:

One thing I've learnt from talking to people who know a lot more about this stuff than I do, is that apparently 10 minutes is the absolute max for stuff like this, and 5 minutes is better.

Why maximum 10 minutes?

[Kevin Buzzard]

Because kids your age don't watch videos which are any longer, apparently

[Kevin Buzzard]

All the MOOC lectures are 10 minutes, apparently. I am a really bad person to make these at this point because I never watch youtube videos at all; this is why I'm keen to hear from people who might actually be interested in watching them.

[Kevin Buzzard]

If you search for Lean Tutorial on youtube you can find a bunch of 90 minute videos with like 200 views from a couple of years ago

[Jason KY.]

I think people with too short attention span won't be bothered to learn lean

[Kevin Buzzard]

My 17 year old son is currently upstairs writing a C++ game engine because he's bored, and got frustrated with unity so decided to make a 2d game engine himself. He seems to only watch 10 minute videos.

[Jason KY.]

Fair enough. But I would say video length around 15 min seems to be okay.

[Kevin Buzzard]

ha ha he just came downstairs to get food, so I asked him to watch my video and his first question was "how long is it?". "Ten minutes", I said. "Oh yeah I'll watch that" he said.

[Marc Huisinga]

great video!
you might want to talk a bit more slowly.
i think when people say that 10 minutes is the maximum they mean that the entire content should fit in that time frame at a regular speed. people will also quickly lose attention if it's too fast for them.

[Andrew Ashworth]

I feel like there is a general principle, here, similar to how you would structure papers and books. Long video lectures are bad because they are difficult to index and use as a reference; a lecture is better organized if it can be subdivided into smaller self-contained topics.

[Andrew Ashworth]

I never found lecture very enjoyable :/ I can read much faster than the lecturer can speak. I can't tell my lecturer to fast-forward through the preliminary bits and then stop for 10 minutes in the middle of a difficult derivation so I can figure out what's going on. So you just end up being a human blackboard copier and struggling through it yourself when you go home.

[Andrew Ashworth]

Marc Huisinga said:

people will also quickly lose attention if it's too fast for them.

The great thing about recorded lecture is that I can rewind when I don't follow something, or continue on and come back to it if later material touches on the topic

[Marc Huisinga]

that's true, but i personally quickly lose interest when i have to rewind the material often. i certainly do this for lectures, but i find myself doing it only very rarely with regular informational youtube videos.
alternatively one can also control the speed of the video, but i only very rarely slow videos down, not sure why. i do however often speed them up when the lecturer is talking too slowly for me to keep focused.

[Jannis Limperg]

As a reasonable young person, I'd say:

• If I randomly stumble upon your video because Youtube's algorithm believes I have weird entertainment preferences, making it shorter will drastically increase the chances that I'll click it on a whim.
• If I'm specifically looking to learn Lean, you can make the video as long as you need. In this case, I'll much prefer a thorough and comprehensive treatment of the content to a rushed introduction.

[Alastair Horn]

Really great video, would love to see more! Perhaps one showcasing an area of mathlib? Depending on what your target audience is, you might consider explaining what notation like $ and <> mean, as you were more explicit when explaining the tactic mode. But maybe that's just because I'm more familiar with tactic mode. I've subscribed :big_smile:

[Alastair Horn]

"Thanks for watching" would be a good way to finish the video :)

[Kevin Kappelmann]

I'd have expected you to use assume instead of intro -- I think it looks less alien to newbies and goes better with the voice explanation, e.g. "so let us assume this as a hypothesis *types 'assume hyp'*" . Also, it would be nice if the link to the web-editor would already contain the problem statement you solve in the video :)

[Kevin Buzzard]

Another trick I missed is that I could have shown off a high-powered tactic like tauto or whatever -- something which just closes the goal immediately.

[Kevin Doran]

Thanks for the video! It was nice to see someone else's thought process.
The video felt like it went by quickly. Some 3 minute Corsera videos can go on for eternity.

[Kevin Buzzard]

I'm not sure if that's a good thing or a bad thing?

[Johan Commelin]

After split, you say "put some parentheses". I thought that means (), but you mean "braces" {}, right? (But you are the native speaker not me... so I guess I'm just wrong.)

[Johan Commelin]

Also, duplicate: https://www.youtube.com/watch?v=p4IrbnPomXg

[Kevin Buzzard]

Brackets: I think this might be a UK/US English thing

[Kevin Doran]

Kevin Buzzard said:

I'm not sure if that's a good thing or a bad thing?

Oh, a good thing!

[Keeley Hoek]

Just on the "kids these days watching short videos" (who cares what I think but): if I was looking up how to do something when I'm programming, I rarely watch videos (and I suppose if so short ones) because they are so information sparse---I just want a reference for some specific thing. (I mean sparse in the information I need.) Maybe I'd like some short videos if I had to learn about a collection of relatively disparate chemical reactions which I had to know about. But 10 min maths lectures would break my heart---there's no story, no soul!---because I don't want a reference, I'm generally hearing about something I have no idea about.

[Shing Tak Lam]

I didn't see this video earlier, but I guess I'm a part of the Kid demographic?

But short videos now according to YouTube are ones that are less than 4 minutes... And videos over 20 minutes are considered long.

With programming videos, I think short ones are nice, but I don't mind long ones if they're like Derek Banas' videos, so timestamps in the descriptions and a transcript that I can Ctrl-F through. The YouTube auto generated transcript is ok, but a proper one is nice (but takes a lot of effort). I've looked at the transcript from the Lean video, and it seems ok. Although Kevin saying the word "goal" is apparently difficult for YouTube.

Suggestions for the video:

• Put the code from the video somewhere, and link to it in the description. Then people can copy and paste if they need to. Right now if someone wants to have the solution from your video they'll need to type it up.
• SEO? Right now when I search "Lean Prover tutorial" in YouTube (incognito mode so my account has no effect), this video doesn't show up. I have to explicitly tell YouTube to sort by newest. YouTube even shows a bunch of Coq ones and Kevin's P vs NP Lecture but not this video.