steinwinde

This dispels all my doubts regarding the utility of this website.

"Element Pro" is not Open Source. Nor does it even come from the EU. From the outside it's incomprehensible anyone in EU bureaucracy would want something like this, given that there are good OS alternatives.

>> The more raw these proofs are, the better.

This was my opinion. But anyone arguing to publish "results immediately" is likely to imply something like it. I guess in chemistry we have the situation you envision - for different reasons: Laboratories holding back their data, until their scientists have published their papers or developed their products. There is a real danger AI companies will do something similar too.

Who do you expect they will select for the exposition?

On which basis do you want a (likely US based) AI company to decide who is to untangle a proof that their latest internal model has just spit out?

Do you expect this to fall to an aspiring, but still unknown mathematician at - say - the mathematics department of Nairobi university?! This is what I meant with my rather unclear "elite" reference: The first publication will always show the name of a mathematician already known to the field, more likely than not to come from the same country as the company ("Our message ... is, you’re a great American company, but you’ve got to hire great American workers"). Are you not worried at all? Don't you think it would be good, if anyone in mathematics had a chance to write that first paper on a new proof?

Where did I say they should "drop everything"? I hope to read more about how they envision their future, instead of all this regretting and whaling how one company (that I very much dislike too) published a large amount of proofs. They will get more of them, very soon - if they like it or not -, and I wish that would be the primary subject of the discussion. And yes, I'd also hope they engage with the published proofs. The more raw these proofs are, the better. If AI companies start selecting mathematicians to write nice expositions of their proofs, this is doomed to become a very elitist science.

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?! :-)