Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Machine-Assisted Proof [pdf]

ams.org

Post reply on HN
Print view View original

61–70 of 106 posts

Re: Machine-Assisted Proof [pdf]

#61

Post by brap »

crete wrote: post #38
brap wrote: post #33

Earlier quoted context omitted.

Human chess players are still incredibly valuable because we want to see what humans are capable of. For the same reason athletes are valuable even though a car can outrun them. With mathematicians, and others working in intelligence-intensive tasks (most of us here probably), I’m not sure what the value would be post-AGI.

Bluntly speaking, I think it is going to be the journey that matters; to work with mathematics is to work on yourself and a way to explore your creativity.

Right, I enjoy programming for the same reasons. But will I be able to make a living from it, 20 years from now? Probably not.

To be clear I don’t think AI is bad, and even if it is I’m pretty damn sure it’s not avoidable. But we’re in for drastic changes and we should start getting used to it.

Re: Machine-Assisted Proof [pdf]

#62

Post by vouaobrasil »

_yb2s wrote: post #58
vouaobrasil wrote: post #54

Earlier quoted context omitted.

> 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…

So far, there is zero evidence that technology can really do that. Any efficiency is countered with absolute growth. Plastic production has not decreased, and CO2 levels are rising as always.

It all comes down to probabilities, but when people find a more efficient way to use something, they use more of it.

Is there a nonzero probability that your closed economoy, zero-mining future is possible? I think so, but I think it's small. And even a 10% chance that your future will NOT come to pass is enough reason to limit technology and go for degrowth instead, which seems far more logical.

No doubt that our differences will ultimately come to valuations and what we consider important, not probabilities. There will be no reconciliation there.

Of course, what I am saying is probably entirely moot, because economy and science as it is today favors your position, and not mine. But I am willing to fight for my position regardless.

Re: Machine-Assisted Proof [pdf]

#63

Post by vouaobrasil »

zmgsabst wrote: post #59
vouaobrasil wrote: post #50

Earlier quoted context omitted.

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 are right in some sense. Of course, my objective is a long-shot: to encourage people to eschew many advanced technologies and go to a simpler way of life. Some will listen, others won't. But I do think there is a future where technology is more restricted along the lines of the Amish way. A long shot I said, but one I intend to promote regardless.

And a suspicion and dislike of advanced technology IS growing among people outside the technophile sphere.

Re: Machine-Assisted Proof [pdf]

#64

Post by vouaobrasil »

brap wrote: post #61
crete wrote: post #38

Earlier quoted context omitted.

Bluntly speaking, I think it is going to be the journey that matters; to work with mathematics is to work on yourself and a way to explore your creativity.

Right, I enjoy programming for the same reasons. But will I be able to make a living from it, 20 years from now? Probably not. To be clear I don’t think AI is bad, and even if it is I’m pretty damn sure it’s not avoidable. But we’re in for drastic changes and we should start getting used to it.

I think it's a sad thing that people may not be able to make a living from what they love. A lot of people suggest hobbies, but I think it's nice to contribute to society with the skills of our minds.

I think we have to do both: get used to it, but fight it at the same time in case we can get rid of it.

Re: Machine-Assisted Proof [pdf]

#65

Post by akoboldfrying »

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…

> I don't believe (and I've never seen any convincing evidence) that we could EVER develop more human and environmentally safe technology.

Come on now. Renewable energy is gaining on fossil fuels around the world. The air in London used to be thick with smog, and now it's not. Acid rain is a thing of the past. The ozone hole is shrinking.

Fire and the wheel are technology; are you against them too?

Re: Machine-Assisted Proof [pdf]

#66

Post by vouaobrasil »

jiggawatts wrote: post #34
kartwna wrote: post #10

"I have found it works surprisingly well for writing mathematical LaTeX, as well as formalizing in Lean; indeed, it assisted in writing this very article by suggesting several sentences as I was writing, many of which I retained or lightly edited for the final version. While the quality of its suggestions is highly variable, it can sometimes display an uncanny level of simulated understanding of the intent of the tex…

Something I've noted about all advanced tools is that the inept fear them, the capable use them, and the elite embrace them wholeheartedly. Everything from IDEs to Google search gets the same treatment. I remember a colleague watching me edit code exclaiming that I was "Cheating!" because I had syntax highlighting and tab-completion. Another coworker who had just failed to get answers after searching for "My PC crash…

> Some people are afraid of these things and suspect there's a hidden agenda, others see things for what they are: Just tools, each fit for a particular purpose.

