VODs of Schwartz-Zippel proof

Stream: general

[Bolton Bailey]

Here are a couple videos in a playlist I am making of me proving the Schwartz-Zippel lemma. Unfortunately the audio on the first half of the first video was lost.

The proof doesn't go very quickly, but I thought it might be good to make public if people are interested in the mistakes I make and where I get hung up when formalizing proofs.

[Bolton Bailey]

@David Renshaw @Ryan McCorvie and other livestreamers, have you all ever tried streaming to YouTube? Do you all know if it will automatically save VODs to my channel if I do?

[David Renshaw]

I've never tried it

[Ryan McCorvie]

I've never streamed on YouTube, but I think it does automatically archive them.. Serious streamers I know recommend independently using OBS, or whatever, to make a local archive. Youtube and twitch will sometimes arbitrarily yank or mute portions of archived streams.

[Bolton Bailey]

Ok I finished the proof today and uploaded the last video. This has been a fun experiment. A few lessons I learned:

• De Bruijn factor: I followed the proof here, which is about 550 words, not including equations. The first pass of the proof is around 400 lines and took me 19 hours all told (not including some false starts at the beginning I didn't record).
• What makes or breaks the time mostly seems to be how long I take to find lemmas/whether I find the right lemma first.
• A lot of the friction is actually in VSCode/the extension rather than mathlib itself - autocomplete not loading quickly enough, useless dropdown menus etc.
• A different limiting factor is managing in my head the analogy between the paper proof I am reading, and the version of it I am formalizing, with all the small modifications (sets instead of probabilities, rearranged addition instead of natural subtraction, etc.)
• When it gets down to lemmas about very low-level types like Fin, I expect automation to handle things, but it often doesn't.
• The prospect of people watching me code is not enough to stop me from swearing profusely (sorry if that bothers anyone, I promise I actually love and appreciate you all).

[Kevin Buzzard]

Re "what did I press to jump to definition" in video 4 -- it's ctrl+click.