Machine-Assisted Proof [pdf] • Hacker News Board

Re: Machine-Assisted Proof [pdf]

#51

Post by vouaobrasil » Sat, Dec 28, 2024, 11:50 AM UTC

zmgsabst wrote: post #47

vouaobrasil wrote: post #45

Earlier quoted context omitted.

Again, like so many, you are taking computer use in math as an indivisible whole. I never said that computers were NOT useful. Only that the use of creative AIs in math are counterproductive in the long run, hence implying a point of diminishing returns that we push towards (due to the peverse incentives of academia). There is also a fundamental difference between swimming and math. There is no prisoner's dilemma sit…

You ignored the thrust of my argument: You’re lamenting that inventing boats has destroyed the beauty of swimming. - - - Edit - - - Responding to your expanded argument: You could never swim to a new continent, which boats enabled. This is the same — people can choose to keep doing the same limited math themselves, in a slower way, but will never reach the places people can aided by tools. That’s simply how the world…

I specifically gave a reason why boats and swimming is an entirely different situation. Due to different incentives, AI can take away opportunities for people to learn math the old fashioned way, but boats did not do that to swimming precisely because the incentives for swimming (moving without a boat) are different. But I added that in an edit before I saw your comment.

Re: Machine-Assisted Proof [pdf]

#52

Post by _yb2s » Sat, Dec 28, 2024, 11:51 AM UTC

vouaobrasil wrote: post #41

_yb2s wrote: post #36

Earlier quoted context omitted.

> The production of truth in an industrialized fashion is boring. Chess is a game, if it gets boring that defeats the point…. Math on the other hand is basic science research, and enables us to understand how the universe and our bodies work, to massive benefit. I don’t care how “boring” it is, the knowledge could have immense value or be critical for our survival and if AI can allow us to access it, all the better.

I would argue with your "massive benefit", unqualified. Because while it is true that basic research HAS improved life, much of modern research and technical production has decreased it: less sense of community, microplastics, climate change, destabilization of the working force (AI), less sense of purpose. What's the use of an even longer life if our entire way of life is just a production to add incremental levels…

I’m not talking about technology, I’m talking about having an understanding of how reality works. I fully agree with you that one should have a sense of ethics and use the precautionary principle when deciding what to do with that knowledge. With deeper knowledge we can develop more humane and environmentally safe technology, and cure diseases that cause massive suffering…

We’re past the point of just going back to preindustrial tech with less negative impacts- but with a deeper understanding of reality we could, e.g. pull carbon straight out of the atmosphere to manufacture almost anything in a renewable way, while also understanding biochemistry enough to make things that won’t be toxic or persist in the environment, and are readily broken down and reused.

Re: Machine-Assisted Proof [pdf]

#53

Post by vouaobrasil » Sat, Dec 28, 2024, 11:51 AM UTC

zmgsabst wrote: post #47

vouaobrasil wrote: post #45

Earlier quoted context omitted.

Again, like so many, you are taking computer use in math as an indivisible whole. I never said that computers were NOT useful. Only that the use of creative AIs in math are counterproductive in the long run, hence implying a point of diminishing returns that we push towards (due to the peverse incentives of academia). There is also a fundamental difference between swimming and math. There is no prisoner's dilemma sit…

You ignored the thrust of my argument: You’re lamenting that inventing boats has destroyed the beauty of swimming. - - - Edit - - - Responding to your expanded argument: You could never swim to a new continent, which boats enabled. This is the same — people can choose to keep doing the same limited math themselves, in a slower way, but will never reach the places people can aided by tools. That’s simply how the world…

Yes, I am arguing that we should limit our intellectual journey, to preserve the humanistic aspects of the journey. That is exactly my position.

Re: Machine-Assisted Proof [pdf]

#54

Post by vouaobrasil » Sat, Dec 28, 2024, 11:56 AM UTC

_yb2s wrote: post #52

vouaobrasil wrote: post #41

Earlier quoted context omitted.

