## Stream: new members

### Topic: Hello

#### Harry Gindi (Nov 10 2018 at 18:35):

Hiya, some of you probably know me from mathoverflow. I was curious how things are going in here.

#### Johan Commelin (Nov 10 2018 at 18:35):

Hey, welcome! Good to see you.

#### Johan Commelin (Nov 10 2018 at 18:35):

Things are going pretty good here (-;

#### Harry Gindi (Nov 10 2018 at 18:36):

I'm a complete noob on the whole theorem proving thing, but I feel like it's something worth learning

#### Johan Commelin (Nov 10 2018 at 18:36):

One of our biggest problems is lack of (wo)man-power

#### Harry Gindi (Nov 10 2018 at 18:36):

I'd like to eventually work on the library for simplicial sets, but I'm completely worthless at programming

#### Johan Commelin (Nov 10 2018 at 18:37):

Right. The first thing you need to learn is that you should ask lots of questions here :lol:

#### Johan Commelin (Nov 10 2018 at 18:37):

You don't need that much programming experience. Coincidentally, I did some stuff on simplicial sets a couple of months ago.

#### Johan Commelin (Nov 10 2018 at 18:38):

In the mean time, Scott wrote a very very nice category library.

#### Harry Gindi (Nov 10 2018 at 18:38):

Does it have Grothendieck constructions

#### Johan Commelin (Nov 10 2018 at 18:38):

I've been meaning to update my stuff, but haven't done so yet.

#### Johan Commelin (Nov 10 2018 at 18:38):

It only has the basics so far. We are in the process of adding limits and colimits.

#### Harry Gindi (Nov 10 2018 at 18:38):

If it does, maybe it's already time to introduce the Theta construction that I use in my research

Ah, ok!

#### Johan Commelin (Nov 10 2018 at 18:39):

For example: we don't have abelian categories yet.

#### Harry Gindi (Nov 10 2018 at 18:39):

If there's a simplicial library and a category theory library, you might be able to use simplicial objects in Cat to get monoidal categories

#### Johan Commelin (Nov 10 2018 at 18:39):

No fundamental obstructions. Just that there are only 3 people working on this in their spare time.

#### Harry Gindi (Nov 10 2018 at 18:39):

via Segal's observation

#### Harry Gindi (Nov 10 2018 at 18:39):

Also, are Abelian categories really that fundamental for theorem proving?

#### Johan Commelin (Nov 10 2018 at 18:40):

Practice seems to show that theorem provers need a delicate balance between hands-on constructions and big theoretical hammers.

#### Johan Commelin (Nov 10 2018 at 18:40):

Not for theorem proving, but they are for applying theorem provers to (some, eg my) mathematical research.

#### Harry Gindi (Nov 10 2018 at 18:41):

mhm, do you know where I can get bootstrapped with experience to start contributing?

#### Johan Commelin (Nov 10 2018 at 18:41):

First you need to install a Lean environment.

#### Johan Commelin (Nov 10 2018 at 18:41):

What editor do you use to type LaTeX and the likes?

vscode

Great!

#### Johan Commelin (Nov 10 2018 at 18:41):

There is a Lean extension for VScode

#### Harry Gindi (Nov 10 2018 at 18:42):

Is the Windows lean environment crippled?

#### Johan Commelin (Nov 10 2018 at 18:42):

Install it, and open an empty Lean file. It will then ask if you want it to install Lean for you.

oh, that's neat!

#### Johan Commelin (Nov 10 2018 at 18:42):

I think it was fixed. I am not sure. I haven't touched Windows in 10 years.

#### Andrew Ashworth (Nov 10 2018 at 18:42):

If you like textbooks I would recommend Theorem Proving in Lean

#### Johan Commelin (Nov 10 2018 at 18:42):

Maybe it is about to be fixed.

#### Harry Gindi (Nov 10 2018 at 18:43):

If it's not working, I have the Win10 Linux emulator installed

#### Andrew Ashworth (Nov 10 2018 at 18:43):

Lean on Windows works great

#### Kenny Lau (Nov 10 2018 at 18:44):

@Harry Gindi here is my (controversal) instructions on how to get Lean on windows

#### Kevin Buzzard (Nov 10 2018 at 21:30):

@Harry Gindi ^^ that

#### Scott Morrison (Nov 10 2018 at 21:33):

Also, welcome @Harry Gindi. :-)

Got it, thanks!

