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

Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

nature.com

Post reply on HN
Print view View original

71–80 of 140 posts

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#71

Post by deadbeef57 »

zozbot234 wrote: post #68
deadbeef57 wrote: post #64

Earlier quoted context omitted.

Where does Lean get sold as a constructive system? Certainly mathlib (the main maths library in Lean) is very upfront about being classical.

mathlib != Lean. I'm talking about the basic logic. People will try to sell you Lean by describing its system as constructive, but if so the quotients stuff is pure breakage as the Coq folks point out. And if Lean could support classical logic without arbitrarily breaking interop for folks who want to also prove constructive statements, we might see some additions to mathlib with a closer focus on constructive math.

I agree very much that mathlib != Lean. Still, I think much of the talk about Lean will mention that mathlib is classical.

It was an honest question: I don't know where Lean is sold as a constructive system. (Note, I haven't read every part of Lean's documentation or website. I might be missing something obvious here.)

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#72

Post by foooobar »

zozbot234 wrote: post #68
deadbeef57 wrote: post #64

Earlier quoted context omitted.

Where does Lean get sold as a constructive system? Certainly mathlib (the main maths library in Lean) is very upfront about being classical.

mathlib != Lean. I'm talking about the basic logic. People will try to sell you Lean by describing its system as constructive, but if so the quotients stuff is pure breakage as the Coq folks point out. And if Lean could support classical logic without arbitrarily breaking interop for folks who want to also prove constructive statements, we might see some additions to mathlib with a closer focus on constructive math.

I don't think anyone is trying to sell Lean as a constructive system. The current developers certainly don't think of it that way, further evidenced by the fact that the typical way of doing computation in Lean does not involve definitional reduction, but using `#eval` with additional low level code for performance. Proof irrelevance (and quotients) were adopted with that in mind.

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#73

Post by Someody42 »

zozbot234 wrote: post #68
deadbeef57 wrote: post #64

Earlier quoted context omitted.

Where does Lean get sold as a constructive system? Certainly mathlib (the main maths library in Lean) is very upfront about being classical.

mathlib != Lean. I'm talking about the basic logic. People will try to sell you Lean by describing its system as constructive, but if so the quotients stuff is pure breakage as the Coq folks point out. And if Lean could support classical logic without arbitrarily breaking interop for folks who want to also prove constructive statements, we might see some additions to mathlib with a closer focus on constructive math.

You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#75

Post by foooobar »

Someody42 wrote: post #73
zozbot234 wrote: post #68

Earlier quoted context omitted.

mathlib != Lean. I'm talking about the basic logic. People will try to sell you Lean by describing its system as constructive, but if so the quotients stuff is pure breakage as the Coq folks point out. And if Lean could support classical logic without arbitrarily breaking interop for folks who want to also prove constructive statements, we might see some additions to mathlib with a closer focus on constructive math.

You can absolutely do constructive things in Lean, as long as you use neither the built-in "quot" type nor the three other axioms described in the docs, and then you get a system with all the desired properties I think

Some constructivists may also take offense with proof irrelevance (and the resulting loss of normalization [1] or its incompatibility with HoTT), which you can only really avoid by avoiding Prop.

[1] https://arxiv.org/abs/1911.08174

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#76

Post by foooobar »

mjreacher wrote: post #74

Is there any opportunity for interested undergrads to learn about this more (since I doubt we could contribute)?

If you're interested in interactive theorem proving with Lean (and not condensed mathematics), the Lean community landing page is a good place to start. https://leanprover-community.github.io/

Especially the "Natural Number Game" under "Learning resources" has been successful in teaching folks the very basics for writing proofs. Once finished, a textbook like "Theorem Proving in Lean" can teach the full basics. Feel free to join the Lean Zulip at any point and ask questions at https://leanprover.zulipchat.com/ in the #new members stream.

Mathlib has plenty of contributions from interested undergrads :)

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#77

Post by GPerson »

kevinbuzzard wrote: post #39
GPerson wrote: post #32

Earlier quoted context omitted.

Why do you say this?

I'm not quite sure what you're asking about. I'm saying that we can't yet take the Wiles and Taylor-Wiles proof of Fermat's Last Theorem, feed it into a machine, and get a Lean proof of Fermat's Last Theorem.

Hi Kevin,

Yes, I was responding to the person who said “we're closer to this than people realize” hoping to learn what they had in mind.

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#78

Post by Tainnor »

zozbot234 wrote: post #65
Tainnor wrote: post #63

Earlier quoted context omitted.

This is missing the point. Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. It requires a lot of effort to reformulate all of mathematics into equivalent formulations. That makes it harder to get buy-in from many working mathematicians, and it also makes the subject less approachable for, say, undergraduates.

Modern math textbooks are based on naïve set theory, which can be quite feasibly modeled, even by structural foundations. It might require some effort at the lowest layer of formalization, but even then only as a one-time thing that's not going to impact the project as a whole.

That may very well be the case, but to a person starting out right now, those foundations seem to be lacking right now (or at least are not easily discoverable).

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#79

Post by ganzuul »

deadbeef57 wrote: post #67
Tainnor wrote: post #45

This is going to be an exciting area. I spent some time previously playing with Coq. It's very powerful, but even proving the simplest undergraduate maths statements (say, about group theory) can prove very challenging. I believe that part of this is that Coq uses different mathematical foundations than traditional mathematics, which mostly uses set theory (ZFC, although most people don't care about the specifics). S…

In my experience, the difficulty is very rarely the transition from set theory to type theory. I find this almost transparent in practice. The issue is rather that you need to deal with edge cases that are usually swept under the rug, or that you need to spend a full page working out the details of a proof that everyone recognizes as obvious. It would be great if computers could give even more assistance with these t…

Kurt Gödel with a bat in dark alleyway of obviousness haunts my dreams.

Re: Mathematicians welcome computer-assisted proof in ‘grand unification’ theory

#80

Post by ixaxaar »

Tainnor wrote: post #45

This is going to be an exciting area. I spent some time previously playing with Coq. It's very powerful, but even proving the simplest undergraduate maths statements (say, about group theory) can prove very challenging. I believe that part of this is that Coq uses different mathematical foundations than traditional mathematics, which mostly uses set theory (ZFC, although most people don't care about the specifics). S…

Hey type hacking is hard. Agda is kinda easier for someone who knows haskell, but hard nonetheless.
Post reply on HN