Maths in 5 years time - a prediction

Stream: new members

[Mr Proof]

This is my prediction of how mathematics will be in 3 years time:

First a mathematician works out a new theory by hand (perhaps with help with a conversation with an LLM). They will write up their paper in the usual style in natural language and latex. Perhaps with some nice graphics.

Then before submitting it to a journal they will feed it into the AGI which will formalise the proof and check it for consistency.

It will report back giving a short list of definitions that it had to create so the mathematician can check them.

The mathematician will then add the proof type only to the appendix along with any necessary definitions. Which is just a formalised proposition not the proof itself.

The mathematician will then send both the human readable paper AND the lean proof generated by the AI and upload it to the journal.

If accepted the theorem is added to the cloud database of theorems.

Millenium Prize Problems
=====================
These will all be formalised as propositions in Lean, and the competition will be open to anyone including AI to submit a proof on the website which is checked by the theorem prover. My prediction is AI will solve 2-3 of them with proofs that are not understandable by humans. Probably the prize money will go to Google.

Social Credit Score
================
Each mathematician will be assigned a social credit score calculated algorithmically by the AI based on proofs they have submitted. The algorithm will consider how their theorems have been used in other theorems. Of course this will be abused by some teams by repeatedly citing their own theorems. And there will be a massive scandal. Ultimately leading to all human mathematicians being banned.

[Julian Berman]

This seems like a parody, at very least by the end of the message? But I'm not sure a parody with what underlying message. Or if it isn't, if there were 2 bets, one from your FLT thread on whether the FLT proof hits a snag and then a second one for whether this happens, I'd have a hard time not betting on the FLT side even if assume the same 99.99% prior...

[Mr Proof]

Yes, indeed. As many have remarked, if we described 2025 to someone in the 1950's it would seem like a parody too!

[Aaron Liu]

Human drivers haven't been banned yet :)

[Mr Proof]

Hopefully one day they will be. It will save lots of lives.

[(deleted)]

The AI optimists make the Zulip instance really lively. I love this

[suhr]

Mr Proof said:

First a mathematician works out a new theory by hand (perhaps with help with a conversation with an LLM). They will write up their paper in the usual style in natural language and latex. Perhaps with some nice graphics.

Then before submitting it to a journal they will feed it into the AGI which will formalise the proof and check it for consistency.

You are suggesting a waterfall model of development. That's not how research works. Consider a more agile process, where formalization is a part of the research (which helps to keep track of details).

[Mr Proof]

@suhr

Well, I'm being conservative in my predictions. Given the 5 year time period I don't think most mathematicians would enjoy formalization as part of their research. I really think by then AGI will be clever enough to deal with mathematicians normal language and be able to translate it to lean without issue.

There will be some people working symbiotically with Lean to create proofs. But my belief is that the proof checking will likely be something in the background just done as a consistency check. Or to pick up errors in the proofs.

As an example, consider an English speaker wanted to submit a journal article to the Chinese Journal of Maths. It would be unlikely that they would first learn Chinese, rather they would translate it with the LLM.

[Yan Yablonovskiy 🇺🇦]

I think this lacks a crucial element -- actually conversing with mathematicians. There isn't some free market benefit to solving RH necessarily , its been assumed true by many for a long time. It is however of interest to mathematicians how you'd prove it. Aside from that, why do you feel there would be a motivation to know its simply true but it remains entirely opaque?

[Arthur Paulino]

There are several applications in many branches of engineering relying on mathematical properties known to be true but leaving the reasoning part for the whiteboard (or some formal method, when rarely applied)