Thanks for pointing me to this video - it's been interesting to follow the discussion! (I personally don't see that math has lost its purpose at all in the past months. I mean, where would we be, if we were thrown at these AI based mathematical proofs and had no mathematicians and specialists?! Much of this discussion is about a disciplin readjusting its way of work and tasks.)
I would like to ask a question to you as a math professor: I think we all agree we do not know what the discipline will look like in ten years. But doesn't the rapid surge in mathematical proofs and methods imply that - at least for the coming years - there will be more, not less, work for mathematics?
Consider the "Jacobian conjecture counterexample": the work doesn't simply end once Terence Tao explains the computer-generated proof to a wider specialist audience.
1. I assume that the counterexample will give rise to a host of new questions, each of which will in turn need to be resolved. In the long run, the process of formulating questions might also be automated by AI - but likely not within the next few years to such an extent the growth of knowledge results in a decline in relevant questions.
2. Mathematicians will have a great deal to do in terms of meaningfully formalizing results within Mathlib - and hopefully Isabelle/HOL and other systems as well. From what I have read, the way current AI formalizes theorems makes them unsuitable for these libraries. I envision this as an undertaking not unlike the development of the Linux kernel. Throughout this formalization process, there should always be a human who has actually grasped the reasoning to ensure the AI hasn't simply exploited a flaw of the system.
3. Physics, chemistry, and many other sciences are currently benefiting from AI to a lesser extent. I anticipate significant changes at the interface between mathematics and other sciences as the body of mathematical knowledge expands dramatically. I cannot imagine this resulting in anything other than an increased workload, at least for the next few years.
Isn't it likely that mathematicians' workloads will initially rise rather than fall, provided they are willing to accept a shift in the nature of their tasks?
In practice, mathematicians' workloads have been a function of their work ethic, motivation, and competing demands on their time. There's no big-picture question of "how much math there is to do now"; the amount of remaining math to discover has long been presumed to be, for all intents and purposes, infinite. (Similar questions are relevant on a much smaller scale -- for example in case of someone who has specialized in a narrow specialty which goes dead.)
Your (1) is most certainly true.
As for your (2), most mathematicians I know have at most a passing interest in formalization, Mathlib, and Lean. My understanding, which is admittedly quite superficial, is that AI is actually getting quite good at translating human-readable mathematics. I could be mistaken about this, but even if there is a lot of human work to do, it sounds like a lot of anal-retentive oversight of work you didn't do yourself -- the sort of task that academics love to complain about!
Perhaps human interest in Lean will grow, but I don't anticipate it occupying the attention of more than a small slice of the community.
Your (3) is an interesting question. I work on the theoretical rather than applied side, but what you describe might very well be true for applied mathematicians.
Where I see models having a huge impact is in simulation code development.
One blocker for years now has been the adoption of GPUs. LLMs can fairly successfully and very quickly port to GPU and suggest/implement useful optimisations. Once it's verified, a code can go from anywhere between 2x to 1000x faster (mainly because CPU codes are so poorly optimised). Some science can reach much greater problem sizes, while some can run the same problems in hours rather than months and both can be revolutionary. Even more than that, LLMs seem to be finding fundamental performance bugs in both open and closed source core libraries so there's a bit of a whole-ecosystem uplift.
Can't comment on the more theoretical, less computational applied maths impacts!
I clicked on the dot for Khartoum, the only one in Sudan. It shows the Nile in Egypt, related to a movie that plays (only) in Egypt. A bit disappointing.
Anyone interested in the subject area has noticed the recent surge of AI-assisted or generated mathematics. From the outside, it is very hard to see, if AI indeed already speeds up progress in mathematics in general - apart from a number of spectacular results, (https://mathoverflow.net/questions/502120/examples-for-the-u...) - or if the quality of the large majority of these "proofs" is so poor that reviewing them is a waste of time.
I would be grateful, if someone familiar with the situation could say a word about this.
As for the proof in question - I'm not sure the author himself can firmly state he understands every detail of what he presented. In a way it's amusing that people who already enjoy a certain level of recognition outside the field are now using it to find (via shiny websites) reviewers for proofs they have worked out as a hobby using Chat GPT and the like.
What we definitely need is more recognition for those who possess the competence and energy to assess the correctness and relevance of such "results".
> reduced to checking the definition of the constant
But this doesn't mean the remaining task is small or doesn't ask much from the reviewer, does it?! Otherwise we'd see a considerable turn-out of new findings on https://palomar-registry.org/ or https://github.com/Vilin97/lean-pool , or not?! (A considerable number of the presented proofs claim new results, as far as I can tell.)
> on a long enough time horizon Gitlab or other provider isn't significantly better
I suspect the same. But do you have any evidence for this? The status pages of Github and Gitlab (more precisely their history pages) don't seem to be a good starting point for comparisons. Anything I find online are people reporting their own experiences, and it's difficult to tell how accurate they are, how many users were truely affected etc. The only thing I can vouch for is that Github has got more unreliable - adding to the hearsay myself...
Tangentially: Although many of the creators, maintainers and board members of Palomar have a background in Lean, the project welcomes alternative proof assistants, see "What about other proof assistants?" on the about (https://palomar-registry.org/about) page. From what I can tell, many in the mathematical community lament the predominance of Lean, but it reached some sort of critical mass (ecosystem, size of library) that makes it very hard to compete with - e.g. find someone who volunteers to support an alternative on Palomar, with all that this entails.
> Palomar does keep a public preservation fork of every registered source, solely as a backup for the registry in the event that the original repository disappears.
The decision to limit git sources to Github is likely in order to be able to use Github's fork mechanism. Palomar could still offer to take a copy of the relevant commit of non-Github repositories.
And since all they need is a particular folder structure, you don't really need anything Git at all. Any kind of blob would do, cf. e.g. how Zenodo works.
For a list of AI accomplishments in mathematics see https://mathoverflow.net/questions/502120/examples-for-the-u... - or a candidate list here: https://aimath.robertj1.com/ . Many have observed an affinity of AI to the search for counterexamples - or examples. Looking at afore lists, something much more sociological crosses my mind: There is a hunt for answering prominent, clearly stated problems. I'm not a mathematician, but is this mostly what progress in mathematics is about? How about stating worthwhile problems in the first place? What about theory building? Am I right saying this is equally important, but none of those utilizing AI for mathematics seem to be interested in such?
You’re correct that those things are also what mathematics is about — but they’re less constrained, hence current LLMs aren’t as good at them.
However, your last question is incorrect: people are working on that, but there haven’t been hugely useful results.
But as an example, I’ve been slowly working on implementing frameworks for theory distillation — eg, take a corpus of science papers and derive a consistent model of the world from them, such as in Lean. (Or more specifically, a sheaf defining what consistent theories are possible.)
I know nothing about mathematics, but are there not famous mathematicians like Terence Tao who utilize AI and are obviously interested in theory building?
This is a reference to Inter-Universal Teichmüller Theory. Its Wikipedia article gives a good overview (https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCll...). In maths lasting disagreements over a published "proof" are rare, but IUTT is an example of it. What the article misses: There is a more recent, ongoing effort to formalize the published proof in Lean under the name of "LANA" (e.g. see https://zen.ac.jp/news/zmcpostevent0717e and https://github.com/katobungen/LANA_report_202607/blob/pdf/LA... for a recent update). I guess most mathematicians agree that a successful compile of the proof in Lean would confirm its validity. My personal impression is that the process got stuck at the very point Peter Scholze and Jakob Stix pointed out 8 years ago. Officially LANA has still not reached a conclusion.
reply