Maybe the next frontier for AI is to make it more pedagogical.
If the aim of mathematics is to promote greater human understanding, then surely elevating everyone’s grasp and appreciation of math is of greater import than chasing another theorem feather for our hats - especially if AI can automate the plucking.
>Finally, the next few years will be extremely interesting. We are at a new frontier, where our communal norms, values, and expectations are beginning to break down, and it’s up to all of us to figure out what should replace them
I'm tired of this cautious optimist talk. It is inevitable that without regulation, AI will eclipse humans in every possible domain, leaving everyone without direct control over the most powerful models completely powerless, economically redundant, and at the mercy of the new AI hegemony. Anything which doesn't confront this possibility honestly is just lying to people.
>Can every interesting mathematical question be answered that way? Probably not, and even questions that can may have more interesting and satisfying solutions that invoke novel ideas and insights. Perhaps, in the near future, AI systems will be able to come up with such insights, but, at the very least, let’s recognize that we are not there yet.
This keeps being repeated by AI skeptics, yet AI keeps solving more and more complex tasks. We've reached the point that it's even started solving Millennium problems.
>Telling us that some AI agent is spinning out theorems that are highly interesting to it and other AI agents does nothing for us.
This is the future of pushing the frontier though. AIs need to be pushed to get better and better. AI understanding of math is millions times more important than human's.
I think too much credit in the AI math discussion is being given to LLMs rather than to Lean, which an incredibly well designed language around which Mathlib coalesced as a side-effect of it's capability
I doubt of this progress could have been made without the specific combination of Lean + Mathlib. Automatic Theorem Provers are not a new idea, but we don't see these breakthroughs happening with any other stack