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

41–50 of 106 posts

Re: Machine-Assisted Proof [pdf]

#41

Post by vouaobrasil »

_yb2s wrote: post #36
vouaobrasil wrote: post #29

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…

> 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 of safety, which hardly helps most anyway?

While you might be right, it is VERY far from clear that the latest advanced research will really help us. It could also lead to our annihilation or at least dehumanization, which is really not much better than annihilation.

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.

Re: Machine-Assisted Proof [pdf]

#42

Post by pepinator »

vouaobrasil wrote: post #29

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…

How is AI different from using a calculator? AI is just giving a new abstraction layer, in the same way that computers have done before AI. And these non-AI tools have allowed us to produce both deep research and beautiful theories. I'd be more worried about the problems related to a few companies concentrating all the tools and therefore the power.

Re: Machine-Assisted Proof [pdf]

#43

Post by imiric »

brap wrote: post #33
vouaobrasil wrote: post #29

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…

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.

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 are today, and their products likely won't power mission-critical infrastructure. Some might pursue it simply as a hobby and for the mental exercise.

It wouldn't be much different from small artisan shops we have today in other industries. Mass production will always be more profitable, but there's a market for products built on smaller scales with care and quality in mind. Large companies that leverage AI black boxes won't have that attention to detail.

Re: Machine-Assisted Proof [pdf]

#44

Post by gbnwl »

throwaway127467 wrote: post #37
jiggawatts wrote: post #34

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.

This is the fourth account you've made in the past hour just to comment on this post.

Re: Machine-Assisted Proof [pdf]

#45

Post by vouaobrasil »

zmgsabst wrote: post #40
vouaobrasil wrote: post #29

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…

Computers allow us to scale what we analyze in math — and that’s a good thing. Nobody examines structure of group diagrams because drawing interesting ones by hand is borderline impossible, but takes just a few minutes on a computer. However, they’re a natural way to arrive at algebraic/geometric equivalence. (And indeed, the first time I had an intuition for it.) To me, you sound like someone lamenting swimming is m…

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 situation when it comes to swimming: with swimming, people CHOOSE to swim because they like it. But due to different incentives, people will CHOOSE to use AI only because others use it and it will become the only path eventually.

In other words, swimming is still possible even though boats exist. People going into mathematics will not have the possibility of being of any use without AI, because the prisoner's dilemma (arms race) will ensure that math is no longer about anyone caring about math without AI.

Re: Machine-Assisted Proof [pdf]

#46

Post by zmgsabst »

vouaobrasil wrote: post #35
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.

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…

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

Re: Machine-Assisted Proof [pdf]

#47

Post by zmgsabst »

vouaobrasil wrote: post #45
zmgsabst wrote: post #40

Earlier quoted context omitted.

Computers allow us to scale what we analyze in math — and that’s a good thing. Nobody examines structure of group diagrams because drawing interesting ones by hand is borderline impossible, but takes just a few minutes on a computer. However, they’re a natural way to arrive at algebraic/geometric equivalence. (And indeed, the first time I had an intuition for it.) To me, you sound like someone lamenting swimming is m…

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 is. But we shouldn’t restrict the distance people can travel to adhere to the aesthetics of swimming.

You’re arguing precisely that: we must limit our intellectual journey because you don’t approve of the aesthetics of the tool to travel further.

Re: Machine-Assisted Proof [pdf]

#48

Post by vouaobrasil »

pepinator wrote: post #42
vouaobrasil wrote: post #29

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…

How is AI different from using a calculator? AI is just giving a new abstraction layer, in the same way that computers have done before AI. And these non-AI tools have allowed us to produce both deep research and beautiful theories. I'd be more worried about the problems related to a few companies concentrating all the tools and therefore the power.

AI is different because its ability to suggest creative lines of thinking will change the entire structure of how mathematics is done.

It's the same difference between "dumb" algorithms and "generative AI" algorithms. The generative AI has the capability to replace human thinking in some cases, whereas the dumb algorithms only replace rote work. Since creativity is not just what allows innovation but also forms the center of community and personal expression, we are also replacing those "soft" components of scentific exploration that eliminate the importance of the individual.

Re: Machine-Assisted Proof [pdf]

#49

Post by vouaobrasil »

imiric wrote: post #43
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.

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 problematic than everyone working too much.

Yes, a few people might find some meaning in a life where they are not that important, but most people need to feel important to others, and AI takes that away.

Re: Machine-Assisted Proof [pdf]

#50

Post by vouaobrasil »

zmgsabst wrote: post #46
vouaobrasil wrote: post #35

Earlier quoted context omitted.

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…

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?
Post reply on HN