#### Harry Gindi (Nov 10 2018 at 21:34):

Also hello, Kevin and Scott, it's been a while since I saw you on MO

#### Kevin Buzzard (Nov 10 2018 at 21:34):

Here is a roadmap to getting started. First read through all of Theorem Proving In Lean and do all the exercises. Then choose a project to work on, and work on it.

#### Kevin Buzzard (Nov 10 2018 at 21:34):

The projects I chose were: (1) do all the exercises in the undergraduate class I was teaching at the time and then (2) define schemes and prove that an affine scheme is a scheme.

#### Kevin Buzzard (Nov 10 2018 at 21:35):

Do not underestimate how difficult all of this is at this point.

#### Harry Gindi (Nov 10 2018 at 21:35):

It seems like it'll be really annoying, don't worry =)

#### Harry Gindi (Nov 10 2018 at 21:36):

I think maybe a good project to work on would be weak factorization systems once I learn stuff

#### Kevin Buzzard (Nov 10 2018 at 21:36):

Working with isomorphisms is difficult. Working with categories is even more difficult, for several reasons -- some associated with dependent type theory (it is difficult to transport structure along isomorphisms at this point, although things will change one day), some associated with universe issues (mathematicians being sloppy about universes, basically) and other things too

#### Kevin Buzzard (Nov 10 2018 at 21:37):

But there is no better recommendation than "start on something and whenever you get stuck, ask here"

#### Kevin Buzzard (Nov 10 2018 at 21:37):

The first thing you will probably have to ask is a question of the form "here's a link to a pdf, I want to make definition 2.3 of that paper in Lean, where do I even start?". There will be an answer.

#### Harry Gindi (Nov 10 2018 at 21:38):

WFS would be useful if anyone wants to go full bore and do model categories, and it can be done with monads for algebraic weak factorization systems

#### Harry Gindi (Nov 10 2018 at 21:38):

I'm guessing that monads work well?

#### Kevin Buzzard (Nov 10 2018 at 21:38):

Listen, honestly, categories are really like jumping in at the deep end

ah

groups work well

#### Kevin Buzzard (Nov 10 2018 at 21:38):

but it is not impossible, and you have to jump in somewhere

#### Harry Gindi (Nov 10 2018 at 21:39):

I mean, my research is in category theory

#### Harry Gindi (Nov 10 2018 at 21:39):

but I'll see how hard it is

#### Kevin Buzzard (Nov 10 2018 at 21:39):

well, when I arrived here a year ago people were already talking about formalising categories, and one year later they still haven't managed to do adjoint functors.

#### Kevin Buzzard (Nov 10 2018 at 21:40):

This is basically for two reasons: (1) universes make this harder than you think and (2) lack of manpower or personpower or whatever it should be called nowadays

#### Harry Gindi (Nov 10 2018 at 21:40):

I would have assumed that monads might be easier than adjunctions, but maybe this is a mistake

#### Kevin Buzzard (Nov 10 2018 at 21:40):

I'm also exaggerating a little. But dependent type theory is perhaps not set up with category theory in mind

#### Kevin Buzzard (Nov 10 2018 at 21:41):

On the other hand, "difficult" is certainly not the same as "impossible"

#### Harry Gindi (Nov 10 2018 at 21:41):

Do presheaves of sets make sense?

#### Kevin Buzzard (Nov 10 2018 at 21:41):

and there is no actual obstruction to doing adjoints and a whole bunch more. It's just that people really like (a) working in the maximal generality and (b) writing automation as they go

#### Kevin Buzzard (Nov 10 2018 at 21:41):

they call them presheaves of types here

#### Kevin Buzzard (Nov 10 2018 at 21:42):

but I defined these in a hands-on way when doing schemes, no problem

#### Harry Gindi (Nov 10 2018 at 21:42):

Neat, I'll have to look at what you've done already before I try to jump in

#### Kevin Buzzard (Nov 10 2018 at 21:42):

I did not use the category theory machinery though, I just wrote down the axioms for a functor in that specific case rather than relying on a general theory (which at that time was not there anyway)

#### Kevin Buzzard (Nov 10 2018 at 21:42):

My code sucks though

#### Kevin Buzzard (Nov 10 2018 at 21:43):

because it was the code I wrote to learn how to do mathematics in dependent type theory

#### Kevin Buzzard (Nov 10 2018 at 21:43):

