4 ms·
Last month Kevin Buzzard gave an interesting talk "How do you convince mathematicians a theory prover is worth their time?" about how he became involved with LE
by bsdz 6y ago
Last month Kevin Buzzard gave an interesting talk "How do you convince mathematicians a theory prover is worth their time?" about how he became involved with LEAN and some of the proofs he formalised with it:
https://youtu.be/8PLrxAfmC_o https://youtu.be/8PLrxAfmC_o
- deleted 6y ago[deleted]
- infogulch 6y agoDuring Q&A there was a friendly quarrel about 'mainstream' vs 'constructive' maths. I think there's a funny analogy in here, if you let: mainstream proof : constructive proof :: program code : machine code then Kevin is arguing that the idea of actually compiling his beautiful algorithms into machine code is silly, and that compiling program code in general is rather pointless.