Mathematicians welcome computer-assisted proof in ‘grand unification’ theory • Hacker News Board

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

#11

Post by deadbeef57 » Sat, Jun 19, 2021, 4:00 PM UTC

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

The claim that Lean's core is not completely sound is FUD. Completely bogus.

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.

The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substantial user base of mathematicians somewhat familiar with the subject at hand (i.e., condensed mathematics).

The initial challenge by Peter Scholze was directed at all theorem proving communities. As far as I know, only the Lean community took up the challenge.

(Concerning Lean 4: yes, mathlib will have to be ported. And yes, people are working hard on this. I think that none of the theorem provers so far are ready for wide-scale use in mathematics. And that's why it is important to iterate fast. The Lean community is not afraid of redesigns and large refactors when discovering better approaches.)

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

#12

Post by deadbeef57 » Sat, Jun 19, 2021, 4:08 PM UTC

lvh wrote: post #3

I recommend the following post, by the author of the proof, for deeper context. Especially near the end, they talk about some of the things they're trying to accomplish with it in plain(ish) English. https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-e...

See also [1] for a follow-up blogpost that is less technical.

[1]: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...

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

#13

Post by xvilka » Sat, Jun 19, 2021, 4:09 PM UTC

deadbeef57 wrote: post #11

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

The claim that Lean's core is not completely sound is FUD. Completely bogus. 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. The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substanti…

> 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, they successfully convinced non-experts of type theory that they could give them quotient types without breaking everything around.

> The first thing they do is to axiomatize quotient types, which is somewhat fine and can be done the same in Coq. As any use of axioms, this breaks canonicity, meaning your computations may get stuck on some opaque term. (While slightly cumbersome, axiomatizing quotients already solves 99,9% of the problems of the working mathematician).

> Now, were they do evil things that would make decent type theorists shake in terror, they add a definitional reduction rule over the quotient induction principle. We could do the same in the Coq kernel, but there is a very good reason not to do this. Namely, this definitional rule breaks subject reduction, which is a property deemed more important than loss of canonicity.

> In Lean, you can write a term t : A where t reduces to u, but u doesn't have type A (or equivalently may not typecheck at all). This is BAD for a flurry of reasons, mark my words. Reinstating it while keeping quotients requires an undecidable type checking algorithm, which is another can of worms you don't want to wander into. The same kind of trouble arises from similar Lean extensions like choice.

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

#14

Post by martincmartin » Sat, Jun 19, 2021, 4:12 PM UTC

ulber wrote: post #10

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

I wasn't aware of Lean not being sound and a quick search didn't come up with anything related to that. Could you link a source?

See other comment. It's sound but not decidable.

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

#15

Post by deadbeef57 » Sat, Jun 19, 2021, 4:15 PM UTC

xvilka wrote: post #13

deadbeef57 wrote: post #11

Earlier quoted context omitted.

The claim that Lean's core is not completely sound is FUD. Completely bogus. 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. The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substanti…

> 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…

Ok, no worries. I understand that from a theoretical point it's not so nice that defeq is not decidable. But frankly I don't care. Because in practice, I don't know of any example where someone was bitten by this. It only shows up in contrived examples. And even if you have some practical example where lean gets stuck on A = B, it will probably be very easy to find a C so that lean gets unstuck on A = C = B.

[Edit, this comment only replies to the first paragraph of parent. I wrote it before parent was edited.]

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

#16

Post by Barrin92 » Sat, Jun 19, 2021, 4:18 PM UTC

The abiltiy to automate proofs creates some interesting questions about the nature of mathematics. The article remined me of Erdos saying that you "don't need to believe in God, but you do need to believe in the book", 'the book' here being an imagined collection of mathematical proofs that are so simple, clear and beautiful that they immedieately stand out to any mathematician.

I don't mind proof assistants as a way to gain new insights into mathematics, but I worry that maths is drifting into a direction where it turns more into hermeneutics than actual mathematics. The automation of proofs isn't the only thing, I also was very scpetical about the whole process of Shinichi Mochizuki's proof of the abc conjecture.

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

#17

Post by kzrdude » Sat, Jun 19, 2021, 4:18 PM UTC

deadbeef57 wrote: post #11

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

The claim that Lean's core is not completely sound is FUD. Completely bogus. 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. The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substanti…

Shouldn't it be easy to automatically port theorems? If they are well defined there can't be ambiguity

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

#18

Post by deadbeef57 » Sat, Jun 19, 2021, 4:22 PM UTC

Barrin92 wrote: post #16

The abiltiy to automate proofs creates some interesting questions about the nature of mathematics. The article remined me of Erdos saying that you "don't need to believe in God, but you do need to believe in the book", 'the book' here being an imagined collection of mathematical proofs that are so simple, clear and beautiful that they immedieately stand out to any mathematician. I don't mind proof assistants as a way…

As explained in another comment, there is only very mild proof automation going on in this Lean project. Every non-trivial idea has to be supplied to the computer by a human being.

The whole circus around Mochizuki's proof of the abc conjecture was dealt with quite well by the social structure of the mathematical community. Many people looked at the proof. Many people got stuck. Several experts got stuck at exactly the same point. And Mochizuki refuses to acknowledge that there is a problem at that point of his "proof". But a consensus was reached in the mathematical community (maybe minus RIMS).

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

#19

Post by deadbeef57 » Sat, Jun 19, 2021, 4:26 PM UTC

kzrdude wrote: post #17

deadbeef57 wrote: post #11

Earlier quoted context omitted.

The claim that Lean's core is not completely sound is FUD. Completely bogus. 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. The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substanti…

Shouldn't it be easy to automatically port theorems? If they are well defined there can't be ambiguity

Yes and no. If you want to port large low-level proof objects in all their gory detail, then this has been done already. But if you want to port the more concise higher-level proof scripts you run in all the same issues as with regular transpilers.

Compare it to porting machine code for one instruction set to another instruction set. This is usually doable in a straightforward manner (maybe with a mild performance penalty). But transpiling idiomatic Java to idiomatic Haskell is nigh impossible.

Luckily, the differences between Lean 3 and Lean 4 are not as large as between Java and Haskell. But still, they have different idioms, different syntax, different features. And this has to be taken care of.

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

#20

Post by Someody42 » Sat, Jun 19, 2021, 4:30 PM UTC

kzrdude wrote: post #17

deadbeef57 wrote: post #11

Earlier quoted context omitted.

The claim that Lean's core is not completely sound is FUD. Completely bogus. 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. The choice for Lean is actually quite natural: (i) it has a large and coherent library of mathematics to build such a project upon. And (ii), it has a substanti…

Shouldn't it be easy to automatically port theorems? If they are well defined there can't be ambiguity

In theory yes, but there are two main things that makes it harder :

- some technical details have changed. They don't affect the axiomatic aspects of Lean, but they force us to redefine some things in a cleaner way.

- we don't only want to port the theorem. We want to port them to a human-readable proof that can be easily maintained