posted in Technology
‘Pure insanity’: Mathematicians will need years to make sense of OpenAI’s latest drop
www.theverge.com/ai-artificial-intelligence/1008726/openai-mathematics-solutions-chaos
This seems to be the mathematical equivalent of using AI to submit 200 unverified pull requests to an open source project and then telling the maintainers it’s their job to figure it all out.
The one mathematician saying he’s not going to spend hours of his time to verify if a slop report is true, let alone do it for dozens of reports, reminds me of all those projects making rules that unverified AI pull requests will be trashed.
Replying to @threeonefour@piefed.ca
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)