tmhn2

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

That seems OK to me. I'd rather live in a state that funds beauty than one that doesn't. Think grants for artists, etc. A strictly practical world is not a good world to live in.

I think one reason it's discouraged is that it's not completely clear how long it lasts, and getting it early may result in less protection later in life. Also it's only been tested in that age group. (At least, this is what I heard when I researched getting it early a while ago).

Research mathematicians have been finding the tools useful [1][2]. I think those problems are interesting, novel, and hard. The AI might stumble sometimes, but it also produces meaningful, quality results sometimes. For experts working on interesting problems, that is enough to be useful.

[1] https://mathstodon.xyz/@tao/115420236285085121 [2] https://xcancel.com/wtgowers/status/1984340182351634571

In that usage the object (football) ends up in the state of spiralling. So the HN title would, strictly speaking, mean that the magnetic fields are causing the black hole to spiral, which isn't right.

It's probably sort of being mixed up with the transitive verb "to circle", which goes the other way, with the subject ending up in a state of circling.

This comment made me curious so I looked up some data (sorry for the formatting, I don't know how to do it better):

Guns per 100 people - Finland 2017: 32.49 (total of 1.79 million) [1] - US 2017: 120.5 (total of 393 million) [2]

All gun deaths - Finland 2017: 138 [1] (~77.09 deaths per million guns) - US 2017: 39773 [2] (~101.2 deaths per million guns) <- A bit higher

Mean death rate per million in mass shootings, 2009-2015 [3] - Finland: 0.132 <- A bit higher - US: 0.089

[1] https://www.gunpolicy.org/firearms/region/finland [2] https://www.gunpolicy.org/firearms/region/united-states [3] https://worldpopulationreview.com/country-rankings/mass-shoo...

The data seems to suggest that the number of deaths and mass shootings sort of tracks with the number of guns, and that Finland isn't particularly better off "per gun".

Right. What "reduction in biodiversity" means is that some species will adapt fast enough and some won't. Unfortunately, there is no lower limit to "reduction in biodiversity".

> some tropical trees will still be able to photosynthesize in tropical regions. Those will become the dominant species.

Unless the environmental changes happen too fast for adaptation to keep up with--the tree of life can have dead ends.

And another fun and powerful technique is "proof by intimidation" (https://en.wikipedia.org/wiki/Proof_by_intimidation), in which you don't have to know what you're doing, but other people have to think you do.

Not as prolific as that Nicolas Bourbaki guy, though!

John Conway showed a generalization of this problem is undecidable. I can't find a PDF but there's a blurb and citation on wikipedia: https://en.wikipedia.org/wiki/Collatz_conjecture#cite_ref-33

I don't know enough to say anything more intelligent about it, but I guess if you are reading through comments on this article you might find it interesting!

I don't think it's correct as stated in the article.

Looking at the paper, it basically says: the orbit starting with N dips to f(N) for "most" N, where f is a function that goes to infinity.

So, you can't pick f(N) = 200, but you can at least pick an f(N) that goes to infinity really slowly--a lot more slowly than previous results (f(N) = ~N^0.7924 is mentioned as a previous result).

The authors of the paper are academics in university CS departments with heavy math backgrounds (one with a B.S. in mathematics, another was a visiting professor at MIT dept of mathematics). I don't understand what you mean or how it relates to the article or surrounding circumstances.

Feedback is critical, though.

I imagine many folks who have watched a lot of videos on, say, economics or history or physics or whatever else hugely overestimate what they understand since they get no expert feedback to test their understanding.

Programmers tend to like self-teaching since it's very easy to get that feedback--write the code and see if it works! But not every subject is that way.

The little cartoon shows they are ambient-isotopic--that they are just topologically equivalent is pretty clear already!