Live data from Hacker News

Machine-Assisted Proof [pdf]

ams.org

71–80 of 106 posts

Re: Machine-Assisted Proof [pdf]

#71
post #58

Earlier quoted context omitted.

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

I sympathize with you and feel as Thoreau said that "men have become the tools of their tools." I care deeply about the natural environment, and find most modern technology dehumanizing. I enjoy simple living and spend most of my time on a small sailboat with no electricity or motor. I personally study "primitive" skills like gathering food, and making boats and buildings with simple hand tools. I feel an essential part of being a healthy human is having a deep connection to, and knowledge about your local environment and watershed.

However, there is more than a small chance of the future I am talking about being possible where we can make virtually anything directly from carbon in the air, with little to no impacts. I am an academic scientist, and am focused on solving the specific problems that will make what I am talking about possible- and basically everything I mentioned is already working fairly well... and is already cheaper, safer, and more practical then petroleum chemistry and mining if you factor in externalities. However, the only real path I see to getting people to use it is to make it better still, so it is fundamentally cheaper and superior, without even factoring in the externalities and nasty impacts of our current way of doing things.

Degrowth is quite frankly not going to happen voluntarily, it's a cultural and political non-starter, and also leaves us with an inability to fix the massive damage to the planet we've already caused, and leaves us dying from diseases that we are very close to understanding how to prevent. We've decimated and poisoned our natural environment such that simple living is no longer even possible in most places- where I live the fish and other wildlife are almost all gone, and the few left are too toxic to eat. Let's instead go all in on understanding science so that we can in principle do almost anything we can imagine with little resources or impacts, and then also have much higher standards for what we actually choose to do with the knowledge.

Edit: I looked at your blog and agree with a lot of what you are saying, but also disagree with a lot, but see you are a deep thinker that cares a lot about this stuff. I think it would be interesting to talk to you more.

Re: Machine-Assisted Proof [pdf]

#72

Earlier quoted context omitted.

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…

Is this phobia angle the new talking point? "If you fear our tool for a hefty subscription price while we are logging all your data, you are inept?" My experience is exactly the opposite: Inept power users jump on the latest bandwagon to camouflage their incompetence. And like true power users they evangelize their latest toy whenever they can.

> tool for a hefty subscription price

There's quite a few solutions to choose with per-request pricing. Only extremely heavy users should be on the subscription these days.

You can invest in running things yourself too.

Re: Machine-Assisted Proof [pdf]

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

> In fact, due to the immense damage technology has caused, the burden of proof should be on the technologists to reliably demonstrate that new technology is even worth it beyond propping up our broken, global capitalistic system.

A fair argument as far as it goes, but unlike engineering and some other activities, mathematics isn't about creating more technology. Although mathematics can be applied to that purpose, that's not its essence.

If electronics and computers didn't exist, if industrial society didn't exist, mathematics would still exist, and perhaps it wouldn't be confused so often with its applications.

Mathematics isn't responsible for how we choose to apply it.

Re: Machine-Assisted Proof [pdf]

#74
post #11

Earlier quoted context omitted.

What’s your reasoning? There’s much more honor in being right for the right reason than for a wrong one.

I’m wagering my entire reputation that no LLM, nor any LLM run in a loop, will ever be as intelligent as a precocious child. The burden rests on OpenAI and the scholars on their payroll to show otherwise.

That's fine, and unrelated to the article in any way.

LLMs are way more useful than a child in many ways, some of which are discussed in the article. They don't need to be as intelligent as a child for anything proposed in the article.

Re: Machine-Assisted Proof [pdf]

#75

I think his comparison to previous machine-assistance is misleading. In previous cases, the use of machines was never creative, whereas now AI has the ability to suggest creative lines. In the short-term, this sounds exciting. But I also think it reduces the beauty of math because it is mechanizing it into a production line for truth, and reduces the emphasis on the human experience in the search for truth. The same…

Philosophy survived the rise of engineering. Informal mathematics will survive the rise of actually getting the answer right just the same.

Re: Machine-Assisted Proof [pdf]

#76

With all respect to luminaries: this will not stand up. This will be treated harshly by history. I’m nobody but I’m going to stand up to Terence Tao and Scott Aarinson: you’re wrong or bought or both. This is a detour and I want to make clear to history what side I was on.

[deleted]

Re: Machine-Assisted Proof [pdf]

#77
post #69

Earlier quoted context omitted.

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

Well, I certainly agree with slowing things down. Time to discuss would be much better than nothing. As I tell many, I am glad I was born when I was, and not now. I cherish the time I had before anyone knew of the internet. Even though I am using it now, mostly to spread my ideas, I would gladly trade it for a world where it didn't exist.

Re: Machine-Assisted Proof [pdf]

#78
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.

The point is that even with mathematics and programming, there is an underlying community aspect that cannot be ignored, but is hidden under layers of utility. For example, even in programming, people getting together to code, collaborating, and sharing their projects is a small but significant drop in people creating a community. With mathematics, the sharing of ideas and slaving over the proof of a theorem brings m…

If a change in other people's ability to do mathematics affects your level of enjoyment in doing mathematics, you don't really enjoy mathematics. You enjoy feeling smarter than other people, of belonging to an exclusive club.

Preserving people's access to this kind of enjoyment is not something that should carry any weight in my opinion.

Re: Machine-Assisted Proof [pdf]

#79
post #23

Earlier quoted context omitted.

Sure: Supporting stuff furthers that stuff. If it works for you, there's your incentive.

Sure, have a Pepsi. It is delicious! At this stage Tao should disclose whether he has any financial relationship with OpenAI, including stock ownership or even access to experimental models or more computational power than the average user. I've never seen any academic hyping up a company like that, unless they explicitly have/had a financial relationship like Scott Aaronson.

A decent fraction of this website is people enthusiastically promoting tools they love using. Good tech wins supporters without paying for them.

Re: Machine-Assisted Proof [pdf]

#80
post #11

Earlier quoted context omitted.

What’s your reasoning? There’s much more honor in being right for the right reason than for a wrong one.

I’m wagering my entire reputation that no LLM, nor any LLM run in a loop, will ever be as intelligent as a precocious child. The burden rests on OpenAI and the scholars on their payroll to show otherwise.

Have you considered that children, and people in general, may be very significantly less intelligent than your baseline assumption?

A flaw in the Turing test is failing to specify which person is making the judgement. We're working with statistical distributions here and I would not bet on the intellect displayed by the LLM models being below that displayed by the human population today, let alone with more improvement to one or degradation to the other.

More concretely, if you sketch some normal distributions on a whiteboard for people vs machine based on how you see things, it should be hard to confidently claim minimal overlap.

Post reply on HN