74
‘Pure insanity’: Mathematicians will need years to make sense of OpenAI’s latest drop
(www.theverge.com)
This is a most excellent place for technology news and articles.
Also makes me wonder if it found and exploited (or got caught out by) some bugs in the Lean programming language...
(Not saying Lean is buggy, but finding bugs seems more likely to me, as a programmer who knows not much about mathematical proofs since I haven't looked at anything like that since uni, about a decade ago)