## Stream: general

### Topic: seminars

#### Nam (Apr 28 2020 at 00:46):

JetBrains Research is going to give a seminar about Arend this April 30. http://math.andrej.com/2020/04/28/every-theorem-prover/

#### Reid Barton (Apr 28 2020 at 01:31):

Thanks. I've been curious about Arend for a while, but haven't looked into it in detail yet.

#### Brandon Brown (Apr 28 2020 at 03:35):

Looks neat but wish it had unicode

#### Mario Carneiro (Apr 28 2020 at 04:30):

they have an unusual solution to the "to bundle or not to bundle" problem: anonymous extensions

#### Johan Commelin (Apr 28 2020 at 04:45):

Which I think looks really cool!

#### Mario Carneiro (Apr 28 2020 at 04:47):

they also have eta for structures which might be part of why this works

#### Reid Barton (Apr 28 2020 at 04:48):

I have a vague recollection of seeing a system which treated lambda and Pi as the same thing

#### Brandon Brown (Apr 28 2020 at 05:05):

"The logic of Arend is intuitionistic. This means that the law of excluded middle, the double negation elimination, and other classically valid principles are not provable in Arend." So one cannot use classical reasoning in Arend like you can in Lean?

#### Mario Carneiro (Apr 28 2020 at 05:22):

You can probably use classical reasoning in Arend the same as in lean, that is, you define it as an axiom and use it

#### Mario Carneiro (Apr 28 2020 at 05:22):

That said, Arend is clearly intended for HoTT applications so it's probably not suitable as a direct alternative to lean

#### Jannis Limperg (Apr 28 2020 at 15:43):

There was some confusion about time zones. New word from Andrej: the talk starts at 18:00 CEST (UTC+2). The linked announcement is already updated.

#### Rob Lewis (Apr 30 2020 at 15:57):

A reminder for anyone interested, this starts in a few minutes. I'm watching the beginning at least.

#### Brandon Brown (Apr 30 2020 at 17:47):

Anyone who attended the seminar want to share their impression of Arend?

#### Mario Carneiro (Apr 30 2020 at 17:52):

No trusted core took me by surprise

#### Mario Carneiro (Apr 30 2020 at 17:55):

from the theory side, there are a lot of features that are simply baked into the "kernel" when there is a reasonable argument that they could be formalized in principle, like subtyping on structures and cumulative universes, universes of h-levels, and omission of constructors for truncated pattern matching

#### Patrick Stevens (Apr 30 2020 at 17:55):

I liked the fact that it doesn't make you prove cases in a higher inductive type which are "obviously true because you're truncated already"

^^

#### Mario Carneiro (Apr 30 2020 at 17:56):

it's a cool feature, but not one I'm comfortable just assuming as axiomatic unless I have to

#### Mario Carneiro (Apr 30 2020 at 17:56):

In lean of course we have things like trunc.rec_on_subsingleton for this

#### Patrick Stevens (Apr 30 2020 at 17:57):

Pattern matching on equalities and having it unfold behind the scenes into J is neat, too - pretty sure Agda can't do that

#### Mario Carneiro (Apr 30 2020 at 17:57):

It doesn't unfold behind the scenes to J

it's axiomatic

#### Patrick Stevens (Apr 30 2020 at 17:58):

Oh, fair enough :P

#### Mario Carneiro (Apr 30 2020 at 17:59):

I think Agda does have something to do with pattern matching on equality, indeed I thought that was how they did all their indexed inductive stuff

#### Mario Carneiro (Apr 30 2020 at 17:59):

(I also think that at least one soundness bug came from pattern matching on rfl, so I'm not thrilled to know it's baked in to Arend)

#### Patrick Stevens (Apr 30 2020 at 18:03):

I was remembering https://github.com/agda/agda/issues/3551

#### Mario Carneiro (Apr 30 2020 at 18:11):

I think that regular Agda has pattern matching on rfl, but the --without-K extension disables it, and Cubical Agda needs that for consistency and haven't yet built a replacement that doesn't assume K

#### Mario Carneiro (Apr 30 2020 at 18:13):

since it's a long-standing feature request I suspect it's not trivial to do safely, and Arend's "let's just do it anyway" approach makes me apprehensive

#### Mario Carneiro (Apr 30 2020 at 18:15):

Really, I think Arend is competing with (cubical) Agda more than Coq/Lean

#### Reid Barton (Apr 30 2020 at 18:26):

