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

61–70 of 526 posts

Re: Formalizing Fermat's Last Theorem

#61

Post by lordnacho »

prometheus1992 wrote: post #50

Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?

This was my question as well. The way I understand it, it's like a compiler, it implements rules, in this case logic/math rules that tell you whether something follows from assumptions you've given it.

But how do you know you told it what you intended to tell it?

Re: Formalizing Fermat's Last Theorem

#62

Post by epgui »

hyperhello wrote: post #53
prometheus1992 wrote: post #50

Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?

The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled. Note to other users: don’t downvote this kind of comment, answer it.

Is Lean a DSL? I’d argue it’s a general purpose programming language that excels at proofs.

Re: Formalizing Fermat's Last Theorem

#63

Post by tossandthrow »

KaiserPister wrote: post #39

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

The proof system is relatively easy to verify.

I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code.

You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.

Re: Formalizing Fermat's Last Theorem

#66

Post by Jaxan »

KaiserPister wrote: post #39

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

This is a crucial point. There have been many bugs in Lean (and in other proof assistants for that matter). Proof assistants work well on human input, because it was created with a certain intent.

We simply don’t know what those 13M contain and whether it “makes sense” and doesn’t trigger Lean bugs. (There are “independent” lean verifiers, but historically they contained the same, or similar, bugs.)

Re: Formalizing Fermat's Last Theorem

#68

Post by tossandthrow »

prometheus1992 wrote: post #50

Can someone with more knowledge help me with this silly question in my head? >>Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems Did a human check the 13 million lines of code? How does QA'ing this type of work works?

No. No human checked it. But a type checker did. And that is much better.

Re: Formalizing Fermat's Last Theorem

#69

Post by epgui »

gowld wrote: post #15
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…

That's like saying the future of code is Assembler. Lean is not for humans.

Lean is for humans.

Re: Formalizing Fermat's Last Theorem

#70

Post by Jaxan »

tossandthrow wrote: post #63
KaiserPister wrote: post #39

13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?

The proof system is relatively easy to verify. I am not entirely sure about lean, but the core algebras for systems like lean are in the 100s of lines of code. You can likely convince yourself it is correct in a weekend or less - especially with an Ai to help you understand it.

Most systems i have seen are way beyond a 100 lines. And their GitHub repository contain many issues, often soundness bugs. (Granted, many get fixed very fast.)
Post reply on HN