PedroST

Stream: new members

[Pedro Sánchez Terraf]

Hi, I'm new here... introducing myself as expected.

[Pedro Sánchez Terraf]

I'm a mathematician from Argentina and I'm partly working on formalization. For that two reasons I got curious about Lean.

[Kevin Buzzard]

What area of maths do you work in?

[Pedro Sánchez Terraf]

Hi! I'm working in mathematical logic, did my PhD in Universal Algebra and now going into Set Theory, mostly applications of Descriptive S.T.

[Pedro Sánchez Terraf]

Mainly, those applications are to theoretical comp. sci.

[Kevin Buzzard]

@Chris Hughes was asking questions about universal algebra on the Discord today

[Pedro Sánchez Terraf]

If it is something close to the topics I studied, I'd be glad to answer here (though I would also strongly suggest to ask on math.stackexchange.com, I know at least one extremely good expert that visits often).

[Adam Topaz]

@Pedro Sánchez Terraf and @Chris Hughes : I've done (and still doing) some basic stuff with universal algebra with @Colter MacDonald in lean. We have a repo here: https://github.com/adamtopaz/UnivAlg in case you find it interesting/useful.

[Pedro Sánchez Terraf]

@Adam Topaz Thanks, I'll take a look

[Adam Topaz]

And since you're now a set theorist, you would probably be interested in flypitch (if you don't already know about it): https://flypitch.github.io/

[Pedro Sánchez Terraf]

They are actually my direct competitors :-)... We were also formalizing forcing, but in Isabelle.

[Adam Topaz]

Ah!

[Pedro Sánchez Terraf]

We're not done yet, our approach is rather different. But I'm aware of their work

[Mario Carneiro]

Yesterday's competitors are today's collaborators :)

[Pedro Sánchez Terraf]

Hi Mario!

[Kevin Buzzard]

I think it's a great idea to formalise serious maths in several provers, so we can figure out what is best at what.

[Pedro Sánchez Terraf]

So sorry, I have to leave for while, my family arrived and have some obligations.
Btw, very nice talk at CICM, @Kevin Buzzard . I also feel sympathetic, I've been at math Olympiads at my country :-) See you in while, or tomorrow.

[Pedro Sánchez Terraf]

@Adam Topaz By the way, the rest of my team (Emmanuel Gunther and Miguel Pagano) were also working on the formalization of UA, but this time without me and in Agda.

[Adam Topaz]

I love agda. But I'm not experienced enough with actually using it.

[Jacques Carette]

Universal Algebra ought to not only be formalized in a theorem prover, it ought to be 'internalized' too. Its constructions work so well (and uniformly), that they should be kept to the meta-level. Much too useful to be segregated just there.

[Pedro Sánchez Terraf]

@Jacques Carette I think I'm not familiar enough with ITP terminology to fully understand the meaning of "internalized", I'd be grateful for any pointer to the literature.

[Jacques Carette]

I mean that it ought to be able to operate on Lean theories to output Lean theories (say for the homomorphism construction). But that is currently metaprogramming of the kind that is not (yet) available. Or has that changed? Last I look metaprogramming in Lean was restricted to the proof monad.

[Adam Topaz]

I also don't know what "internalized" means, but I still completely agree! I started that UnivAlg repository as an experiment because it felt silly to repeat all these free constructions from universal algebra (and some basic ones still seem to be missing from mathlib, like the free algebra on a multiplicative monoid with an absorbing zero, which I wanted for other reasons). In this case the internalization can probably be accomplished with some metaprogramming

[Adam Topaz]

Oh, just saw the new comment!

[Jacques Carette]

[I'm also "cheating" here, as I've been working on that for a while. See the paper at CICM 2020 for an example of the work that's already done. Just not in Lean. Not quite in Agda either as, although it comes closer, it still doesn't let one create fresh names that escape their scope.]

[Jalex Stark]

i think this kind of thing is in scope for current lean metaprogramming

[Jalex Stark]

one of the more advanced things I know of in this direction is to_additive

[Jalex Stark]

i think it is true that this kind of metaprogramming will be easier in lean 4, and indeed the community will have to learn about new metaprogramming stuff in order to port mathlib

[Scott Morrison]

I think a fairly low-hanging piece of universal algebra / metaprogramming might be to automate the construction of colimits in algebraic categories, i.e. writing Lean commands that synthesize most or all of https://github.com/leanprover-community/mathlib/blob/84b450d/src/algebra/category/Group/colimits.lean just looking at the definitions of add_comm_group and monoid_hom. But it's not clear to me it's really worth the effort. :-)

[Scott Morrison]

One could also "do more theory" first (Lawvere theories).

[Jacques Carette]