I am currently refactoring all of it with an MSc student

#### Harry Gindi (Nov 10 2018 at 21:43):

so when you defined schemes, did you follow e.g. Toën?

#### Harry Gindi (Nov 10 2018 at 21:44):

working with functors of points the whole way?

#### Harry Gindi (Nov 10 2018 at 21:44):

or is that exactly the kind of non-kosher thing that implicitly uses universes

#### Kevin Buzzard (Nov 10 2018 at 21:44):

I followed the stacks project

#### Kevin Buzzard (Nov 10 2018 at 21:44):

https://github.com/kbuzzard/lean-stacks-project/blob/master/src/tag009I.lean

#### Kevin Buzzard (Nov 10 2018 at 21:44):

there's presheaves of types on a basis of open sets of a top space

#### Kevin Buzzard (Nov 10 2018 at 21:44):

But nowadays we would not write it like that

#### Kevin Buzzard (Nov 10 2018 at 21:45):

we'd use the category theory machinery, which seems to be just about ready to do that sort of thing.

neat!

#### Harry Gindi (Nov 10 2018 at 21:45):

I heard that some simplicial set machinery was developed up-thread

#### Kevin Buzzard (Nov 10 2018 at 21:47):

In that code I linked to, I am literally saying that a presheaf of types is a function F which takes a basis element to a type, plus a restriction F(U)->F(V), plus the axioms that res from U to U is id and res of res is res. So I am avoiding explicit usage of any category theory formalism.

#### Kevin Buzzard (Nov 10 2018 at 21:47):

You'll have to ask @Johan Commelin where he put his simplicial set stuff. That was also written before categories were available, I believe.

mhm

#### Harry Gindi (Nov 10 2018 at 21:47):

alright let's not but the cart before the horse, I've gotta do the exercises and stuff

#### Harry Gindi (Nov 10 2018 at 21:48):

cheers, this seems exciting

it's the future

#### Kevin Buzzard (Nov 10 2018 at 21:48):

but I might have died before it becomes really important

#### Kevin Buzzard (Nov 10 2018 at 21:48):

I have no idea of the time frame before it becomes (a) useful (b) powerful (c) better than us

#### Harry Gindi (Nov 10 2018 at 21:48):

ascended to robothood

#### Kevin Buzzard (Nov 10 2018 at 21:48):

but currently we are still a long way from (a)

#### Kevin Buzzard (Nov 10 2018 at 21:49):

"proof assistants" currently do nothing but make mathematician's lives harder, for the most part.

#### Harry Gindi (Nov 10 2018 at 21:49):

like any assistant they must be trained =p

#### Harry Gindi (Nov 10 2018 at 21:49):

otherwise all they do is spill coffee on you

#### Kevin Buzzard (Nov 10 2018 at 21:50):

right. And my view (and I do say this firmly with my tongue in my cheek and slightly provocatively, but there is a grain of truth in it) is that currently the main problem is that for the most part they are being trained to do mathematics by computer scientists, which is in my opinion not driving development in the right directions.

#### Harry Gindi (Nov 10 2018 at 21:51):

I'm going to try to get my friend in the US involved on this

#### Kevin Buzzard (Nov 10 2018 at 21:51):

There are a few mathematicians here who are trying to change all this, mostly by saying things such as "mathematicians will not be able to use your software unless you make stuff like (x+y)^3=x^3+3x^2y+3xy^2+y^3 easy to do"

#### Harry Gindi (Nov 10 2018 at 21:51):

he did a math undergrad and he's doing a CS Ph.D., but he hates CS

#### Harry Gindi (Nov 10 2018 at 21:52):

this might be a nice change of pace for him

#### Kevin Buzzard (Nov 10 2018 at 21:52):

https://xenaproject.wordpress.com/2018/06/13/ab3/

#### Harry Gindi (Nov 10 2018 at 21:52):

is anyone doing analysis-related stuff?

#### Kevin Buzzard (Nov 10 2018 at 21:52):

Yes, but it's happening very slowly

#### Harry Gindi (Nov 10 2018 at 21:52):

because he always liked analysis

#### Harry Gindi (Nov 10 2018 at 21:52):

alright, I'll try to cajole him into helping =)

#### Kevin Buzzard (Nov 10 2018 at 21:53):

and in my opinion there is a problem with the development plan we have

#### Kevin Buzzard (Nov 10 2018 at 21:53):