I would argue with your "massive benefit", unqualified. Because while it is true that basic research HAS improved life, much of modern research and technical production has decreased it: less sense of community, microplastics, climate change, destabilization of the working force (AI), less sense of purpose. What's the use of an even longer life if our entire way of life is just a production to add incremental levels…

I’m not talking about technology, I’m talking about having an understanding of how reality works. I fully agree with you that one should have a sense of ethics and use the precautionary principle when deciding what to do with that knowledge. With deeper knowledge we can develop more humane and environmentally safe technology, and cure diseases that cause massive suffering… We’re past the point of just going back to p…

> With deeper knowledge we can develop more humane and environmentally safe technology, and cure diseases that cause massive suffering…

This is where we fundamentally disagree. I don't believe (and I've never seen any convincing evidence) that we could EVER develop more human and environmentally safe technology. Primarily because technology always requires physical resources (mining) and habitat destruction, and because there are 8 billion people in the world and there will always be the unscrupulous who will use that technology for destruction. And even ignoring the unscrupulous, the existing habitat destruction from said technology use already (in my valuation) is too great to balance out some of the so-called positive uses of technology.

Re: Machine-Assisted Proof [pdf]

#55

Post by [deleted] » Sat, Dec 28, 2024, 11:57 AM UTC

vessenes wrote: post #2

I'd call this paper a "big deal" in that it is a normalization of, very fair summary of, and indication that there is a future for, LLMs in pure mathematics from one of its leading practitioners. On HN here, we've spent the last few years talking and thinking a lot about LLMs, so the paper might not include much that would be surprising to math-curious HN'ers. However, there is a large cohort of research mathematicia…

[deleted]

Re: Machine-Assisted Proof [pdf]

#56

Post by zmgsabst » Sat, Dec 28, 2024, 11:58 AM UTC

vouaobrasil wrote: post #51

zmgsabst wrote: post #47

Earlier quoted context omitted.

You ignored the thrust of my argument: You’re lamenting that inventing boats has destroyed the beauty of swimming. - - - Edit - - - Responding to your expanded argument: You could never swim to a new continent, which boats enabled. This is the same — people can choose to keep doing the same limited math themselves, in a slower way, but will never reach the places people can aided by tools. That’s simply how the world…

I specifically gave a reason why boats and swimming is an entirely different situation. Due to different incentives, AI can take away opportunities for people to learn math the old fashioned way, but boats did not do that to swimming precisely because the incentives for swimming (moving without a boat) are different. But I added that in an edit before I saw your comment.

Those reasons exist for learning math: mental fitness, personal enjoyment, sport, etc.

But you’ve subtly changed your argument: before you were arguing that the beauty was in creating mathematics, not merely learning already written mathematics.

My exact point is that learning surmathematics (math taken further by AI) is it’s own interesting pursuit — and appeals to my sense of aesthetics and adventure more than piddling around merely to say it was all done by human hands.

I’m not following where you believe the swimming and boat analogy breaks down: there’s still the same personal reasons to learn and do mathematics one might swim; but learning surmathematics is an adventure to a whole new land.

- - - Edit - - -

Responding to sibling comment as well:

> I am arguing that we should limit our intellectual journey, to preserve the humanistic aspects of the journey. That is exactly my position.

That’s exactly what I compared to swimming rather than boats — because you won’t reach the same places and it’s done for aesthetic reasons.

Some people (eg, myself) want the surmathematics adventure.

Re: Machine-Assisted Proof [pdf]

#57

Post by fastneutron » Sat, Dec 28, 2024, 11:59 AM UTC

The idea of neurosymbolic systems has been in the air a long time, but every time I look at the commentary of an article like this I’m surprised at number the “OMG why didn’t anyone think of this?” type of comments.

For a while I got the impression that an ideological undercurrent of “DL vs GOFAI” had gotten in the way of more widespread exploration of these ideas. Tao’s writing here changed my view to something more pragmatic, that being the formalization of the symbolic part of neurosymbolic AI requires too much manual intervention to easily scale. He is likely onto something by having an LLM in the loop with another system like Lean or Athena to iterate on the formalization process.

Re: Machine-Assisted Proof [pdf]

#58

Post by _yb2s » Sat, Dec 28, 2024, 12:03 PM UTC

