Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Formalizing Fermat's Last Theorem

anthropic.com

Post reply on HN
Print view View original

41–50 of 525 posts

Re: Formalizing Fermat's Last Theorem

#41

Post by voxl »

lseplot wrote: post #10

https://github.com/anthropics/fermats-last-theorem/blob/main... status: "self-assessed" 13 million lines of Lean, where the Lean and Nanoda kernels missed the Collatz hack. Fable, please translate to HOL-light. Make no mistakes. You are doing great!

It's a great comedy that we move the buck from "I don't trust the human proof" to "I don't trust the Lean proof" despite the level of trust dramatically increasing. Moving to HOL-light might be another modest increase in trust, but to pretend the implementation of HOL-light has never had bugs and it's kernel could never have a bug is hubris.

Re: Formalizing Fermat's Last Theorem

#42

Post by artifact_44 »

dakolli wrote: post #30
atleastoptimal wrote: post #18

It seems clear AI has the potential to perform any cognitive task at far greater speeds, reliability, and scale than any human. The question is whether it will be allowed to scale to that point, and what will happen to humans after this occurs.

You'll get mass poverty and violence which the owners of AI will qwell with AI surveillance and weapons. AI will be used to pit us against eachother and justify wars to keep us busy. Fun times ahead. Not sure why anyone is excited about this tech.

[dead]

Re: Formalizing Fermat's Last Theorem

#43

Post by refibrillator »

Proving FLT was such a profoundly emotional and spiritual experience for Andrew Wiles, it almost brought a tear to my eye:

https://news.ycombinator.com/item?id=49203626

It is truly saddening to think that machines will deprive us of this wonder and experience.

But truly exciting to dream about what lies beyond the limits of our biology.

Re: Formalizing Fermat's Last Theorem

#44

Post by bawolff »

refibrillator wrote: post #43

Proving FLT was such a profoundly emotional and spiritual experience for Andrew Wiles, it almost brought a tear to my eye: https://news.ycombinator.com/item?id=49203626 It is truly saddening to think that machines will deprive us of this wonder and experience. But truly exciting to dream about what lies beyond the limits of our biology.

Formalizing is not the same as discovering. There is still plenty of room for human ingenuity.

Re: Formalizing Fermat's Last Theorem

#45

Post by mannanj »

refibrillator wrote: post #43

Proving FLT was such a profoundly emotional and spiritual experience for Andrew Wiles, it almost brought a tear to my eye: https://news.ycombinator.com/item?id=49203626 It is truly saddening to think that machines will deprive us of this wonder and experience. But truly exciting to dream about what lies beyond the limits of our biology.

Makes me wonder, if we make a tradeoff for comfort and advancement from our biology's "limits" - and that tradeoff is spiritual fulfillment.

Seeing it hit across: the work we used to do outdoors, the sleep-wake-dark cycle we adhered to for millennia, and more

Re: Formalizing Fermat's Last Theorem

#48

Post by charlieyu1 »

estetlinus wrote: post #33
anony-123 wrote: post #29

So, what I am thinking is that, the AI generated numbers or tried to find numbers "a", "b" and "c" to check if aⁿ + bⁿ = cⁿ Can not we do it by code?

Sure, go on and try it ;)

I found a brilliant proof but there was not enough hard disk space to save the file :(

Re: Formalizing Fermat's Last Theorem

#49

Post by yesitcan »

dakolli wrote: post #30
atleastoptimal wrote: post #18

It seems clear AI has the potential to perform any cognitive task at far greater speeds, reliability, and scale than any human. The question is whether it will be allowed to scale to that point, and what will happen to humans after this occurs.

You'll get mass poverty and violence which the owners of AI will qwell with AI surveillance and weapons. AI will be used to pit us against eachother and justify wars to keep us busy. Fun times ahead. Not sure why anyone is excited about this tech.

So much doom and gloom on this site. Makes it almost not worth reading.
Post reply on HN