seminars

Stream: general

[Nam]

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]

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

[Brandon Brown]

Looks neat but wish it had unicode

[Mario Carneiro]

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

[Johan Commelin]

Which I think looks really cool!

[Mario Carneiro]

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

[Reid Barton]

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

[Brandon Brown]

"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]

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]

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

[Jannis Limperg]

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]

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

[Brandon Brown]

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

[Mario Carneiro]

No trusted core took me by surprise

[Mario Carneiro]

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]

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"

[Patrick Stevens]

^^

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Stevens]

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]

It doesn't unfold behind the scenes to J

[Mario Carneiro]

it's axiomatic

[Patrick Stevens]

Oh, fair enough :P

[Mario Carneiro]

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]

(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]

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

[Mario Carneiro]

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]

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]

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

[Reid Barton]

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]

that's the anonymous extensions I linked above

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Reid Barton]

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]

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

[Valery Isaev]

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]

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?

[Johan Commelin]

Nope.

[Johan Commelin]

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

[Johan Commelin]

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

[Valery Isaev]

What about eta for $\Pi$-types?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

We have that one

[Valery Isaev]

Johan Commelin said:

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

Yes, this one.

[Johan Commelin]

Ok, that one is fine.

[Kevin Buzzard]

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

[Kevin Buzzard]

Like eta for structures is a theorem

[Valery Isaev]

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

[Marc Huisinga]

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

[Marc Huisinga]

there's an eta rule in 2.2

[Marc Huisinga]

(https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf)

[Chris Hughes]

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]

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

[Valery Isaev]

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]

You need it to prove funext I think.

[Mario Carneiro]

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]

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]

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]

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]

zoom link: https://msri.zoom.us/j/4105167397?status=success

[Kenny Lau]

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]

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]

In the zoom chat: Kevin and Patrick hating on HoTT

[Patrick Massot]

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

[Jeremy Avigad]

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

[Reid Barton]

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

[Jeremy Avigad]

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]

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

[Jeremy Avigad]

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]

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

[Bhavik Mehta]

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

[Patrick Massot]

Jeremy Avigad said:

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]

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:

3. Everybody should be doing infinity categories because this is all of mathematics
4. 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]

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]

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]

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]

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

[Nam]

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

[Reid Barton]

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

[Reid Barton]

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

[Alex J. Best]

Nam said:

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

On right now https://www.youtube.com/watch?v=ya5SAmx-7QI

[Jason Rute]

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

[Jason Rute]

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

[Jason Rute]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

Lean sure is getting a lot of airtime

[Jason Rute]

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]

this slideshow is nice, apparently he used ATP techniques to help in polymath14
http://math.iisc.ac.in/~gadgil/presentations/HomogeneousLengths.html#/3

[Jason Rute]

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]

@Patrick Lutz is running a Lean learning seminar
https://sites.google.com/view/berkeleyleanseminar/schedule?authuser=0

[Patrick Lutz]

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]

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.