> > Basically the same sentiment "machine output is raw data, log, sloppy > > outline" from mathematicians talking about LLM-generated proofs and > > how to embrace the slop there: […] > > Why should one embrace slop if one can just avoid it?
Well, good luck sending a proof of a theorem to a conference, when this theorem has already been proved, in Lean, by AI. However, if the conference embraces the slop and accepts papers that treat the AI-generated proof only as raw data but explain the proof to humans, propose how to make the proof more beautiful, what next questions to ask in the domain, what theories to build thanks to the new insights stemming from the AI proof, etc., then you don't need a time machine or an Amish village to survive as a mathematician in the long run. The link again, because I'm mostly repeating its lines: https://youtu.be/LKrwhjOI8Nc?si=-qI0GbJo0rTSSWTW&t=1391 _______________________________________________ ghc-devs mailing list -- [email protected] To unsubscribe send an email to [email protected]
