> You've seen them?

> Yes sir.

> You realize there's a government directive stating that there is no such thing as a flying saucer?

> Yes sir.

> Do you stand by your statement that you've seen flying saucers?

> Well, uh yes sir.

Plan 9, https://upload.wikimedia.org/wikipedia/commons/e/e8/Plan_9_f...

What you are arguing for is somewhat like the "proprietary period" in astronomy (e.g. see https://www.scientificamerican.com/article/nasas-plan-to-mak... ). But there is no mathematician who asked for the run of AI, i.e. there is no mathematician, who can be regarded as the owner of the result, even if ownership was temporary. Complex proofs might take years to explain in detail (think of the ternary Goldbach problem, https://en.wikipedia.org/wiki/Goldbach%27s_weak_conjecture ). It's just unfair, if AI companies held back with their data until a proof has been put into a nicely readable article, and at the same time mathematicians elsewhere are spending all their time trying to solve it.

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?

What do you think is gained, if AI companies manage "cleaning up"? Tax money?

There are good reasons not to delay publishing at all:

> They should release all their results immediately. (Imagine working on one of the problems they already solved.)

This is the most popular answer to a question regarding AI advisory group and immediate access on a popular website for professional mathematicians: https://mathoverflow.net/a/515442/473286

The whole debate regarding the behaviour of OpenAI is a red herring. Mathematics need to redefine their profession and how they work (like us software developers too). There are very good reasons to believe mathematics has an important role to play. If they could just stop talking about OpenAI and get back to work - they are very much needed, in particular now!

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.

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

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

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?

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

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

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.

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.