vouaobrasil wrote: post #54

_yb2s wrote: post #52

Earlier quoted context omitted.

I’m not talking about technology, I’m talking about having an understanding of how reality works. I fully agree with you that one should have a sense of ethics and use the precautionary principle when deciding what to do with that knowledge. With deeper knowledge we can develop more humane and environmentally safe technology, and cure diseases that cause massive suffering… We’re past the point of just going back to p…

> With deeper knowledge we can develop more humane and environmentally safe technology, and cure diseases that cause massive suffering… This is where we fundamentally disagree. I don't believe (and I've never seen any convincing evidence) that we could EVER develop more human and environmentally safe technology. Primarily because technology always requires physical resources (mining) and habitat destruction, and beca…

> Primarily because technology always requires physical resources (mining) and habitat destruction

There is no fundamental reason to require such things. As Fuller said, the goal of technology is to “do more and more with less and less until you can do everything with nothing.”

In my view it’s not the idea of technology that has been the problem, but that it was done by people with no understanding of the impacts, or sense of responsibility. The reason our current tech is so nasty and damaging is because our knowledge has been too primitive to do better thus far, and now people are not willing to give it up.

Synthetic biology, for example can now pull carbon straight from the air and make it into nontoxic biodegradable building materials- or really almost anything. This can eventually replace all mining and toxic chemical factories, with basically just old fashioned fermentation in a vat, that neither produces or uses anything toxic- but can replace all of the nasty stuff we currently make from mining and petroleum. A deeper understanding of biology will allow us to further reduce risks and environmental impacts by really deeply understanding which molecules we can make safely without toxic impacts on humans or other species, and without environmental persistence.

Re: Machine-Assisted Proof [pdf]

#59

Post by zmgsabst » Sat, Dec 28, 2024, 12:06 PM UTC

vouaobrasil wrote: post #50

zmgsabst wrote: post #46

Earlier quoted context omitted.

Chess has never had a larger community — entirely because computers enable streaming and exciting faster games.

Again, I am not arguing against ALL computer use of chess. Just the chess engine/AI itself. Why do you insist on taking all of technology as an indivisible unit in your argument?

They’re the same technology: you don’t get to select only some of the applications, which appeal to your personal aesthetics.

We arrived at engines before online chess, and the two have come up together — both being enabled by the growth of computers. You can choose not to use an engine, but it will exist either way because others will choose to use it when it’s enabled by those same things.

To get rid of the engine, you have to get rid of computers — or in the case of Freestyle/Chess960, create so many openings a human can’t memorize them all so only has a short time to prepare.

Re: Machine-Assisted Proof [pdf]

#60

Post by vouaobrasil » Sat, Dec 28, 2024, 12:07 PM UTC

zmgsabst wrote: post #56

vouaobrasil wrote: post #51

Earlier quoted context omitted.

I specifically gave a reason why boats and swimming is an entirely different situation. Due to different incentives, AI can take away opportunities for people to learn math the old fashioned way, but boats did not do that to swimming precisely because the incentives for swimming (moving without a boat) are different. But I added that in an edit before I saw your comment.

Those reasons exist for learning math: mental fitness, personal enjoyment, sport, etc. But you’ve subtly changed your argument: before you were arguing that the beauty was in creating mathematics, not merely learning already written mathematics. My exact point is that learning surmathematics (math taken further by AI) is it’s own interesting pursuit — and appeals to my sense of aesthetics and adventure more than pidd…

> That’s exactly what I compared to swimming rather than boats — because you won’t reach the same places and it’s done for aesthetic reasons.

For some reason, and I can't explain it, but I do believe that people still value personal physical achievements even when machines can do it better, but the same is not true of mental achievements. I take it as an axiom.

> Some people (eg, myself) want the surmathematics adventure.

That is where we fundamnetally differ, again axiomatically. I think it's offensive. But even if you do like it, that will eventually lead to the path where AI is just doing mathematics so well that no one will have much of a chance to understand what it is doing at all. And that ultimate conclusion, or even a probably chance of it, is enough reason to scrap the whole thing.