Hello

Stream: new members

[Harry Gindi]

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

[Johan Commelin]

Hey, welcome! Good to see you.

[Johan Commelin]

Things are going pretty good here (-;

[Harry Gindi]

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

[Johan Commelin]

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

[Harry Gindi]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Harry Gindi]

Does it have Grothendieck constructions

[Johan Commelin]

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

[Johan Commelin]

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

[Harry Gindi]

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

[Harry Gindi]

Ah, ok!

[Johan Commelin]

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

[Harry Gindi]

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]

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

[Harry Gindi]

via Segal's observation

[Harry Gindi]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Harry Gindi]

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

[Johan Commelin]

First you need to install a Lean environment.

[Johan Commelin]

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

[Harry Gindi]

vscode

[Johan Commelin]

Great!

[Johan Commelin]

There is a Lean extension for VScode

[Harry Gindi]

Is the Windows lean environment crippled?

[Johan Commelin]

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

[Harry Gindi]

oh, that's neat!

[Johan Commelin]

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

[Andrew Ashworth]

If you like textbooks I would recommend Theorem Proving in Lean

[Johan Commelin]

Maybe it is about to be fixed.

[Harry Gindi]

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

[Harry Gindi]

that's why I'm asking

[Andrew Ashworth]

Lean on Windows works great

[Kenny Lau]

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

[Andrew Ashworth]

There are some issues with setting $PATH correctly. However, if you are the kind of person to have WSL installed, I'm sure you'll be able to fix it

[Harry Gindi]

Thanks!

[Kenny Lau]

oh wait, you said you're working in Linux, never mind then

[Harry Gindi]

Both work, Kenny. WSL is slow though

[Harry Gindi]

Disk I/O is extremely bad

[Harry Gindi]

then again, so is mingw64 =D

[Kenny Lau]

what do you mean?

[Harry Gindi]

iirc disk i/o on cygwin and msys is benchmarked just as slow as WSL

[Harry Gindi]

it's the main reason why things are so slow.

[Harry Gindi]

I was really active on the WSL github for like two years, and performance is on-par with linux now except for disk i/o

[Johan Commelin]

@Harry Gindi Once you have Lean installed, you will want to fork https://github.com/leanprover-community/mathlib/
Then you need to run leanpkg build in that directory. After that, get yourself some tea. Your computer will be warming your room for about an hour.

[Harry Gindi]

but I also used msys2 before, and it was even slower

[Kenny Lau]

then what's the best one?

[Harry Gindi]

Kenny Lau, meh, nothing's great. The best thing you could do probably is run a VM

[Harry Gindi]

if you're concerned about performance

[Harry Gindi]

Thanks Johan!

[Andrew Ashworth]

I compile Lean with MSYS2, disk i/o is far from the limiting factor when it comes to performance

[Kenny Lau]

and you need to rewarm your room for an hour every time you update mathlib, isn't Lean wonderful!

[Harry Gindi]

Andrew Ashworth, then maybe performance on WSL is better than msys2 on everything but disk I/O

[Kenny Lau]

@Harry Gindi ping

[Harry Gindi]

hello!

[Kenny Lau]

Harry Gindi, not ping

[Harry Gindi]

I'm aware, I'm just using the web UI

[Andrew Ashworth]

is it now? I can't imagine there being a huge difference

[Harry Gindi]

Andrew, they did benchmarks on phoronix, and on cpu-only tasks, WSL performs at 95-100% of native

[Harry Gindi]

once it hits disk i/o, it crashes to like 20%

[Harry Gindi]

it has to do with the fact that NTFS doesn't use inodes and therefore can't cache them effectively

[Harry Gindi]

also, windows defender, and a bunch of other things just kill it on disk i/o

[Harry Gindi]

anyway, going to get this lean system installed

[Harry Gindi]

does arch have a lean-git AUR package?

[Harry Gindi]

Looks like it does

[Andrew Ashworth]

ah, I was aware of that. I think you can compile Lean with visual studio and get a totally native binary, if i recall correctly

[Andrew Ashworth]

i've never investigated it though, so ymmv

[Harry Gindi]

blech, I have an arch installation on this pc

[Andrew Ashworth]

