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

391–400 of 537 posts

Re: Formalizing Fermat's Last Theorem

#391

Post by CaptWorld »

hcknwscommenter wrote: post #363
CaptWorld wrote: post #194

Earlier quoted context omitted.

Like? I feel breakthroughs that can be found via AI might help us more in the long term where even previously non AI fields can be helped by AI. So you have specific non AI research in mind that we're underinvesting in? Because the USA is already spending crazy anyway for healthcare and I don't feel like funding is the issue but better incentives, reforms etc

Funding for basic research is being slashed by the current administration. Our society is underinvesting in basic scientific research. And, AI will not fill the gap.

It's just because of this administration but future admins can revert it back and even then, i would expect the fund receivers themselves will eventually use AI so.

Re: Formalizing Fermat's Last Theorem

#392

Post by tonyedgecombe »

AmazingEveryDay wrote: post #246
martinpw wrote: post #231

Earlier quoted context omitted.

Looks like it is available here: https://www.dailymotion.com/video/x3wrbsb

Also: https://archive.org/details/BBCHorizonCollection512Episodes/...

Also https://www.bbc.co.uk/iplayer/episode/b0074rxx/horizon-19951... (if you are in the UK).

Re: Formalizing Fermat's Last Theorem

#393

Post by nutjob2 »

CyLith wrote: post #197
nutjob2 wrote: post #101

Earlier quoted context omitted.

Most people want more life. For most people it's also the most terrifying part of "the natural human experience". If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?

Because living longer is a huge drain on resources that could be better spent on other things. End of life care is expensive and rarely results in a "good" life for the the life being extended.

> End of life care is expensive

Only in places like the US, which is out of its mind in this regard.

In most other western countries, they just let (old) people with terminal conditions die.

> living longer is a huge drain on resources that could be better spent on other things

That's not right. Any living is a drain on resources and draining resources is the issue not the living. More broadly we need to use less resources or manage them better and there are much better ways in doing that than reducing life.

Re: Formalizing Fermat's Last Theorem

#394

Post by nutjob2 »

defrost wrote: post #358
s7atic wrote: post #354

Earlier quoted context omitted.

Fertility rates are below replacement, which means that population sizes are convergent. A decreasing population is a more likely future scenario for many western countries, even if human lifespan was indefinite.

Fertility rates are currently below replacement, there's no good reason to imagine they will always be that way, particularly after global population numbers peak and fall to, say, half or a quarter of their peak.

What's the basis for your claim? You seem to be saying that people are magically going to have more children because there is a desperate need for them? Maybe if government finances this but how will that work economically at such a huge scale? Will children be born in debt for their birth?

Re: Formalizing Fermat's Last Theorem

#395

Post by NooneAtAll3 »

vlovich123 wrote: post #159
zamadatix wrote: post #137

Earlier quoted context omitted.

While pretty much everyone is certain Fermat was mistaken in believing he had a valid proof for the theorem, this is an expanded (compared to proof presentations) version of one proof - not the shortest presentation of the shortest valid proof.

Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin. My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.

> Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin.

https://xkcd.com/1381/

Re: Formalizing Fermat's Last Theorem

#396

Post by nutjob2 »

tinfoilhatter wrote: post #107
nutjob2 wrote: post #101

Earlier quoted context omitted.

Most people want more life. For most people it's also the most terrifying part of "the natural human experience". If you're happy to die, why be bothered by others' trying to live longer? You won't be around. And assuming people can finance it themselves, is it really a problem for society?

I assume you mean that dying is the most terrifying pat of the natural human experience. Also, I'm not sure why you infer that me thinking death is a natural part of life, means that I'm happy or eager to die. There are many reasons that people living forever would be a problem for society, the most obvious being an ever-increasing population.

> I'm not sure why you infer...

Your post was vague and emotive, I did my best.

Also things like chronic disease and violence are a "natural" part of life but we seek to minimize or eliminate them, why do we have to accept a "natural" death and not attempt to put it off as long as possible?

> the most obvious being an ever-increasing population

This notion seems to be commonly accepted as bad without being properly examined.

Why is a larger population in and of itself a problem? Lots of societies throughout history have used less resources than we have and we have superior tech now. We are well within our abilities to use the same or less resources with a much larger population. Why should there be a limit based solely on undefined notions of "too many"?

Re: Formalizing Fermat's Last Theorem

#397

Post by beng-nl »

salomonk_mur wrote: post #132
t_gamer_kle wrote: post #124

Earlier quoted context omitted.

Forgive the authors of the article for assuming readers would complete it.

For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side. Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?

I think this is a Fermat joke :-)

Re: Formalizing Fermat's Last Theorem

#399

Post by eproxus »

2muchcoffeeman wrote: post #253
_aavaa_ wrote: post #102

Earlier quoted context omitted.

Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.

The token price seems like a poor measure. Building the LLM that could do this work in 11 days cost multi billions. The economics probably only make sense if LLMs prove to be a benefit to almost everyone in a way we can all accept. Otherwise this cost a lot more than we’d otherwise pay. It was incredibly fast though. But we all know: cost, speed, quality. Pick two.

This the correct way to look at it. Just as the person spending 5 years working on this will have learnt many things which will be useful after this problem is solved, you have to factor in the training cost (sure it's only done "once", but that is the same for the person too once they jump on the next problem).

The model wouldn't not be able to solve this without all the training leading up to the actual execution, so counting only the tokens of the execution doesn't give the full picture.

Re: Formalizing Fermat's Last Theorem

#400

Post by derkha »

jmusall wrote: post #204
Smaug123 wrote: post #110

Earlier quoted context omitted.

It is possible, although the post notes that the proof was also verified by the Comparator, which means any exploited bug has to also be present in that checker. Which is not unheard of, but is much less likely than merely an exploit in Lean 4.

The comparator was only used to verify that the final statement indeed is a valid formalization of Fermat's Last Theorem, not that the proof leading up to it is correct.

No, comparator does check the entire closure
Post reply on HN