Some of the non-HoTT-related features also look quite attractive though, particularly the Monoid Nat 0 stuff (I don't remember whether there was a name for this, but I guess we could call it some kind of auto-unbundling)

#### Mario Carneiro (Apr 30 2020 at 18:27):

that's the anonymous extensions I linked above

#### Mario Carneiro (Apr 30 2020 at 18:27):

not having a kernel really helps here - doing this in lean would be a nightmare

#### Mario Carneiro (Apr 30 2020 at 18:29):

I recall @Thales trying to implement something like this for his lean frontend, I forget what it was called

#### Mario Carneiro (Apr 30 2020 at 18:31):

I think keeping track of all the anonymous semi-structures is hard because you either have to pre-implement all 2^N of them or you generate them on the fly and have double import problems when they get autogenerated twice

#### Mario Carneiro (Apr 30 2020 at 18:34):

But it does underscore the point that bundling is only a problem because of the architecture of lean. If you build your system a different way it becomes a non-issue

#### Jannis Limperg (Apr 30 2020 at 19:19):

Mario Carneiro said:

I think that regular Agda has pattern matching on rfl, but the --without-K extension disables it, and Cubical Agda needs that for consistency and haven't yet built a replacement that doesn't assume K

Agda with --without-K has pattern matching on equalities, only with some mild additional restrictions compared to --with-K. Agda with --cubical, as far as I understand, has no pattern matching on path types. I don't know whether they have it for the separate 'cubical identity type', but they'd prefer you don't use that anyway.

#### Marc Huisinga (Apr 30 2020 at 20:59):

the arend talk has been uploaded: https://vimeo.com/413726748

#### Reid Barton (May 01 2020 at 11:51):

I think cumulative universes plus covariance in universe parameters also fixes the issue that you can't define isomorphisms of Rings as an instance of a general category-theoretic notion of isomorphism

#### Reid Barton (May 01 2020 at 11:51):

though I would have to play around with it to be sure

#### Valery Isaev (May 02 2020 at 12:08):

Hi everyone! Just found this thread. I want to address Mario's concern about the core. I mentioned in the talk that it is that large primarily because of efficiency considerations. I thought about implementing a smaller version of the core and a translator between them. It should be easy to eliminate some of the features (like insert missing clauses or replace p.m. with J). I think eliminating subtyping for classes might be a big problem for the efficiency though because every instance of a subclass should be recreated when it is passed to a function that expects the super class. This means that there will be several copies of the same expression and if the expression is large this will be a problem. I think there can be some exponential blow ups.

#### Valery Isaev (May 02 2020 at 12:11):

Mario Carneiro said:

they also have eta for structures which might be part of why this works

I think subtyping is also essential for this feature. Btw, did you mean lean doesn't have eta for structures?

Nope.

#### Johan Commelin (May 02 2020 at 12:15):

We have lots of cases X; cases Y; congr proofs.

#### Johan Commelin (May 02 2020 at 12:15):

And p is not defeq to (p.1, p.2).

#### Valery Isaev (May 02 2020 at 12:17):

What about eta for $\Pi$-types?

#### Johan Commelin (May 02 2020 at 12:20):

Hmm, I wouldn't know. I'm not an expert. But I think we have very little eta.

#### Johan Commelin (May 02 2020 at 12:21):

Wait, you mean f = \lambda x, f x?

We have that one

#### Valery Isaev (May 02 2020 at 12:22):

Johan Commelin said:

Wait, you mean f = \lambda x, f x?

Yes, this one.

#### Johan Commelin (May 02 2020 at 12:23):

Ok, that one is fine.

#### Kevin Buzzard (May 02 2020 at 12:25):

It's not defeq though, it's a theorem, right?

#### Kevin Buzzard (May 02 2020 at 12:25):

Like eta for structures is a theorem

#### Valery Isaev (May 02 2020 at 12:27):

If it's a theorem, then it's not eta.

#### Marc Huisinga (May 02 2020 at 12:28):

if i am reading mario's master thesis right, then eta is defeq

#### Marc Huisinga (May 02 2020 at 12:29):

there's an eta rule in 2.2

#### Chris Hughes (May 02 2020 at 12:34):

f = \la x, f x is a defeq. I'm not sure it would even be provable if it wasn't a defeq.

#### Johan Commelin (May 02 2020 at 12:35):

It's provable by funext and beta? (Misa very much out of comfort zone, now)

#### Valery Isaev (May 02 2020 at 12:35):

Chris Hughes said:

f = \la x, f x is a defeq. I'm not sure it would even be provable if it wasn't a defeq.

You can always add it as an axiom :)

#### Chris Hughes (May 02 2020 at 12:35):

