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

291–300 of 526 posts

Re: Formalizing Fermat's Last Theorem

#291

Post by andriy_koval »

Almondsetat wrote: post #287
andriy_koval wrote: post #272

Earlier quoted context omitted.

you are entitled to have your opinion :-)

and you are entitled to talk about maths while rejecting maths

coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants.

I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory. Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another.

ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it. Additionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.

Re: Formalizing Fermat's Last Theorem

#293

Post by p-e-w »

bryanlarsen wrote: post #192
mbesto wrote: post #163

Earlier quoted context omitted.

> healthy profit margin (as near as we can tell from the outside) Ugh we still don't know if this is true and it's nearly impossible to calculate without a full understanding of the real CAPEX cycle. Stop spreading these rumors until we know for sure.

SemiAnalysis estimates their profit margin to be 70%. To be losing money on inference implies that their costs are almost 4X higher than SemiAnalysis has calculated. That's not credible.

I don’t see how they could credibly estimate inference costs without knowing the model size.

Re: Formalizing Fermat's Last Theorem

#294

Post by newAccount2025 »

m_w_ wrote: post #7

> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.

It’s common for formal proof efforts about software and hardware to involve thousands to tens of thousands of small lemmas.

13M lines does seem extreme and there is probably a lot of inefficiency given the way the proof was developed. Cutting it down is probably a long road, but is also a very well defined problem that AIs can probably just go do with enough time and budget now.

Re: Formalizing Fermat's Last Theorem

#295

Post by mietek »

lanstin wrote: post #258
ajs1998 wrote: post #140

Earlier quoted context omitted.

ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.

Reply to sibling - lean4 doesn't rest on ZF or ZFC. https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Co... However I believe an equivalence of power has been shown between the two.

Roughly, yes. See B. Werner (1997) “Sets in types, types in sets”.

Re: Formalizing Fermat's Last Theorem

#296

Post by mietek »

slowin wrote: post #219
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?

There are cultures where dying isn't feared like it is in Christian based societies. It's considered a natural progression and part of nature. I'd also say people may want more life for themselves, but what does that mean at scale, forever?

There is a lot of space in, you know, space, for people who live long enough to travel.

Re: Formalizing Fermat's Last Theorem

#297

Post by sanxiyn »

logicallee wrote: post #266

amazing, it's a huge achievement. can someone clarify, where the writeup says "The finished proof was checked by Lean; it uses just Lean’s three standard axioms" what does this mean? Aren't there a large set of standard axioms that are also necessary? (i.e. ZFC+)? if not, since it's only three axioms, can someone say what they were?

Lean's three standard axioms are documented in The Lean Language Reference.

https://lean-lang.org/doc/reference/latest/Axioms/#standard-...

The axiom of choice: axiom Classical.choice {α : Sort u} : Nonempty α → α

The axiom of propositional extensionality: axiom propext {a b : Prop} : (a ↔ b) → a = b

The quotient axiom: axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Eq (Quot.mk r a) (Quot.mk r b)

Re: Formalizing Fermat's Last Theorem

#299

Post by beepbooptheory »

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?

Feel very grateful I was never taught this... Would have missed out on quite a lot of good bodies of text in my life I think! Pushing through any initial friction or ignorance I might have as a reader, having the patience and charity to bear with an author until you get it, was instead what I was always taught.

Giving such a blanket "responsibility" to the author at all is just such a bummer! I say let them do whatever they want, there is always more than one way to express oneself. Someone who was never taught to write a clear thesis in the first paragraph for whatever reason doesn't inherently have less to say.

Re: Formalizing Fermat's Last Theorem

#300

Post by UltraSane »

glimshe wrote: post #205

"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…

advanced math like this takes 10 years to learn all the tower of things it is based on.
Post reply on HN