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

91–100 of 106 posts

Re: Machine-Assisted Proof [pdf]

#91

Post by vouaobrasil »

_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 know that the Amish aren't against technology, but they are against most advanced forms. When it comes to power tools, they also engineer specific requirements so that the electricity they use can't be used for anything else. And when it comes to computers, a lot of them contract out the work so they don't have to be exposed to them.

When it comes to making decisions, I am pretty sure no one in modern society makes any choices when it comes to the net benefits, only the short-term gains. That's regardless of how much technical training they have. And the net benefits are mainly about the use, not how the thing works, so people could really indeed make such decisions if there were a governing body to do so.

Re: Machine-Assisted Proof [pdf]

#92

Post by vouaobrasil »

_yb2s wrote: post #71
vouaobrasil wrote: post #62

Earlier quoted context omitted.

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

> I am talking about being possible where we can make virtually anything directly from carbon in the air,

I really would like a citation for this, perhaps several. How do we make various metals from carbon from the air? How could we make the silicon for the solar panels? Lubricants for the wind turbines? Lithium for the batteries? Or will all batteries be made out of pure carbon?

Metal is required for industrial civilization. Even if it isn't, not everything could be made from just the gaseous elements in the air.

I really do love the idea that we COULD do that. If you're right, what I am doing is completely unnecessary. In that case, I will gladly accept that I am wrong.

But if I am right, then civilization will start to destabilize and we will have to give up advanced technology and I will also accept that and work towards making that a better future.

I may not be right all the time, and honestly, TRULY, hope that I am wrong....feel free to email of course if you ever want a deeper chat.

Re: Machine-Assisted Proof [pdf]

#93

Post by Syzygies »

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…

Our world is increasingly defined by software without correctness proofs. Our tools are too clumsy, and we're just not smart enough, so we accept this situation. AI-verified code could become one of the most economically important applications of machine learning, when we cross the threshold where this becomes feasible.

I'm a mathematician, and we struggle with the purpose of a proof: Is it to verify, or also to explain so we can generalize? Machine proofs tend to be inscrutable.

While "the singularity" is unlikely anytime soon, we should recall that before the first atomic test there were calculations to insure that we didn't ignite the atmosphere. We're going to need proofs that we have control of AI, and there's an obvious conflict of interest in trusting AI's say so here. We need to understand these proofs.

Re: Machine-Assisted Proof [pdf]

#94

Post by nextos »

Syzygies wrote: post #93
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…

Our world is increasingly defined by software without correctness proofs. Our tools are too clumsy, and we're just not smart enough, so we accept this situation. AI-verified code could become one of the most economically important applications of machine learning, when we cross the threshold where this becomes feasible. I'm a mathematician, and we struggle with the purpose of a proof: Is it to verify, or also to expl…

This is also my take on this. IMHO, LLMs + theorem provers have the potential to make formal methods cheap enough to use more widely.

And we should give more credit to the theorem prover part of the equation, which comes in part from old AI symbolic efforts.

Re: Machine-Assisted Proof [pdf]

#95

Post by gsf_emergency »

vouaobrasil wrote: post #92
_yb2s wrote: post #71

Earlier quoted context omitted.

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

> I am talking about being possible where we can make virtually anything directly from carbon in the air, I really would like a citation for this, perhaps several. How do we make various metals from carbon from the air? How could we make the silicon for the solar panels? Lubricants for the wind turbines? Lithium for the batteries? Or will all batteries be made out of pure carbon? Metal is required for industrial civi…

Hey, if you're for degrowth, demetallization, and not just defossilfuelization/depolymerization is the way to go.

Basically, replace most electricity with photonics, the rest with ionics. We have efficient ion-flow based computing and flying machines, don't we? (Birds & brains)

As for how to revamp the rest of the "irreplaceable" material culture not based on photosynthesis: What's in it for me to talk to you about this :)? How many years further have you seen than Grothendieck, since Fuller was not so visionary after all? (Including, how to fund actionable, scalable stuff, that's 30 years give or take 5)

(Note that there are siliceous, if not entirely silicon-based, lifeforms on earth. Diatoms, molluscs, etc, perhaps a significant amount of our low-end chips already come from them, through seasand? :)

Re: Machine-Assisted Proof [pdf]

#96

Post by _yb2s »

vouaobrasil wrote: post #92
_yb2s wrote: post #71

