[JoeAltmaier]

Already happened? The four-color map theorem was a computer program exhaustively going through some solution-space until it found one. Thousands of lines of logic spit out on paper. Probably impossible for any human to comprehend.

[pylua]

That had been proven previously ? I guess so has flt, but it will eventually solve an unsolved problem ?

[kevinbuzzard]

Right now, machines proving stuff which is interesting to lots of human mathematicians but unprovable by them is science fiction. People seem to have very different opinions on the following two questions:

1) Whether it will still be science fiction by 2030;

2) Whether ITPs like Lean will be useful when working on this goal, or whether it will just be LLMs all the way.

But rather than asking questions like "will some system belch out a million line incomprehensible proof of the Riemann Hypothesis" one could ask the following much easier question. Computers are very helpful to mathematicians who do calculations right now, but are way way less helpful to mathematicians who prove theorems (there are many pure mathematicians in my department who have absolutely no use for computers in their research other than the obvious email/search/etc applications). Can we make tools which will help these mathematicians (who might be trying to prove theorems about uncountable and noncomputable objects) to do their day job? Again one can ask two questions:

1) Will this still be science fiction in 2030;

2) Will ITPs be involved?

And again I don't know the answers, but this work is an attempt by the Lean community to help ITPs understand precise statements of what's going on in modern number theory, in case that helps with (1).

[pylua]

2030 will be here before you know it. I am excited that this could help distribute knowledge of the field. Good luck and Godspeed!

[JoeAltmaier]

The original proof was the computer program, as I understand it.