steinwinde

Is it not more democratic, if AI companies announce new theorems and proofs, and the discipline of mathematics furthers "our understanding" - instead of that the wealthiest universities in existence (all of them in the US) use their advantageous access to AI to produce them, along with their exclusive furthering of our understanding?

In a world, where expensive AI models running thousands of agents produce the most remarkable results, how should the discipline of mathematics look like, when money and access to compute plays such a pivotal role?

With the Navier-Stokes solutions being out in the wild, any mathematician at an impoverished university can make a stab at it and help our understanding. Assume the solutions being held back by those who produced them at Harvard & Co. (until they have their nice articles ready), what would the role of mathematicians be at less affluent universities?

I do not assume AI companies will be ready to provide equal access to their AIs to worldwide mathematics.

Isn't it counterproductive for every European country with a bit of extra money to develop its own open source software stack?

Don't the stakeholders perceive this as a problem, too?

Or is it inevitable, given how differently these bureaucracies are structured?

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?

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.

I suppose you mean the book "How to Make the World Add Up" of Tim Harford?! :-)

> 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.)

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".

> 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...

Agreed.

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.

> suffer whenever either of the sources goes unreachable

This is not the way Palomar works. From the About page (https://palomar-registry.org/about):

> 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.

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?

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.

Please critisize the harassment, not libraries for providing shelter to homeless people. A well managed library has a degree of supervision that allows the visitor to do something about harassment. This level of control is also important for homeless people, who are subject to harassment more than most. A reasonably well run library is also no place to consume alcohol or drugs in plain sight. In these respects libraries are so much more apt places than train/subway stations - something acknowledged by large user groups: https://www.ala.org/advocacy/diversity/librariesrespond/serv...

15 years ago I lived in East London, and when I came to borrow books (e.g. to the "Idea Store Whitechapel"), I felt some sort of proudness seeing homeless people hanging out there, listening to mp3, having a coffee in the cheap cafeteria or - yes! - reading: True inclusion seemed to work in so few places in the country - at least there it was tangible. I live in Marseille/France now and haven't noticed this here; but a homeless person is not necessarily obvious - next time I visit, I'll have a look!

https://govstack.global/ is trying to find common grounds, but it doesn't coordinate any government work

I'm a member of an organization that collects money for Sudanese soup kitchens and hospitals in affected areas (https://sound-of-sudan.org/) , and I know a few other organizations that indirectly support such campaigns (e.g. https://sudfa-media.com/). Being personally acquainted with people, who spend much of their time, energy and last-but-not-least their own money on such activities, your claim makes me slightly angry.

> such regions the most money will be "lost" halfway

Please elaborate and don't lump all "regions" in with each other. My personal impression is that the combination of the community kitchen movement (which has its roots in the failed Sudanese revolution) and money transfers to mobile phones makes it relatively transparent where one's money goes and what it achieves. I'm not in the US, but I have no doubt that money donated to an organization like the Sudanese American Medical Association (https://sama-sd.org/about-us/finances/) largely reaches the people that need it.

> Those warloard will simply come and take it away from those citizens and provide to their armies.

I can assure you none of use would send money to hospitals or community kitchens, if this was likely to happen. What makes you think so?

According to Dario Amodei, companies bear a lot of responsibility and must act on this. Just read https://www.darioamodei.com/essay/the-adolescence-of-technol... . But it seems that he has given up on this, even if he has a president that demands "complete and total control of Greenland" etc. What "allies" is this Anthropic statement referring to anyway?

From a non-US perspective this must be disquieting to read: Not so much that Anthropic considers only US companies as partners. But what does Anthropic do to prevent malicious use of its software by its own government?

> Anthropic has also been in ongoing discussions with US government officials about Claude Mythos Preview and its offensive and defensive cyber capabilities. As we noted above, securing critical infrastructure is a top national security priority for democratic countries—the emergence of these cyber capabilities is another reason why the US and its allies must maintain a decisive lead in AI technology.

Not a single word of caution regarding possible abuse. Instead apparent support for its "offensive" capabilities.

You can listen to each of the original recordings. Just make sure you click on the first play button after you've chosen the sound, not the second (which often seems to be the default).

Reminds me of a visit of a garden restaurant in Munich, back in the days. My friend ordered a soup, but got a beer. Pointing out the mistake to the waiter, he was told that it doesn't matter, because the price is the same.