Earlier quoted context omitted.

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

> I am talking about being possible where we can make virtually anything directly from carbon in the air, I really would like a citation for this, perhaps several. How do we make various metals from carbon from the air? How could we make the silicon for the solar panels? Lubricants for the wind turbines? Lithium for the batteries? Or will all batteries be made out of pure carbon? Metal is required for industrial civi…

Happy to provide citations, but I think more explanation is in order. The stuff we currently make from metals and petroleum are not optimal, they are just whatever we could easily make from those things we could find historically.

With precise, programmable control over biochemistry, we can make almost any organic carbon based molecule from almost any other carbon source- but obviously not things like metals. However, I posit we will be able to make things with drastically superior performance that fills all of the same use cases. Consider for example that Dyneema - which is just simple straight saturated carbon chains- is already 15x the strength of steel on a weight basis. I'm talking about being able to predict the properties of a molecule ahead of time, and then make something with exactly the properties we want.

It would be quite shortsighted to make a more environmentally friendly way of making the exact same stuff when those things were limited by constraints that no longer apply and we have the potential for drastically superior materials (stronger, more durable, lower toxicity, more recyclable, etc.) for a specific problem- but it depends on what specific problem you are addressing.

Re: Machine-Assisted Proof [pdf]

#97

Post by gsf_emergency »

_yb2s wrote: post #96
vouaobrasil wrote: post #92

Earlier quoted context omitted.

> I am talking about being possible where we can make virtually anything directly from carbon in the air, I really would like a citation for this, perhaps several. How do we make various metals from carbon from the air? How could we make the silicon for the solar panels? Lubricants for the wind turbines? Lithium for the batteries? Or will all batteries be made out of pure carbon? Metal is required for industrial civi…

Happy to provide citations, but I think more explanation is in order. The stuff we currently make from metals and petroleum are not optimal, they are just whatever we could easily make from those things we could find historically. With precise, programmable control over biochemistry, we can make almost any organic carbon based molecule from almost any other carbon source- but obviously not things like metals. However…

As I imply below we should also be able to biosynth silicon-based stuff :)

FWIW I doubt we understand biology enough today to make biomanufacturing more efficient than conventional industrial processes, see the non sequitur of fungi based meat substitutes.

However, in the meantime, we can defo learn from bio to improve or even revolutionize our processes.

The other thing is: CO2 capture is also going to be far less feasible than increasing albedo, that's where we should focus our short term imagination. Don't lose hope for albedo increase to be biotech based, in the short term, though!

(Eat meat that shit little yet fart more like humans)

Re: Machine-Assisted Proof [pdf]

#98

Post by vessenes »

Syzygies wrote: post #93
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…

Our world is increasingly defined by software without correctness proofs. Our tools are too clumsy, and we're just not smart enough, so we accept this situation. AI-verified code could become one of the most economically important applications of machine learning, when we cross the threshold where this becomes feasible. I'm a mathematician, and we struggle with the purpose of a proof: Is it to verify, or also to expl…

Interesting thoughts, thanks. It seems to me a model trained to generate Lean could also be purposed to explain a large Lean proof, and that’s very interesting. So much of modern math is limited to extremely small cohorts.

None of that is dispositive inre provable safety, obviously.

Re: Machine-Assisted Proof [pdf]

#99

Post by _yb2s »

gsf_emergency wrote: post #97
_yb2s wrote: post #96

Earlier quoted context omitted.

Happy to provide citations, but I think more explanation is in order. The stuff we currently make from metals and petroleum are not optimal, they are just whatever we could easily make from those things we could find historically. With precise, programmable control over biochemistry, we can make almost any organic carbon based molecule from almost any other carbon source- but obviously not things like metals. However…

As I imply below we should also be able to biosynth silicon-based stuff :) FWIW I doubt we understand biology enough today to make biomanufacturing more efficient than conventional industrial processes, see the non sequitur of fungi based meat substitutes. However, in the meantime, we can defo learn from bio to improve or even revolutionize our processes. The other thing is: CO2 capture is also going to be far less f…

True, in addition to things like diatoms making silicon structures, magnetotactic bacteria make iron containing metallic structures to detect magnetic fields. It is in principle possible to both recycle and manufacture metal and silicon objects biologically with precise control over 3D structure... but a lot further off from making carbon based small molecules and polymers.
Post reply on HN