alt Hacker NewsI think an under appreciated part of mathematics has been contributing clean and elegant work precisely so that others could use that as a foundation for further work and new insights. This dump from Open AI seems to be the opposite. Huge and messy, incomprehensible and taken seriously only because of Lean.
There is this assumption that AI will contribute to faster progress in math but given the garbage dump of proofs which we have to take on faith are robust I wonder if the opposite is true.
My reservation could only be dismissed if AI turns out to be able to contribute fundamental new insights and pose new problems. This takes us into an area where AI progress has been slow to say the least.
The dump from OpenAI seems to be the opposite: huge, messy, and incomprehensible, and taken seriously only because of Lean.
Math papers were hard to comprehend well before AI. This is hardly new. For example, here’s a screenshot of a paper from 40 years ago:
https://i.imgur.com/kPFlczp.png
At least with AI, you can download the LaTeX, upload the paper to your favorite LLM, and have it explain the paper at whatever level of granularity you like. That wasn’t possible even two years ago.