Applied mathematics is funded because of its practical use. Pure mathematics, like other theoretical fields, is funded to explore ideas practically oriented people ignore. Most of the time such exploration produces nothing of practical value. But occasionally theoreticians stumble upon ideas that turn out to be fundamental to understanding something practically oriented people discover much later.

> It's funded because of its practical use.

That's exactly what the Simons foundation was set up to reject, and it's one of most important funding streams for math

Mathematics as a field will not cease to exist, and not everyone will be interested in (or qualified to) managing the fields progress and its applications.

Haha, the breaks from reality there are two, one professionals do not spend most of their time inventing proofs, and two, practical use? :-)

Plenty of these AI proofs have been accepted. On the most important result, on the Quasi-Riemann Hypothesis, there is no serious belief it's wrong. Mathematicians have already dissected and reformulated the claims.

The proof with the 11/12 constant, the simplest one, has already prompted what looks like chagrin from some. It's an unexpected combination of known results/techniques, a combination that apparently fell into a blind spot so it wasn't picked up before (even though it could have been, even 20 years ago).

I think these results are showing there was a lot of low hanging fruit that human mathematicians didn't have the breadth or mental bandwidth to find.

Isn't it also possible that the written proofs themselves are incorrect, say, for example, by mis-specification of constraints? Let's say I publish what I claim is a proof that 2+2=4, but in the Lean specification, I proved 1+1=2.

the impression i get is that people don’t per se assert that exploitable bugs exist in Lean, but that the volume of (code) proofs published represent a new magnitude of challenge to the integrity of Lean.

the obverse would be to assert that Lean (or any other theorem prover) is infallible under all circumstances, present and future - an even weightier claim in my opinion.

No. Lean being bug-free is a far bigger claim.

Hmm, am no expert at Lean, but on one hand, since it's a programming language, guessing it necessarily means like all other programming languages, it has bugs.

But on the other hand, agree with you that the chances that one its bugs causes a solved proofs to be wrong is probably very, very low. Yeah, each version of Lean obviously must be run against hundreds if not thousands tests of existing proofs to ensure it's working correctly...

... Although, one thing that is a little worrying is that some mathematicians have said the Lean code generated in these OpenAI proofs is supposedly really complex and undecipherable. It might be pushing Lean to corner cases that are not well tested.

There's been many bugs found in Lean already, and there are probably still a few. So that's not the main issue.

Many academic disciplines bring no everyday life improvements. They exist because they provide intrinsic value and long-term foundations, hence they aren't merely entertainment. Mathematics/physics happen to be fields that span the entirety of applied/pure spectrum. Those said, your question can be generalized: Should society continue funding human intellectual activities when AI can perform them substantially better?

Mathematicians can have as much fun as they want while working on math problems, they have the skills and the brains, why shouldn't they enjoy their work?

With math you never know up front what 'real improvements in engineering and other life improving fields' will require some key bit of it that someone interested in pure math came up with a decade or two (or 10) before we found an application.

Why do you think we pay historians or english professors?

> Why do you believe human brains are magic?

We chose the problems to value. Literally every step of a proof is equally proved as the starting point. The choice of the starting point is what makes the problem, and it's a normative choice, which is to say it is a social choice.

Why do you believe that LLMs are good at the same things humans are?

It's not magical abilities - humans have proved for millenia that they can find novel solutions to problems - we have no idea how that comes to be though (which could be called magic I guess)

At issue with AI is that it's searching an existing corpus for fragments of solutions generated by humans - that's not necessarily novel, and we've not yet worked out how to make the machines actually invent.

How do you reach the conclusion that society is something that admits rational design?

What?