disk access is not an issue at 20% or 100% anyway

[Harry Gindi]

but every time I decide to jump into linux, I get sidetracked

[Harry Gindi]

I end up staying up all night messing around with it, it's unhealthy for me

[Johan Commelin]

Don't use that arch thing.

[Harry Gindi]

oh, it's bad?

[Harry Gindi]

or are you saying don't use arch in general :D

[Johan Commelin]

The VScode Lean extension is better. It sets up a useful wrapper called elan.

[Johan Commelin]

No, I run arch as OS :lol: So that's fine.

[Harry Gindi]

the arch thing is just a lean system, I thought

[Harry Gindi]

anyway gonna work on this tomorrow morning

[Harry Gindi]

cheers all

[Kevin Buzzard]

@Kenny Lau I think https://github.com/leanprover/mathlib/blob/master/docs/elan.md is a better place to direct computer-savvy Windows users to than your link

[Kenny Lau]

fair

[Scott Morrison]

Yes --- please, please, everyone should now be using elan, no messing around with $PATH, no installing complicated things like msys2 or WSL, just go with the bare minimum provided by "git bash" and its installer, then work entirely inside VS Code.

[Kevin Buzzard]

@Harry Gindi ^^ that

[Scott Morrison]

Also, welcome @Harry Gindi. :-)

[Harry Gindi]

Got it, thanks!

[Harry Gindi]

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

[Kevin Buzzard]

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]

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]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

I'm guessing that monads work well?

[Kevin Buzzard]

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

[Harry Gindi]

ah

[Kevin Buzzard]

groups work well

[Kevin Buzzard]

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

[Harry Gindi]

I mean, my research is in category theory

[Harry Gindi]

but I'll see how hard it is

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Harry Gindi]

Do presheaves of sets make sense?

[Kevin Buzzard]

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]

they call them presheaves of types here

[Kevin Buzzard]

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

[Harry Gindi]

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

[Kevin Buzzard]

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]

My code sucks though

[Kevin Buzzard]

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

[Kevin Buzzard]

I am currently refactoring all of it with an MSc student

[Harry Gindi]

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

[Harry Gindi]

working with functors of points the whole way?

[Harry Gindi]

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

[Kevin Buzzard]

I followed the stacks project

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

But nowadays we would not write it like that

[Kevin Buzzard]

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

[Kevin Buzzard]

As of about last week

[Harry Gindi]

neat!

[Harry Gindi]

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

[Harry Gindi]

was this done entirely without model structures using e.g. Ex^∞?

[Kevin Buzzard]

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]

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

[Harry Gindi]

mhm

[Harry Gindi]

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

[Harry Gindi]

cheers, this seems exciting

[Kevin Buzzard]

it's the future

[Kevin Buzzard]

but I might have died before it becomes really important

[Kevin Buzzard]

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

[Harry Gindi]

ascended to robothood

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Harry Gindi]

like any assistant they must be trained =p

[Harry Gindi]

otherwise all they do is spill coffee on you

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Harry Gindi]

this might be a nice change of pace for him

[Kevin Buzzard]

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

[Harry Gindi]

is anyone doing analysis-related stuff?

[Kevin Buzzard]

Yes, but it's happening very slowly

[Harry Gindi]

because he always liked analysis

[Harry Gindi]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Harry Gindi]

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

[Kevin Buzzard]

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]

Is that even possible?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Harry Gindi]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Eventually we'll have them on Banach manifolds or something

[Harry Gindi]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

they will not want to work on a Banach manifold

[Harry Gindi]

it's not even meaningful on a banach manifold

[Harry Gindi]

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

[Kevin Buzzard]

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

[Harry Gindi]

sure, yes

[Kevin Buzzard]

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]

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

[Harry Gindi]

and that identification is not obvious without additional structure

[Kevin Buzzard]

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

[Harry Gindi]

I get ya!

[Harry Gindi]

I fully agree with this

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

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

[Harry Gindi]

cheers!

[Cris Perdue]

I am a software developer and longtime aficionado of computerized deduction, taking a scenic excursion from building a web GUI proof assistant "for beginners" (https://prooftoys.org/) to the modern world of Lean.