375: TZ Discussion - How the World Went Soft
TechZing
00:00
How to Start a Proof Editor and Proof UI for Students
Jason: I'm really excited about it, but you know, it's a little out of sequence. It was Yuri who had the idea with the sort of mad lib approach as opposed to rearrangement. That's actually much more flexible. And we can have multiple proofs in a row because sometimes these questions will be like, you have to prove a couple lemmas, thenYou have to prove the big theorem is almost think of it like writing a couple helper functions and then writing a big function that uses helper functions. You need the helper functions in order to, in a coherent way, make the larger argument.
Play episode from 01:15:19
Transcript
