Machine-Assisted Proof [pdf] • Hacker News Board

Re: Machine-Assisted Proof [pdf]

#81

Post by akoboldfrying » Sat, Dec 28, 2024, 1:03 PM UTC

vouaobrasil wrote: post #68

akoboldfrying wrote: post #65

Earlier quoted context omitted.

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

I think we agree that technology is not inherently a force for good. But I take your original claim to be that it is exclusively a force for (environmental) evil, which I think is demonstrably untrue. Although you have now added an exception for "primitive" forms, it's not clear to me (a) that these are any better for the environment than "advanced" forms (fire can be pretty bad for the environment) or (b) where the line between "primitive" and "advanced" is in any case.

Re: Machine-Assisted Proof [pdf]

#82

Post by _yb2s » Sat, Dec 28, 2024, 1:30 PM UTC

vouaobrasil wrote: post #68

akoboldfrying wrote: post #65

Earlier quoted context omitted.

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

I really like the Amish approach to technology, but don't think most people are aware of the nuance: they aren't against technology, but critically evaluate the net benefit, and adopt it if it seems like a benefit to them, not just because they can. Plenty of Amish use modern technology when they feel it is appropriate- a lot of them are running businesses that require computers, power tools, and high speed travel to make a living - I see them on Amtrak frequently.

However, I do wonder if they are still able to make coherent decisions about the net benefits of various technologies, without a deep level of technical and scientific training nowadays. Living up against a world of people not making the same choices as them would present a lot of new challenges- for example, if a chemical factory is placed nearby... are they learning how to use mass spec to see if they are being poisoned? Or to read scientific literature to see what the likely risks and impacts of that poisoning is? Sure they could hire external experts, but can they trust people that don't share their views and values to navigate those issues as they would?

Taking personal responsibility for if a technology is appropriate to use or not may require an even deeper level of technical and scientific knowledge than the usual approach of not being critical of technology.

Re: Machine-Assisted Proof [pdf]

#83

Post by api » Sat, Dec 28, 2024, 1:35 PM UTC

_yb2s wrote: post #82

vouaobrasil wrote: post #68

Earlier quoted context omitted.

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

I really like the Amish approach to technology, but don't think most people are aware of the nuance: they aren't against technology, but critically evaluate the net benefit, and adopt it if it seems like a benefit to them, not just because they can. Plenty of Amish use modern technology when they feel it is appropriate- a lot of them are running businesses that require computers, power tools, and high speed travel to…

I’ve always thought that super advanced aliens would be like this.

Sure they can fold space-time and have quantum computers the size of dust particles, but they also use traditional tools from their ancient history when appropriate or when it serves a role in their culture. They also don’t do absolutely everything they know how to do, deciding some things are harmful or useless.

You see this sometimes in sci-fi, e.g. Star Trek.

It’d probably be a sign of being advanced far beyond the hype phase, even having gone through many hype - disillusionment - enlightenment phases. They would be far post the phase where things look like cyberpunk, but you’d probably see phases like that in their history.

Re: Machine-Assisted Proof [pdf]

#84

Post by wwweston » Sat, Dec 28, 2024, 1:44 PM UTC

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…

One of Bill Thurston's answers on MathOverflow should be required reading on this and a lot of related topics. When basically asked "How do I cope with the fact that I'm no Gauss or Euler?" he replied:

> The product of mathematics is clarity and understanding. Not theorems, by themselves... mathematics only exists in a living community of mathematicians that spreads understanding and breaths life into ideas both old and new. The real satisfaction from mathematics is in learning from others and sharing with others. All of us have clear understanding of a few things and murky concepts of many more. There is no way to run out of ideas in need of clarification. The question of who is the first person to ever set foot on some square meter of land is really secondary. Revolutionary change does matter, but revolutions are few, and they are not self-sustaining --- they depend very heavily on the community of mathematicians.

https://mathoverflow.net/questions/43690/whats-a-mathematici...

Ongoing relationships and cooperation is how humanity does its peak stuff and reaches peak understanding (and how humans usually find the most personal satisfaction).

LLMs are powerful precisely because they're a technology for concentrating and amplifying some aspects of cooperative information sharing. But we also sometimes let our tools isolate.

