seeing more math on the TL recently. i haven't mathposted in a long time but i'm still happy to field math questions from twitter peeps, just reply here or tag me or w/e. big meaty philosophical questions like "wtf are real numbers anyway" would be particularly fun for me rn
Conversation
What is your opinion on the trend of formalizing mathematics with computer proof assistants? Do you think this is ultimately a productive or counterproductive endeavor?
1
5
Replying to
sounds dope to me. could lead to a lot of very cool stuff. i’ve really enjoyed reading this blog by the :
I think it's cool, and Scholze's recent venture with Lean has been a resounding success. I'm mostly skeptical of claims like "eventually all new papers will come with formalized proofs" since I think this would slow down and whither the more human aspects of mathematics.