It's all about scale. From ~300 lines of Tog (a toy Agda-like language), my PhD student Yasmine can generate slightly over 10,000 lines of Tog that in all systems we know about need to be written out by human beings. We're working a DSL to control the generation (you don't really want all that stuff by default). Homomorphisms, 4 different variations of term algebras, products, logical relations, and more, are all "free". Why would we force humans to write them out by hand once we know they don't have to?

[Jacques Carette]

[I've tried to do Lawvere Theories in Agda. I didn't get far. Most of the stuff out there is seriously thin on details, and I chose to not use the (evil) skeletal version, and that made things worse. I don't think any of what's out there is wrong, just massively detail-poor.]

[Adam Topaz]

What do you mean by the "evil" skeletal version of Lawvere theories?

[Adam Topaz]

Oh, is this just referring to a choice of a skeleton for the category of finite sets?

[Jacques Carette]

@Adam Topaz Yes. I was trying to see if I could get away without artificial choices like that. Mostly, yes. In that case, I got thoroughly stuck. I think it's my problem. Not sure who to ask though - most don't have the patience for these kinds of concerns.

[Jalex Stark]

maybe someone on the category theory zulip would offer some patience

[Patrick Massot]

Jacques, I have two questions about your description of your work. First, did you look at what Cyril and his coauthors did in this paper which is also about fighting boilerplate while writing algebraic theories, but maybe in another direction? This whole story seems pretty important to me, and it would be nice to have a specification language independent from the target proof assistant. My second question may sound polemic but I'm really curious so I hope it won't sound aggressive. Since you seem really interested in mathematics, why do you use Agda which is openly a type theory playground and programming language much more than a proof assistant (and is basically not used for maths compared to Mizar, Coq, Isabelle and Lean)?

[Patrick Massot]

I also have a question for Pedro, a very naive one since I know nothing about foundations and set theory. You wrote that you use Isabelle/ZF to formalize forcing. Isn't it harder to prove things about set theory in a proof assistant based on set theory? Naively I expect it to be much harder to separate the meta-theory from the theory in this setup. Type theory naturally seems more neutral with respect to axioms of set theory.

[Mario Carneiro]

Most set theory is done in set theory, even more explicitly than the usual hat tip to ZFC you see elsewhere

[Mario Carneiro]

Also Lean definitely isn't neutral with respect to the axioms of set theory (it proves ZFC!)

[Mario Carneiro]

Flypitch was IIRC mainly a problem of how to rephrase all the constructions of meta-set theory from set theory (where these people all worked) to type theory, often quite nontrivially

[Mario Carneiro]

For example a "countable transitive model of ZFC" is a very common concept in meta-set theory but it doesn't make any sense in type theory (because "transitive model" talks about the relation between the model's epsilon and the real epsilon, and the latter doesn't exist in type theory)

[Pedro Sánchez Terraf]

Thanks @Patrick Massot for your question. Mario's observations are all correct. Let me put some detail.
One of the appealing features of forcing is that it enables you to prove rather basic/fundamental stuff by working with the full machinery of set theory.

In a nutshell, assuming that ZFC is consistent, you want to prove that ZFC + ¬CH is consistent (the assumption is necessary by Gödel's second thm). Naively, this amounts to assuming you have a model M of ZFC, and you need to construct some model N of ZFC + ¬CH. Forcing lets you do this in a rather canonical way (akin to adding a new element G which is “transcendental” over M). Now, some logical manipulations translate this model-theoretic construction to finitary one: you end up with a proof (assuming only arithmetic) that there is no proof of contradiction from the axioms of ZFC+¬CH, if there wasn't one from ZFC.

[Pedro Sánchez Terraf]

Our formalization work focuses on the model-theoretic part of the argument, that is, forcing as a tool to extend (countable transitive) models of ZFC, and our results are proved in ZF. This does not gives us finitary consistency proofs, but are framework does not assume more than needed.

Type theories like the ones that support Lean and Coq assume much more than that (due to the availability of universes). In that sense, they are “more likely to be inconsistent” (though nobody believe they are). It is just that if you want to formalize (relative) consistency results as above, you have to start with a really poor metatheory.

All that said, working on Isabelle/ZF is especially laborious, since it lacks the full automation of the usual Isabelle logic (HOL), yet.

[Jacques Carette]

@Patrick Massot I'll answer your first question here (it doesn't highjack this thread too much) and start a new one for the other. I am well aware of that paper - chronologically it appeared after the authors saw my talk in August 2018 at a Dagstuhl meeting on formalizing mathematics in type theory, where I showed a lot of my work on boilerplate elimination. My current work (with Yasmine Sharoda and Bill Farmer) aims for just that: a language-independent specification language for algebraic theories. See Leveraging the Information Contained in Theory Presentations presented at the latest CICM for the details. The prototype is on github (https://github.com/ysharoda/tog). We embed it into Tog, but that's just because we didn't want to write a type checker for a dependently typed language with modules from scratch, and also be able to program it easily [so the fact that it's written in Haskell is a big plus.] Yasmine's next task is to write back-ends that target other languages, to show that it is indeed system-independent.

[Pedro Sánchez Terraf]

@Jacques Carette please ping for your next answer!

[Jacques Carette]

@Pedro Sánchez Terraf It's in the "Why Agda?" thread.

[Patrick Massot]

Thanks Jacques. Am I right to think that https://github.com/ysharoda/tog/blob/master/Library/mathscheme.tog is the source that gets translated? I don't see anything involving several types, like a module over a base ring. Do you handle that?

[Jacques Carette]

Yes, that's the main input. Right now, the code only handles unisorted equational theories (same as with classical universal algebra). We're definitely planning to extend to the multi-sorted case. We just want to be careful, as there are some subtleties that arise, and we don't want to produce incorrect results.