Weird thing I wish existed: I wish there were more videos of what I think of as ‘math/programming speedruns’. For those familiar with speedrunning video games, this would be similar except the idea would be to do the same thing for a math proof or programming problem. While it might seem like this would be quite boring since the solution to the problem/proof is known, I still think there’s an element of skill to and would enjoy watching someone do everything they can to get to a solution, proof, etc. as quickly as possible (in an editor, on paper, LaTex, etc.).
This is kind of similar to streaming ACM/math olympiad competition solving except I’m equally more in people doing this for known problems/proofs than I am for tricky but obscure problems. E.g., speed-running the SVD derivation.
While I’m posting this in the hope that others are also really interested, my sense is that this would be incredibly niche even amongst people who like math so I’m not surprised it doesn’t exist...
I’m not super familiar with the competitive math circuit, but my understanding is that this is part of it? People are given a hard problem and either individually or as a team solve it as quickly as possible.
3Blue1Brown has a video where he sort of does this for a hard Putnam problem. I say “sort of” because he’s not solving the problem in real time so much as retrospectively describing how one might solve it.
Yep, I touched on this above. Personally, I’m less interested in this type of problem solving than I am in seeing someone build to a well-known but potentially easier to prove theorem, but I suspect people solving IMO problems would appeal to a wider audience.
Last Thursday on the Discord we had people any% speedrunning and racing the Lean tutorial project . This fits very well into my general worldview: I think that doing mathematics in Lean is like solving levels in a computer puzzle game, the exciting thing being that mathematics is so rich that there are many many kinds of puzzles which you can solve.
This is awesome! I’ve been thinking I should try out the natural number game for a while because I feel like formal theorem proving will scratch my coding / video game itch in a way normal math doesn’t.
The problem with this is that it is very difficult to figure out what counts as a legitimate proof. What level of rigor is required, exactly? Are they allowed to memorize a proof beforehand? If not, how much are they allowed to know?
Yeah what would be ideal is if theorem provers were more usable and then this wouldn’t be an issue (although of course there’s still the issue of library code vs. from scratch code but this seems easier to deal with).
Memorizing a proof seems fine (in the same way that I assume you end up basically memorizing the game map if you do a speedrun).
I had a similar idea which was also based on an analogy with video games (where the analogy came from let’s play videos rather than speedruns), and called it a live math video.
Cool, I hadn’t seen your page previously but our ideas do in fact seem very similar. I think you were right to not focus on the speed element and instead analogize to ‘let’s play’ videos.
Serious in that I mean he might, I’d say, 0.1 that he’d be interested, but if that’s not negligible, I think if he took it up he’d be very good at it. I’ll ask him.
Weird thing I wish existed: I wish there were more videos of what I think of as ‘math/programming speedruns’. For those familiar with speedrunning video games, this would be similar except the idea would be to do the same thing for a math proof or programming problem. While it might seem like this would be quite boring since the solution to the problem/proof is known, I still think there’s an element of skill to and would enjoy watching someone do everything they can to get to a solution, proof, etc. as quickly as possible (in an editor, on paper, LaTex, etc.).
This is kind of similar to streaming ACM/math olympiad competition solving except I’m equally more in people doing this for known problems/proofs than I am for tricky but obscure problems. E.g., speed-running the SVD derivation.
While I’m posting this in the hope that others are also really interested, my sense is that this would be incredibly niche even amongst people who like math so I’m not surprised it doesn’t exist...
I’m not super familiar with the competitive math circuit, but my understanding is that this is part of it? People are given a hard problem and either individually or as a team solve it as quickly as possible.
Do you know of any videos on this? Ideally while the person is narrating their thoughts out loud.
3Blue1Brown has a video where he sort of does this for a hard Putnam problem. I say “sort of” because he’s not solving the problem in real time so much as retrospectively describing how one might solve it.
Yeah, that is one of my favorite videos by 3Blue1Brown and more like it would be pretty good.
Yep, I touched on this above. Personally, I’m less interested in this type of problem solving than I am in seeing someone build to a well-known but potentially easier to prove theorem, but I suspect people solving IMO problems would appeal to a wider audience.
Somewhat related:
https://xenaproject.wordpress.com/2020/05/23/the-complex-number-game/
This is awesome! I’ve been thinking I should try out the natural number game for a while because I feel like formal theorem proving will scratch my coding / video game itch in a way normal math doesn’t.
Related: here, DJB lays out the primary results of a single-variable calculus course in 11 LaTex-ed pages.
The problem with this is that it is very difficult to figure out what counts as a legitimate proof. What level of rigor is required, exactly? Are they allowed to memorize a proof beforehand? If not, how much are they allowed to know?
Solutions might be better to go with than proofs—if the answer is wrong, that’s more straightforward to show that whether or not a proof is wrong.
Yeah what would be ideal is if theorem provers were more usable and then this wouldn’t be an issue (although of course there’s still the issue of library code vs. from scratch code but this seems easier to deal with).
Memorizing a proof seems fine (in the same way that I assume you end up basically memorizing the game map if you do a speedrun).
I had a similar idea which was also based on an analogy with video games (where the analogy came from let’s play videos rather than speedruns), and called it a live math video.
Cool, I hadn’t seen your page previously but our ideas do in fact seem very similar. I think you were right to not focus on the speed element and instead analogize to ‘let’s play’ videos.
I have a friend who might be into programming speedrunning https://merveilles.town/@cancel/104005117320841920
Seems like the post you linked is a joke. Were you serious about the friend?
Serious in that I mean he might, I’d say, 0.1 that he’d be interested, but if that’s not negligible, I think if he took it up he’d be very good at it. I’ll ask him.
Cool!