You need it to prove funext I think.

#### Mario Carneiro (May 02 2020 at 14:17):

Hi @Valery Isaev . I agree that subtyping in the type theory is difficult to mimic if it has to be simulated. I'm okay with this, but it does require a proper handling in the metatheory - the difficulty of elimination indicates that it's more than just a sugaring step, and it significantly affects various critical theorems about the type theory (including in particular consistency).

#### Mario Carneiro (May 02 2020 at 14:22):

I think a moderate intermediate goal is to write down the type theory that you implement (in informal mathematics), including all features that are even moderately suspicious. Do you have an internal language of fully elaborated terms? If so those terms should map directly to the term language in the theory.

#### Valery Isaev (May 02 2020 at 14:27):

Mario Carneiro said:

Do you have an internal language of fully elaborated terms? If so those terms should map directly to the term language in the theory.

Yes, we do. It's definitely possible to write down all the details, it's just a lot of work and I don't really have time for that.

#### Kevin Buzzard (May 08 2020 at 14:13):

Emily Riehl is going to explain how to teach infinity categories to undergraduates in 15 minutes, if I understand UTC correctly (I mean she's going to explain in 15 minutes' time ;-) )

https://mathseminars.org/seminar/IsolatedInfinityCategories

#### Kenny Lau (May 08 2020 at 14:20):

The password for the zoom meeting is the surname of the person who coined the phrase "univalent foundations" in all lower case. You can read about the history of univalent foundations on Wikipedia.

#### Reid Barton (May 08 2020 at 14:31):

The first phrase of the main body of the talk is apparently "Dependent type theory" so it might be of extra interest to people here (of course it is going to be about homotopy type theory, but still)

#### Reid Barton (May 08 2020 at 15:22):

In the zoom chat: Kevin and Patrick hating on HoTT

#### Patrick Massot (May 08 2020 at 15:32):

Only because she keeps repeating "type theory" when she means "hott"

#### Jeremy Avigad (May 08 2020 at 15:47):

Here are the Simpson lectures she just referred to: https://www.msri.org/people/7306.

#### Reid Barton (May 08 2020 at 15:48):

I don't think she said anything specific to HoTT actually

#### Jeremy Avigad (May 08 2020 at 15:50):

I haven't been following closely, but when she talked about sigma types, didn't she draw a picture and call them fibrations? The HoTT is in the interpretation.

#### Bhavik Mehta (May 08 2020 at 15:53):

kind of off-topic but does anyone know what software she's using to write/present those notes?

#### Jeremy Avigad (May 08 2020 at 15:57):

I was wondering the same thing! She did a nice job with them. My guess is that she is using a Wacom tablet and a Google Jamboard.

#### Bhavik Mehta (May 08 2020 at 15:58):

I don't think it's a google jamboard - the icons at the top look like apple icons rather than google's

#### Bhavik Mehta (May 08 2020 at 16:21):

I'm pretty sure it's Notability for mac actually

#### Patrick Massot (May 08 2020 at 16:55):

I haven't been following closely, but when she talked about sigma types, didn't she draw a picture and call them fibrations? The HoTT is in the interpretation.

This has nothing to do with HoTT. This is what any geometer or topologist will think about in the very first second they see sigma types. Presenting this interpretation as a revolutionary idea is the beginning of what makes the HoTT community often look so arrogant. HoTT starts with equality types that are not subsingletons.

#### Patrick Massot (May 08 2020 at 17:14):

To clarify things, let me say I mostly enjoyed @Emily Riehl's talk (and I love her little book about categories). And she seems really honest, but the sloppy language and lapsus still reinforce the dark sides of HoTT. She explained very clearly:

1. why HoTT seems like very promising foundations for infinity categories
2. hence why explaining infinity categories to undergrads (or say general mathematicians) would require teaching HoTT first

