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

531–539 of 539 posts

Re: Formalizing Fermat's Last Theorem

#531

Post by rao-v »

voxl wrote: post #37
rao-v wrote: post #6

An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable. I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think…

Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.

I hear you but point me to one novel formalization right now that is not Lean. It’s really becoming a refacto standard. Which is lovely but terrible for pedegogy

Re: Formalizing Fermat's Last Theorem

#532

Post by voxl »

rao-v wrote: post #531
voxl wrote: post #37

Earlier quoted context omitted.

Hearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.

I hear you but point me to one novel formalization right now that is not Lean. It’s really becoming a refacto standard. Which is lovely but terrible for pedegogy

??? Look at any conference that publishes mechanized results? You'll see plenty of Isabelle, ACL2, Rocq, Agda. You exist in the pop science bubble. If Lean has done anything it's advertised itself well. It did a good job of that as far back as the Liquid Tensor Experiment, and it's pissed many people off in the community with it's marketing antics.

Re: Formalizing Fermat's Last Theorem

#533

Post by drdeca »

andriy_koval wrote: post #529
drdeca wrote: post #528

Earlier quoted context omitted.

ZFC

zfc is a bunch of axioms and not inference system. It is commonly assumed that it is built on top of some unspecified first order logic which commonly assumed to include bunch of inference rules. There is no ground truth in my understanding where this all is formally defined.

If you want to use “ZFC” to refer to the axioms without any rules of inference, I guess you can do that, but when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.

Re: Formalizing Fermat's Last Theorem

#534

Post by andriy_koval »

drdeca wrote: post #533
andriy_koval wrote: post #529

Earlier quoted context omitted.

zfc is a bunch of axioms and not inference system. It is commonly assumed that it is built on top of some unspecified first order logic which commonly assumed to include bunch of inference rules. There is no ground truth in my understanding where this all is formally defined.

If you want to use “ZFC” to refer to the axioms without any rules of inference, I guess you can do that, but when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.

> when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.

its bro-math. In formal math you need to be specific what inference system you use. There are many of them. Then you need to have formal proof that in that system you can derive concept of function and then think about question if it won't make paradoxes and contradictions with ZFC.

Re: Formalizing Fermat's Last Theorem

#535

Post by contubernio »

YeGoblynQueenne wrote: post #450
contubernio wrote: post #445

Earlier quoted context omitted.

As a mathematician not expert kn these things, yes it scans as reasonable, and yes it has me and most of my colleagues reconsidering what we do for a living.

Well, if I were a mathematician, what I'd be noodling about with right now is a way to model the number of failed attempts that AI companies must be making for every success they report. I guess you don't have to be a mathematician to do that sort of calculation, but I'm just proposing it as a way to lift mathematicians' spirits a bit. Also pay attention to the fact that every time a new model is released there's a s…

Nobody is in panic, but we are using these systems and seeing what are their capabilities and it's clear that their use has a big impact on the practice of mathematical research, probably far more impact than it has in other areas. Part of mathematics involves classifying structures - think of describing combinatorial objects - and this is a sort of game with which a well directed AI tool can be very effective. Part of mathematics involves being able to bring to bear on a problem a diversity of techniques, and AI is also very helpful in this regard.

The point is that people who spend their time classifying nilpotent Lie groups that admit structure X are out of work if they don't change their perspective. Maybe such problems were never really that interesting, although it was useful to have a group of people acting as human computers to work them out - but well used AI yields for such problems more complete and more reliable results - and so allows researchers to spend their time on other more interesting things. The problem for your run of the mill professional mathematician is that more interesting things are harder ...

Re: Formalizing Fermat's Last Theorem

#536

Post by jibal »

jibal wrote: post #315
andriy_koval wrote: post #261

Earlier quoted context omitted.

looks like we are in disagreement

That increases the likelihood that they are right. > support your point with explanation or be ignored :-) Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore. https://math.stackexchange.com/questions/1366560/why-does-g%... https://math.stackexchange.com/questions/1090437/how-to-prov.…

> imo, those two links are example of rather low quality weird math discussions, but you can keep your opinion

I've seen a lot of bad faith on this site, but none exceeding that.

Re: Formalizing Fermat's Last Theorem

#537

Post by jibal »

jasomill wrote: post #513
andriy_koval wrote: post #466

Earlier quoted context omitted.

Your third year notes from Cambridge has very low authority to me

Formally, a function f is a relation between sets A and B such that, for all x in A and u , v in B , f ( x ) = u and f ( x ) = v implies u = v . It's just a definition. Authority is, as the parent suggests, any introduction to set theory.

The guy's remarkable response makes clear that he's a clueless troll.

Re: Formalizing Fermat's Last Theorem

#539

Post by hn_throwaway_99 »

lalitmaganti wrote: post #3

I suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... Provides great context on this accomplishment, what it means but also doesn't mean.

Regarding "what it doesn't mean", when I read that I thought there would be some sort of limitation on what Claude could do in the realm of proof autoformalization, but that's not really true. All the "what it doesn't mean" stuff that Kevin mentions is basically just stuff that he thinks Anthropic won't get around to because it's not that important to them, but they certainly could if they desired:

> But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway).

What I'm saying is that if you thought there were still some scraps in this domain where humans still had some superior capabilities, that does not seem to be the case.

Post reply on HN