Well, there's also the arms-race scenario. A classic example is computer security: people only make computers more secure because people hack them, which makes hackers improve their stuff. This prisoner's dilemma scenario gives a deterministic force to technology that certainly makes it more than just a tool: it is a force that acts upon society that transcends human choice.

Re: Machine-Assisted Proof [pdf]

#67

Post by [deleted] »

jiggawatts wrote: post #34
kartwna wrote: post #10

"I have found it works surprisingly well for writing mathematical LaTeX, as well as formalizing in Lean; indeed, it assisted in writing this very article by suggesting several sentences as I was writing, many of which I retained or lightly edited for the final version. While the quality of its suggestions is highly variable, it can sometimes display an uncanny level of simulated understanding of the intent of the tex…

Something I've noted about all advanced tools is that the inept fear them, the capable use them, and the elite embrace them wholeheartedly. Everything from IDEs to Google search gets the same treatment. I remember a colleague watching me edit code exclaiming that I was "Cheating!" because I had syntax highlighting and tab-completion. Another coworker who had just failed to get answers after searching for "My PC crash…

[deleted]

Re: Machine-Assisted Proof [pdf]

#68

Post by vouaobrasil »

akoboldfrying wrote: post #65
vouaobrasil wrote: post #54

Earlier quoted context omitted.

> 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…

> I don't believe (and I've never seen any convincing evidence) that we could EVER develop more human and environmentally safe technology. Come on now. Renewable energy is gaining on fossil fuels around the world. The air in London used to be thick with smog, and now it's not. Acid rain is a thing of the past. The ozone hole is shrinking. Fire and the wheel are technology; are you against them too?

> Come on now. Renewable energy is gaining on fossil fuels around the world.

What matters to me is CO2. When we can drop that below 400, then I will be impressed. As for now, I'm waiting to see if this is not just a case of Jevon's paradox.

> Fire and the wheel are technology; are you against them too?

No, those are local technologies that anyone can make with some basic knowledge. I am not against primitive technologies. We will always use them. What I am saying is that we should be like the Amish: examine individual technologies for their long-term consequences, and not develop those. And, we should regress many as well. The discussion of which and how would be lengthy but we should have it (as a society).

Re: Machine-Assisted Proof [pdf]

#69

Post by imiric »

vouaobrasil wrote: post #49
imiric wrote: post #43

Earlier quoted context omitted.

I think there will always be a demand for human knowledge workers. They might not push their respective fields forward in the same capacity as AI will be able to, but there will be a niche market for products and ideas authored entirely by humans. Programmers and mathematicians will actually be craftspeople, and communities will continue to exist around this. These will probably not be highly paid positions as they a…

The problem with this is that most people will sense a reduced importance for themselves. Most people seem to think that with AI doing everything, we can just relax and do our hobbies. But that's just wishful thinking based on a culture of overworking: we overwork so we dream of a utopia where we don't work. But the opposite of overworking is a sense of complete irrelevance, which will in some sense be more problemat…

That's true. It's a problem that isn't discussed nearly enough.

This is partly why I think that the pace of AI development needs to slow down. We've had disruptive technologies in the past, and society eventually adapted when new jobs were created, but none of them had the potential to completely replace humans in most industries. None of them raised existential questions about our humanity, the value of human labor, our place in society, and the core pillars of economy, education, etc. And, crucially, none of them were developed in just a few years.

We need time to discuss these topics and prepare for the shift. But, of course, any mention of slowing down is met with criticism of regulations stifling innovation and profits, concern about losing a technological advantage over political opponents, etc., so this is unlikely to happen.

This century certainly won't be boring, so let's enjoy the ride, and hope that no major conflict pops off. Though with the way things are going, my hope is waning.

Re: Machine-Assisted Proof [pdf]

#70

Post by viraptor »

kartwna wrote: post #10

"I have found it works surprisingly well for writing mathematical LaTeX, as well as formalizing in Lean; indeed, it assisted in writing this very article by suggesting several sentences as I was writing, many of which I retained or lightly edited for the final version. While the quality of its suggestions is highly variable, it can sometimes display an uncanny level of simulated understanding of the intent of the tex…

> He does not appear to have any issues that his thought processes are logged by servers owned by a multi-billion dollar company.

His job is publishing his thoughts. They're not going to a single company, but everyone. If he gets results faster, we all get to see his thought process faster. Ideally, chatgpt would be familiar with everything coming from researchers like him.

> constantly singing the praises of specifically ChatGPT and now CoPilot

Chatgpt is mentioned just once and only as a "such as" example.

Post reply on HN