In fact Harry to be honest basic freshman one variable analysis would be a perfect project to learn Lean with

#### Kevin Buzzard (Nov 10 2018 at 21:53):

because the maths is basically very well known and well understood, and putting it into a theorem prover would be a formidable challenge for a beginner, however there would be plenty of people around to help

#### Kevin Buzzard (Nov 10 2018 at 21:54):

The problem is that the general position here is "do everything in the correct generality" which means "the maximal generality"

#### Harry Gindi (Nov 10 2018 at 21:54):

break out a copy of Bourbaki's 'analysis in one real variable' haha

#### Kevin Buzzard (Nov 10 2018 at 21:55):

so instead of developing a basic theory of analysis of functions of one real variable, everyone wants to do stuff on normed spaces and Banach spaces etc etc and then prove all the single-variable theorems in one fell swoop by specialising to this case

#### Harry Gindi (Nov 10 2018 at 21:55):

Is that even possible?

#### Kevin Buzzard (Nov 10 2018 at 21:55):

In my mind a good analogy here is what happened with polynomials

#### Kevin Buzzard (Nov 10 2018 at 21:55):

A computer scientist developed a fabulous library of polynomials in an arbitrary number of variables (in fact for an arbitrary set of variables)

#### Kevin Buzzard (Nov 10 2018 at 21:56):

but when mathematicians wanted to actually use it to prove basic stuff like quadratic reciprocity or finite fields or whatever

#### Harry Gindi (Nov 10 2018 at 21:56):

For example, defining C^\infty functions requires you do have partial derivatives, which come from the 1-dimensional case, if I remember correctly (I haven't done analysis in around 8 years =\)

#### Kevin Buzzard (Nov 10 2018 at 21:56):

they found they really just wanted a much deeper theory of polynomials in one variable

#### Kevin Buzzard (Nov 10 2018 at 21:57):

so at the end of the day an undergraduate here at Imperial, Chris Hughes, just wrote the theory of polynomials in one variable anyway.

#### Kevin Buzzard (Nov 10 2018 at 21:57):

And I kind of suspect that the same might happen for differentiable functions.

#### Kevin Buzzard (Nov 10 2018 at 21:57):

Eventually we'll have them on Banach manifolds or something

#### Harry Gindi (Nov 10 2018 at 21:57):

oh, you're saying that you agree that the 1-variable case is separate and important

#### Kevin Buzzard (Nov 10 2018 at 21:57):

but then when someone wants to prove that the derivative of sin is cos (which we do not have at this point)

#### Kevin Buzzard (Nov 10 2018 at 21:58):

they will not want to work on a Banach manifold

#### Harry Gindi (Nov 10 2018 at 21:58):

it's not even meaningful on a banach manifold

#### Harry Gindi (Nov 10 2018 at 21:58):

the derivative of a map of manifolds is a map on tangent bundles

#### Kevin Buzzard (Nov 10 2018 at 21:58):

I know, I'm just saying that if you write general functions which work in some big generality then you will just end up constantly having to tell these functions to specialise to the case of the real numbers

sure, yes

#### Kevin Buzzard (Nov 10 2018 at 21:59):

the derivative of a map of manifolds is a map on tangent bundles

right, and you'll then have to identify the tangent space of the reals with the reals etc

#### Kevin Buzzard (Nov 10 2018 at 21:59):

What I am saying is that in my opinion there is a need for a theory of functions in one real variable

#### Harry Gindi (Nov 10 2018 at 21:59):

and that identification is not obvious without additional structure

#### Kevin Buzzard (Nov 10 2018 at 21:59):

I believe that there is a little about functions in one complex variable, somewhere in the modular forms work

I get ya!

#### Harry Gindi (Nov 10 2018 at 22:00):

I fully agree with this

#### Harry Gindi (Nov 10 2018 at 22:01):

there's almost always a distinguished most important 1-dimensional case of whatever

#### Harry Gindi (Nov 10 2018 at 22:01):

imagine if people tried to write the categories library starting with 2-categories

#### Harry Gindi (Nov 10 2018 at 22:01):

It's also why e.g. Lawvere's ETCC was dead on arrival

#### Harry Gindi (Nov 10 2018 at 22:02):

anyway, I'm going to give some of this a shot tomorrow morning

#### Harry Gindi (Nov 10 2018 at 22:02):

cheers!

Last updated: May 11 2021 at 00:31 UTC