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

61–70 of 140 posts

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

#61

Post by generationP »

xvilka wrote: post #7

Interesting choice of the proof assistant though - some specific parts of the Lean's core are not completely decidable, moreover the upcoming Lean 4 version is incompatible with many libraries and proofs written for Lean 3. See also the discussion[1] if the Coq is suitable for number theory as quotients are ubiquitous here. [1] https://github.com/coq/coq/issues/10871

As to decidability: I suspect you mean that Lean's foundations are non-constructive. I'd rather they weren't, but with what Peter Scholze is doing, I'd be surprised if the arguments could be made constructive within just a few years from their conception. This usually takes much longer (e.g., constructive proofs of the Quillen-Suslin theorem appeared in print just a few years ago).

About incompatibility: Last time I checked (some 3 or so years ago), Coq was not backwards compatible either, and libraries had to be ported manually with each update. Sadly, as this is the one greatest anti-feature that is currently putting me off proof assistants, but probably it needs some time, and the quickest way to get there is to maximize usage. From what I know about Coq and Lean, I suspect Lean will stabilize faster than Coq does, due to it being more "declarative" (Coq is based too much on complex tactics, which are hard to make stable by design).

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

#62

Post by zozbot234 »

deadbeef57 wrote: post #25
xvilka wrote: post #13

Earlier quoted context omitted.

> You might be confused by the fact that Lean's definitional equality is not decidable, but that doesn't mean it isn't sound. Nobody has ever found a proof of `false` so far in Lean 3. You are right, my bad. Taking my words back on that. A bit more details from the Pierre-Marie Pédrot: > Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, t…

> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around. This is not the first time that I hear someone from the Coq community talk about Lean and its "mastermind PR campaign". To me it comes across in a denigrati…

The Coq folks tend to focus on constructivity, and Lean gets sold as a constructive system but then you get this weird axiomatised-quotients stuff that's the farthest thing from constructivity. I can see how they might find that kind of thing highly frustrating.

It might not show up as a problem if you only ever care about classical stuff, but there are arguably better ways of doing purely classical mathematics that don't arbitrarily break interoperability w/ the constructive world.

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

#63

Post by Tainnor »

zozbot234 wrote: post #59
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…

ZFC was only ever developed as a proof of concept, not as a practical foundation for formal math. Structural set theories, type theories or category-based foundations are actually a lot easier to work with, and otherwise quite equivalent in power.

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.

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

#64

Post by deadbeef57 »

zozbot234 wrote: post #62
deadbeef57 wrote: post #25

Earlier quoted context omitted.

> Lean does not escape this limitation, as it defines the equality type inductively as in Coq. Rather, in a mastermind PR campaign, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around. This is not the first time that I hear someone from the Coq community talk about Lean and its "mastermind PR campaign". To me it comes across in a denigrati…

The Coq folks tend to focus on constructivity, and Lean gets sold as a constructive system but then you get this weird axiomatised-quotients stuff that's the farthest thing from constructivity. I can see how they might find that kind of thing highly frustrating. It might not show up as a problem if you only ever care about classical stuff, but there are arguably better ways of doing purely classical mathematics that…

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

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

#65

Post by zozbot234 »

Tainnor wrote: post #63
zozbot234 wrote: post #59

Earlier quoted context omitted.

ZFC was only ever developed as a proof of concept, not as a practical foundation for formal math. Structural set theories, type theories or category-based foundations are actually a lot easier to work with, and otherwise quite equivalent in power.

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.

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

#66

Post by amelius »

sabujp wrote: post #23

"Proof assistants can’t read a maths textbook, they need continuous input from humans, and they can’t decide whether a mathematical statement is interesting or profound — only whether it is correct, Buzzard says. Still, computers might soon be able to point out consequences of the known facts that mathematicians had failed to notice, he adds." we're closer to this than people realize

> we're closer to this than people realize

At least give a proper reference to what you're alluding to, please.

Also, closeness in AI has shown to be a misleading concept.

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

#67

Post by deadbeef57 »

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 tedious parts of formalization, and I'm very glad that people are working hard on realizing this.

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

#68

Post by zozbot234 »

deadbeef57 wrote: post #64
zozbot234 wrote: post #62

Earlier quoted context omitted.

The Coq folks tend to focus on constructivity, and Lean gets sold as a constructive system but then you get this weird axiomatised-quotients stuff that's the farthest thing from constructivity. I can see how they might find that kind of thing highly frustrating. It might not show up as a problem if you only ever care about classical stuff, but there are arguably better ways of doing purely classical mathematics that…

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.

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

#69

Post by wolverine876 »

deadbeef57 wrote: post #55
wolverine876 wrote: post #54

Earlier quoted context omitted.

Thanks for sharing your expertise. Would you be open to sharing your background? Obviously it's not required, but it would help contextualize what you're saying for the interested non-mathematician; otherwise we're kinda stuck with 'some guy on the Internet said ...' syndrome. :)

Sure, I just created an account a couple of days ago, and my favourite username was already taken :oops: I'm Johan Commelin, https://math.commelin.net/

Thank you! And welcome! Make yourself at home.

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

#70

Post by foooobar »

zozbot234 wrote: post #57
kevinbuzzard wrote: post #36

Earlier quoted context omitted.

I agree, but I think my statement is accurate today in 2021. I would love to see funds directed towards this sort of question. The big problem is that at high level so so much is skipped over, and you still sometimes have to struggle to put undergraduate-level mathematics into Lean -- this is why UG maths is such a good test case.

> The big problem is that at high level so so much is skipped over This is an issue, but there's an established practice of writing formal sketches where the gaps in the proof are explicitly marked, and future tooling might bring ways to address these gaps once a full formal context is provided. One issue is that Lean has little or no support for declarative proof, which is by far the most natural setting for these "…

As far as I can tell, this is not quite true. Tactic proofs aside, you can also write functional term mode proofs and declarative "structured" proofs in the sense of Isar. Theorem Proving in Lean introduces that style, so most people who use Lean are familiar with it: E.g. https://leanprover.github.io/theorem_proving_in_lean/proposi...

Additionally, even in tactic proofs you can use tactics like `have`, `suffices`, etc. to manipulate the structure of the proof and make subgoals explicit like you would usually do in the structured style. In practice, people in Lean still prefer imperative tactic proofs with the option to write in a structured/declarative style where reasonable. The full "structured" mode does not see much use, since it is quite verbose. As a result, Lean 4 will not support this style out of the box anymore, but you could still add it yourself using the macro system.

Post reply on HN