Zulip Chat Archive

Stream: general

Topic: seminars


view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip Brandon Brown (Apr 28 2020 at 03:35):

Looks neat but wish it had unicode

view this post on Zulip Mario Carneiro (Apr 28 2020 at 04:30):

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

view this post on Zulip Johan Commelin (Apr 28 2020 at 04:45):

Which I think looks really cool!

view this post on Zulip Mario Carneiro (Apr 28 2020 at 04:47):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Brandon Brown (Apr 30 2020 at 17:47):

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

view this post on Zulip Mario Carneiro (Apr 30 2020 at 17:52):

No trusted core took me by surprise

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Patrick Stevens (Apr 30 2020 at 17:55):

^^

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 30 2020 at 17:56):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 30 2020 at 17:57):

It doesn't unfold behind the scenes to J

view this post on Zulip Mario Carneiro (Apr 30 2020 at 17:58):

it's axiomatic

view this post on Zulip Patrick Stevens (Apr 30 2020 at 17:58):

Oh, fair enough :P

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Patrick Stevens (Apr 30 2020 at 18:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 30 2020 at 18:15):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 30 2020 at 18:27):

that's the anonymous extensions I linked above

view this post on Zulip Mario Carneiro (Apr 30 2020 at 18:27):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Apr 30 2020 at 20:59):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 01 2020 at 11:51):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 02 2020 at 12:15):

Nope.

view this post on Zulip Johan Commelin (May 02 2020 at 12:15):

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

view this post on Zulip Johan Commelin (May 02 2020 at 12:15):

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

view this post on Zulip Valery Isaev (May 02 2020 at 12:17):

What about eta for Π\Pi-types?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 02 2020 at 12:21):

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

view this post on Zulip Johan Commelin (May 02 2020 at 12:21):

We have that one

view this post on Zulip Valery Isaev (May 02 2020 at 12:22):

Johan Commelin said:

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

Yes, this one.

view this post on Zulip Johan Commelin (May 02 2020 at 12:23):

Ok, that one is fine.

view this post on Zulip Kevin Buzzard (May 02 2020 at 12:25):

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

view this post on Zulip Kevin Buzzard (May 02 2020 at 12:25):

Like eta for structures is a theorem

view this post on Zulip Valery Isaev (May 02 2020 at 12:27):

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

view this post on Zulip Marc Huisinga (May 02 2020 at 12:28):

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

view this post on Zulip Marc Huisinga (May 02 2020 at 12:29):

there's an eta rule in 2.2

view this post on Zulip Marc Huisinga (May 02 2020 at 12:29):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 02 2020 at 12:35):

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

view this post on Zulip 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 :)

view this post on Zulip Chris Hughes (May 02 2020 at 12:35):

You need it to prove funext I think.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 08 2020 at 14:19):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Reid Barton (May 08 2020 at 15:22):

In the zoom chat: Kevin and Patrick hating on HoTT

view this post on Zulip Patrick Massot (May 08 2020 at 15:32):

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

view this post on Zulip Jeremy Avigad (May 08 2020 at 15:47):

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

view this post on Zulip Reid Barton (May 08 2020 at 15:48):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (May 08 2020 at 16:21):

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

view this post on Zulip Patrick Massot (May 08 2020 at 16:55):

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Nam (May 14 2020 at 14:10):

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

view this post on Zulip Nam (May 14 2020 at 14:10):

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

view this post on Zulip Reid Barton (May 14 2020 at 15:27):

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

view this post on Zulip Reid Barton (May 14 2020 at 15:28):

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

view this post on Zulip Alex J. Best (May 17 2020 at 10:45):

Nam said:

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

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

view this post on Zulip Jason Rute (May 17 2020 at 11:46):

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

view this post on Zulip 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"

view this post on Zulip 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.)

view this post on Zulip Kevin Buzzard (May 17 2020 at 12:07):

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

view this post on Zulip Kevin Buzzard (May 17 2020 at 12:07):

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

view this post on Zulip Reid Barton (May 17 2020 at 12:18):

Lean sure is getting a lot of airtime

view this post on Zulip 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?

view this post on Zulip Jalex Stark (May 17 2020 at 17:24):

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

view this post on Zulip 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.

view this post on Zulip Jalex Stark (May 19 2020 at 00:16):

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

view this post on Zulip 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

view this post on Zulip 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