tmhn2

Completely wrong.

Often a problem is important because we have no idea how to solve it, which means we need to develop new machinery to solve it. That new machinery can then be used to do things we couldn't do before. Stimulating the development of that machinery is the most important part of the problem.

You should remember that mathematicians and programmers working for a company have different jobs with very different goals.

Of course you must check the statement, that is obvious. The advantage (to put it mildly) is that you don't have to check the entire proof by hand.

Yes, everyone is aware that the statement needs to be checked. No one has suggested otherwise. It goes without saying.

The "magic" of lean is that (in principle, assuming lean is sound and the proof is verified) that is all you have to check by hand. That is a big deal.

I certainly didn't intend to imply that the declaration is against using AI.

My point is just that I feel a little optimistic that the human culture around math ("ideas we disseminate in talks, private discussions and careful writeups, connecting them to the previous ideas of others" and so on, to quote the declaration) is robust even against relatively irresponsible use of AI (i.e., an onslaught of proof-slop).

And I guess we'd better try to be optimistic, because even if the declaration results in some realignment between the community and big AI companies, the models capable of this work are not always going to be exclusively under the control of those aligned parties.

That said, I think the declaration is great and I support it--let's see what comes out of it.

Hopefully that's true. Instead of bypassing the community maybe it stimulates the community. I think it does disrupt things a bit, but I'm optimistic at the moment!

I don't think that's entirely fair.

I think it's OK that there are some materials designed for a specialist audience, and some materials designed for a wider audience. Technical density serves a real purpose in the former (I'd like to just say "stack" without including an explanation 10 times longer than the rest of my paper about what a stack is and why we are talking about them), and some people expend a lot of effort on the latter (think lectures, lecture notes, textbooks, seminars, blogs, etc--totally appropriate to dig into the motivations here).

It's just the fact that it's a really vertical field, not some cultural failing, that results in pretty opaque stuff sometimes.

I'm not totally sure what you mean. You can validate the proof using lean, which is what it's for--the whole magic of it is you don't have to just trust what AI says. That said, to your larger point, there are loopholes, and we'd certainly better be able to read the statement in lean, etc.

I agree entirely with what you're saying, right up until your final question:

> why bother grinding through all the material of climbing Mt. Everest and then attempting it if the helicopter ride is how things are done now?

I think you answered this yourself earlier:

> I think progress is really measured by what humans are able to do and understand

People want to make this progress. Therefore people will "grind Everest" as a mathematical community, and that is maybe not so hugely different from a lot of previous mathematical work.

There's still ample room for creativity: simplifying, generalizing, asking new questions humans are interested in, ...

That's true, but the story would have unfolded differently if Mochizuki had a lean-verified proof and was correct. I guess baked into my premise is that AI is producing reliable proofs (in the long term at least).

I wonder if they will continue to dump proofs, though? Their point has been made, the novelty will wear off, and it maybe won't be a priority use of their resources to spend however many millions on another big proof--they will move on to the next thing to show off I'm sure. At that point, the ones generating proofs will be, I hope, mathematicians (professional and otherwise) that are more interested in the results and community discussion.

(Well that's my hopeful, optimistic take, anyway.)

As a mathematician maybe I am a little more optimistic than this declaration.

I am thinking of Mochizuki's abc conjecture: He worked in relative isolation, and dumped a huge incomprehensible proof on the community (to oversimplify a bit). That's not totally unlike what might happen if AI generates a huge, incomprehensible proof of let's say RH.

Well, what is the result? In the Mochizuki case, it was a lot of skepticism, but it also generated conferences, papers, talks in the hallway, discussions with students, and so on--a flurry of exactly that kind of community process that the declaration says is the main driver of mathematics.

Ultimately we think a fatal flaw was found in Mochizuki's proof, so it didn't lead anywhere in particular. But in our hypothetical "AI lean-verified proof of RH" situation, it would presumably generate substantially more of that community activity we saw in the Mochizuki situation. And if it's correct, that community activity would be productive (expository talks, students given problems to flesh out or generalize, etc).

Maybe mathematics just becomes a little more like other fields--relying on labs with lots of money for compute, digging through a corpus of AI-generated proofs, etc.

At issue is the fact that it doesn't typically work like: mathematician produces a proof in isolation, generates a PDF, and shares it with a bunch of people. There's a whole culture and community going on behind the scenes with conferences, seminars, lectures, chats in the hallway, advising students, etc. that AI-generated proofs bypass.

The issue of credit is a relatively minor point in the declaration.

It's more about bypassing the culture and processes mathematicians have developed that lead to human understanding, generating new ideas, and bringing up new generations of mathematicians. (See also his article about "non-renewable mining" of good problems.)

Reducing mathematics to "let's just generate results through an isolated and automated system" is a misalignment since it bypasses those processes.

> Are they paid to type code or create programs?

The goal is more to understand why something is true than just whether it is true. To oversimplify a lot, it's the difference between industry versus academic motivation. In the former case you have a point, but not so much in the latter. We really need both modes of work going on.

> As a not math person, seems strictly good that AI can solve more problems.

As a math person I think that's probably true, though it's not that simple. We do still have to understand the solutions to the problems, and take time to explore. That's how we figure out what problems should be solved in the first place. Cognitive debt is bad enough in your codebase, but you don't really want it to overwhelm entire academic disciplines.

It's important to remember that historically many advances have been made without "customer value" in mind. Indeed, freeing oneself from such concerns can open up unexpected avenues for discovery which only later provide "customer value".