Something as simple as a map of a library is an interesting case: it is a form of toolified cooperation, you can use it to orient yourself in discovering and orienting library materials without having to talk to a librarian, which saves time/attention... and also reduces social surface area for incidental connection and cooperation.

That's a mild example with very mild consequences and only needs mild individual or cultural tools in order to address the tradeoffs. We might also consider markets and the social technology of business which have resorted in a kind of target-maximizing AGI. The effects here are also mixed, certainly in terms of connection / isolation, also potentially in terms of environmental impact. A paperclip maximizer has nothing on an AGI/business that benefits from mass deforestation, and we created that kind of thing hundreds of years ago.

The question is if we're going to maintain the kind of social/cultural infrastructure that could help us be aware of and continue to invest in the value the social/cultural infrastructure.

Or, put more simply, if we're going to build a future for people.

Re: Machine-Assisted Proof [pdf]

#85

Post by sylware » Sat, Dec 28, 2024, 2:36 PM UTC

LLM is probably not the right model for AIs strapped to a formal solver. But experience which has been gained with LLMs may help design those maths oriented models.

Re: Machine-Assisted Proof [pdf]

#86

Post by xaml » Sat, Dec 28, 2024, 2:51 PM UTC

voxl wrote: post #5

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…

LLMs as they are I postulate would not work well for this. But, purpose built stochastic auto complete with a type checker to reject the junk? That could be actually useful. Funnily enough it's also a domain of application that wouldn't make any money at all. It would have to be an offline LLM that is reasonably efficient to execute locally.

Why would it not make any money?

Re: Machine-Assisted Proof [pdf]

#87

Post by 4ad » Sat, Dec 28, 2024, 2:58 PM UTC

benreesman wrote: post #12

aamar wrote: 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.

Even without a definition of intelligence, this is not what the paper is about, which only mentions LLMs in passing. And LLMs can be useful even if they are wrong, because formal verification (though Lean and such) checks the result.

Are LLMs useful enough? I don't know.

Re: Machine-Assisted Proof [pdf]

#88

Post by _yb2s » Sat, Dec 28, 2024, 3:35 PM UTC

akoboldfrying wrote: post #81

vouaobrasil wrote: post #68

Earlier quoted context omitted.

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

I think we agree that technology is not inherently a force for good. But I take your original claim to be that it is exclusively a force for (environmental) evil, which I think is demonstrably untrue. Although you have now added an exception for "primitive" forms, it's not clear to me (a) that these are any better for the environment than "advanced" forms (fire can be pretty bad for the environment) or (b) where the…

A lot of people I think mistakenly assume technology, capitalism, etc. are fundamentally evil because they’ve been used to do awful things… but they are just amoral powerful tools. One needs to have a sense of ethics, quality, and responsibility to make good decisions in their use. Deeper basic scientific knowledge also allows for more accurate predictions of the consequences and risks- enabling more responsible actions.

Re: Machine-Assisted Proof [pdf]

#89

Post by vouaobrasil » Sat, Dec 28, 2024, 5:15 PM UTC

_yb2s wrote: post #88

akoboldfrying wrote: post #81

Earlier quoted context omitted.

I think we agree that technology is not inherently a force for good. But I take your original claim to be that it is exclusively a force for (environmental) evil, which I think is demonstrably untrue. Although you have now added an exception for "primitive" forms, it's not clear to me (a) that these are any better for the environment than "advanced" forms (fire can be pretty bad for the environment) or (b) where the…

A lot of people I think mistakenly assume technology, capitalism, etc. are fundamentally evil because they’ve been used to do awful things… but they are just amoral powerful tools. One needs to have a sense of ethics, quality, and responsibility to make good decisions in their use. Deeper basic scientific knowledge also allows for more accurate predictions of the consequences and risks- enabling more responsible acti…

I don't thin it is good or evil but neither do I subscribe to the instrumentalist view that it is a tool. It does grow with a deterministic force that is partly beyond human control. (Various mechanisms make it so in a large populace). So, I don't agree that it's "just a tool" either.

Re: Machine-Assisted Proof [pdf]

#90

Post by vouaobrasil » Sat, Dec 28, 2024, 5:17 PM UTC

akoboldfrying wrote: post #78

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…

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.

Oh come on, that's ridiculous. I wasn't referring to a change in ability, but a change in culture. The modern culture of mathematics is getting worse in my opinion, and many feel the same. Besides, I don't even practice math any more...