This seems all fair (although I'm not competent at all in this kind of mathematics). And then she very carefully didn't cross the boundary to claim that:

1. Everybody should be doing infinity categories because this is all of mathematics
2. Hence everybody should use HoTT since this kind of foundations is relevant to all of mathematics.

This is very subjective, but I felt she was really close to saying 4, which I think is really wrong. The other thing that annoyed me but was 100% in the chat and not in her talk is the way some HoTT zealots boast that HoTT is good for formalized mathematics since type theory is everywhere in formalized mathematics. This is almost 100% scientific fraud until someone comes up with a non-trivial maths formalization in HoTT foundations that is not about HoTT-style mathematics (homotopy theory). Of course this gets us back to point 3 above: if mathematics is only about infinity categories then everything is HoTT-style mathematics. Again, Emily essentially didn't mentioned formalized mathematics, but using the terms "type theory" and HoTT interchangeably reinforce this dark temptation of HoTT.

#### Emily Riehl (May 08 2020 at 17:43):

Hi @Patrick Massot . I'm glad to hear you "mostly" enjoyed the talk ;)

To clarify I didn't claim your point 4 because I don't believe it myself! I agree that it would be arrogant to claim that the sort of foundations that would be convenient for me would necessarily also be convenient for everyone else.

When I framed this talk for the Berkeley logic folks, I explicitly described it as an attempt to share one mathematician's particular point of view of foundations. As a personal anecdote rather than a diatribe.

#### Patrick Massot (May 08 2020 at 18:14):

Probably you didn't read the whole thread, but this discussion started with Reid's message saying "In the zoom chat: Kevin and Patrick hating on HoTT". I only wanted to clarify that. Again I don't say that you claim point 4, but I think being extra careful with wording can help. I also guess you didn't really expect almost 300 people attending the talk, which makes things way too serious when we simply want to have fun with mathematics...

#### Emily Riehl (May 08 2020 at 18:23):

Haha, you're right, I see the context now. Glad to see the zoom and zulip chats are functioning exactly as intended @Reid Barton (I was trying to invite a bit of heckling ;)

In any case, don't worry. I'm not offended. I view this as a mostly friendly debate that's good for both the lean and HoTT communities.

#### Nam (May 14 2020 at 14:10):

https://www.icts.res.in/outreach/kaapi-with-kuriosity/2020may

#### Nam (May 14 2020 at 14:10):

Online lecture "Automating Mathematics" by Siddhartha Gadgil, the author of ProvingGround

#### Reid Barton (May 14 2020 at 15:27):

Sounds remarkably similar to https://www.ias.edu/events/seminar-theoretical-machine-learning-87

#### Reid Barton (May 14 2020 at 15:28):

I guess AlphaZero is the sort of thing one can't avoid mentioning in this context

#### Alex J. Best (May 17 2020 at 10:45):

Nam said:

Online lecture "Automating Mathematics" by Siddhartha Gadgil, the author of ProvingGround

#### Jason Rute (May 17 2020 at 11:46):

I just saw this (and am watching the end of the talk).

#### Jason Rute (May 17 2020 at 11:49):

They just mentioned Lean. "The lean theorem prover has three (small) proof checkers written in three languages"

#### Jason Rute (May 17 2020 at 12:03):

Anyone who saw the whole thing, is it mostly a big idea, or does he build anything? (Both are ok. I'm just curious.)

#### Kevin Buzzard (May 17 2020 at 12:07):

it's a general audience talk just giving an overview of the area

#### Kevin Buzzard (May 17 2020 at 12:07):

He's talking about Lean again, he has been experimenting with it

#### Reid Barton (May 17 2020 at 12:18):

Lean sure is getting a lot of airtime

#### Jason Rute (May 17 2020 at 12:21):

So I just found his ProvingGround. It seems to be some sort of Scala wrapper around Lean, but using HoTT. Is it Lean 2?

#### Jalex Stark (May 17 2020 at 17:24):

this slideshow is nice, apparently he used ATP techniques to help in polymath14

#### Jason Rute (May 17 2020 at 18:44):

Just a small advertisement. If anyone (including @Siddhartha Gadgil ) is interested in Machine Learning for Lean or other theorem provers, there is a lot of discussion (mostly from me, but also from others) on the stream Machine Learning for Theorem Proving.

#### Jalex Stark (May 19 2020 at 00:16):

@Patrick Lutz is running a Lean learning seminar

#### Patrick Lutz (May 19 2020 at 01:37):

I should add that I am running it jointly with Rahul Dalal and Thomas Browning and that the main page for the website is https://sites.google.com/view/berkeleyleanseminar/home

#### Siddhartha Gadgil (May 19 2020 at 06:28):

Jason Rute said:

So I just found his ProvingGround. It seems to be some sort of Scala wrapper around Lean, but using HoTT. Is it Lean 2?

Thanks for mentioning ProvingGround. It is not a wrapper on lean but an implementation in scala of DTT (using scala types as upper bounds capturing some of the type theory). I have tried to import from Lean's export format. My goal is to have various forms of learning, including for example recognizing when a Lemma is non-trivial etc. But since the successes so far are minor I will share more when there is more to write about.

Last updated: May 17 2021 at 22:15 UTC