Live data from Hacker News

Machine-Assisted Proof [pdf]

ams.org

101–106 of 106 posts

Re: Machine-Assisted Proof [pdf]

#101
I know this guy is Fields medalist, but all his recent posts and now this publication lack any substance and actual contributions, so it sounds like he is more in the role of hyped twitter influencer than researcher.

Re: Machine-Assisted Proof [pdf]

#102
post #99

Earlier quoted context omitted.

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.

Pedantry: I love that HN has at least one person who's attempted to culture magnetotactics: https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...

Re: Machine-Assisted Proof [pdf]

#103
post #99

Earlier quoted context omitted.

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.

Pedantry: I love that HN has at least one person who's attempted to culture magnetotactics: https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...

Haha. Pedantry for future diyrs

You can start easier today (thanks thoughtful USian industry!) from, otc https://www.himedialabs.com/us/m643a-mineral-modified-glutam...

Following, e.g. (thanks academia!) https://www.researchgate.net/publication/46007644_Enhancemen...

Also note they are better thought of as anaerobic.

Also diyrs, if you're to wean off the Man, keep detailed notes (or at least back up your pdfs on tape)!

Source: have tried basic MSGM "at home" for easier anaerobes, reasonably successful

Found this, also seems diyable, not chips, but li batt anodes from beachsand (thanks the lowest end of springer-demia!) https://www.nature.com/articles/srep05623

Re: Machine-Assisted Proof [pdf]

#104

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…

> Using advanced AI in math is a mistake in my opinion.

I too feel saddened by the idea of automating math if it leads to inscrutable proofs or theories. But it seems essential that we advance the tools used for mathematical discovery if we hope to keep advancing. Hopefully we can find a balance where the advancement of mathematical understanding continues to be a human story, but we're not artificially held back by pretending new tools don't exist.

Re: Machine-Assisted Proof [pdf]

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

A good thing about machine proofs is that, just like code, they can be refactored. I also use LLMs when writing code, but the code that I end up pushing is almost never exactly what the LLM has generated. I don't really see the problem with that. It's way less taxing for me mentally to get an LLM to generate definition and implementations and just refactor them quickly. I would expect LLMs for lean to be similar in the future.

Re: Machine-Assisted Proof [pdf]

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

You think people in the hunter gatherer days lived a better more humane life? You walked too close to a branch and got a small cut and a few weeks later you are dead. Oh no, You fell and can't get up while a predator is chasing your group, better prepare to be eaten alive. You accidentally ate that one fruit that looks similar to another one, oops you die shitting your bowels out. What's that? You are getting your third child, too bad the other two died in child birth together with their mother.

I really don't think you realize how cushy modern life is compared to even the hardships of a few hundreds years ago.

Post reply on HN