Introductions

Stream: new members

[Xita Meyers]

Hello, I have never asked a public question on Zulip before, and in order for me to get used to doing so, I have been ordered by @Kenny Lau to state the following in order to introduce myself:

"I am a proud student of Kevin Buzzard."

I look forward to learning much more about Lean through Zulip.

Thanks.

[Kenny Lau]

Welcome!

[Xita Meyers]

Thanks for welcoming me! This is my first time navigating Zulip, nice to meet you!

[Johan Commelin]

Welcome Xita! Nice to meet you.

[Johan Commelin]

What kind of stuff have you been looking at lately? Were you involved in UROP?

[Xita Meyers]

I've been involved in the UROP, but didn't learn very much by reading Theorem Proving in Lean; It was hard to understand to some extent. Currently I'm trying to prove a lemma in number theory that if p is a prime of form 4K + 3, then it cannot divide an integer of form x^2 + 1.

[Johan Commelin]

Ok, nice. Whenever you have questions, just ask! That's how we are all learning. (Most of us don't find the documentation sufficient, but we lack the time, energy, or courage to improve it.)

[Kenny Lau]

or motivation

[Kevin Buzzard]

Hey Su. Here would be a cheap way of doing this. If x^2=-1 mod p (p=4K+3) then x^{4K+2}=-1 mod p as well, contradicting Fermat's Little Theorem.

[Xita Meyers]

Yeah, that's how I've been trying to do it. It's taking longer than I expected.

[Harald Schilly]

Hi, I'm Harald, and I'm one of the devs behind CoCalc ... I've just worked on improving its syntax highlighter and well, I should also learn one or another detail about lean itself :-)

[Patrick Massot]

Welcome Harald!

[Kevin Buzzard]

@Harald Schilly here would be a good place to get information about where Lean is looking for files to import. At the minute I couldn't get mathlib imports working in CoCalc. This and the current inability to see the goal in tactic mode are in my mind the last two problems which need to be solved before lean is really usable. In particular, you guys are nearly there. I am hoping Gabriel Ebner gave you some hints about the latter goal, and the former goal can't be hard. I can't believe I'm saying this but actually just dumping the mathlib files into the lean core directory would probably work, although it's a horrible idea.

[Harald Schilly]

So, I know there is an env variable LEAN_PATH and we could set it to something. There is also a precompiled (but months old) mathlib in /ext/lean/lean/mathlib/. I bet it just depends on setting that lean path correctly to make it work. Should we discuss this in #general ?

[Johan Commelin]

Sure, I think we could move this discussion to the CoCalc thread.

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/CoCalc

[Mario Carneiro]

@Harald Schilly Don't use LEAN_PATH, it is deprecated since the leanpkg tool

[Kevin Buzzard]

There's something I don't understand about the set-up. At some point Lean will have to be told "look at leanpkg.path, that's where you should import stuff". How does that bit work? Aah, presumably this depends on the IDE. And because Harald is involved with writing a new IDE...maybe he needs to be told to look at leanpkg.path.

[Tobias Grosser]

Hey guys, just wanted to introduce myself as it seems to be a common habit here. Some of you may already have seen that I started to ask some smaller questions and also organize a theorem proving sozial at ETH.

[Tobias Grosser]

My background is mostly compilation, static analysis, loop transformations, often using Presburger arithmetic to get where I want to be.

[Tobias Grosser]

Since a year I look into theorem proving, and recently started to use lean.

[Tobias Grosser]

I work since maybe 10 years on LLVM and developed there the Polly loop optimizer

[Tobias Grosser]

I am interested in using lean eventually for teaching and for some of my day-to-day work.

[Simon Hudon]

Welcome to the Lean community! I hope it lives up to your expectations :)

[Tobias Grosser]

Thanks. Until now everybody is very helpful. Looking forward to meet the first members in person next week.

[Simon Hudon]

I wish I could attend. I'm no longer in Zurich but I'm sending a representative

[Simon Hudon]

My friend Malte is a lecturer at ETH and I think he wants to attend

[Tobias Grosser]

That's great.

[Tobias Grosser]

Let me know when you are back in Zurich

[Simon Hudon]

I haven't been back in years but I think I'm due for a visit soon :)

[Corey Richardson]

hi :) I'm coming back around to using Lean. previously I was an intern working on the seL4 verification, and a student doing research for cryptographic protocol analysis ATPs. good to see such a community has sprung up around lean!

[Ryan Smith]

Hi, I'm completely new to Lean. I come from an algebra and number theory background, and don't have much experience with formal logic beyond a course taken in undergrad a lot of years ago.

[Johan Commelin]

Cool, welcome! Where are you based?

[Johan Commelin]

I'm a postdoc in Freiburg, working in algebraic geometry.

[Tobias Grosser]

Welcome Ryan.

[Tobias Grosser]

Researcher at ETH Zurich here!

[Patrick Massot]

Hi Ryan! I'm a French mathematician working in Orsay. Would you care to tell us how you heard about Lean?

[Sebastian Graf]

Hi, I'm a PhD student in Karlsruhe with strong interest in functional programming. Although I'm mostly into GHC middle-end stuff, I really like type systems and would spend more time (well, if I had more time to spend) formalizing things, preferrably in Lean :)

[Johan Commelin]

Welcome! Karlsruhe is not too far from Freiburg (-; Have you seen https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/LUG.20Freiburg.202018 ?

[Sebastian Graf]

Sounds interesting! I'm afraid I won't be able to make it due to the usual busy stuff during semester.

[Agnishom Chattopadhyay]

Hi;

I am Agnishom. I am an undergraduate student of Mathematics and Computer Science. I am interested in Logic in general.

Can somebody help me figure out how to install lean and configure emacs on my system?

[Alistair Tucker]

I suggest homebrew if you are on a mac

[Agnishom Chattopadhyay]

I am on linux mint

[Kevin Buzzard]

https://xenaproject.wordpress.com/2017/12/02/how-to-install-mathlib-and-keep-it-up-to-date/

[Kevin Buzzard]

Does that help? Are there some instructions somewhere on github? I forget.

[Robert Kornacki]

Hi there, I've just started going through Theorem Proving In Lean and I've got to say I've really been enjoying using it. I come from a functional programming background, and when I tried out Idris earlier this year I really got a pull into the dependent type world. Lean has been a joy to use thus far in comparison to Idris for the very small reason that it's impeccably fast for displaying goals & holes making the whole process feel really smooth rather than a little clunky (though I do enjoy Idris' ability to name holes). Out of curiosity, does anyone know of any performance comparisons of Lean vs Idris, would be neat to know.

[Andrew Ashworth]

Seeing as how Idris allows for code extraction to C, and is a language very much more focused on programming, I can't imagine the comparison being very favorable. When Lean 4 rolls around, that'll be a more interesting comparison since there will be easy interop with C++

[Reid Barton]

And ordinary lean programs will be compiled/JITted, as I understand it, rather than run in a VM like today

[Simon Winwood]

Hi All, I am a research engineer at Galois. I am mainly used to Isabelle, and less-so Coq. I am mainly interested in program verification, but also am keen on theorem proving in general.

[Simon Hudon]

Hi Simon! Welcome to Lean! I was an intern at Galois last year and that's actually where I first started using Lean. I got hooked.

[Simon Winwood]

Ah, I thought I recognised your name,

[David Michael Roberts]

Hello all. I've been following UF/HoTT/proof assistants as a lurker since the special year at the IAS. I'm in category theory/differential geometry/topos theory. I have some non-commutative algebra constructions (groupoid/category algebras) that I'd like to have a crack at formalising, as I warm up to learning about serious C*-algebra stuff (don't think I'd formalise that, but who knows...)

[Kevin Buzzard]

By far the best way to learn how to use the software is to just decide that you're going to try formalising X (rather than X and Y and Z and W) and then ask on the forum with a precise reference of what you're aiming at, and you'll get comments either of the form "this is done" or "this is feasible, start like this" or "this is way too hard, you'll first need to do X' so if you're still interested in then start there".

[David Michael Roberts]

OK, thanks. :-)

[Kevin Buzzard]

...although probably reading Theorem Proving In Lean might help too. I was planning on writing docs for mathematicians over the summer, but my mathematicians didn't really seem to need docs, they asked each other questions (or me) and got stuck on things which wouldn't necessarily be covered in the docs I was planning on writing, so I didn't write them. I might have to write them next month when I have far more students than I can talk to individually.

[Kevin Buzzard]

I guess even if you don't plan on formalising something, you could still state more precisely what you might be interested in formalising and the community might offer comments.

[Scott Morrison]

Welcome, David! It's fun here. :-)

[David Michael Roberts]

Well, given a small groupoid and a field, I want to construct the convolution algebra on the vector space with basis the arrows of that groupoid, and also construct the multiplier algebra of such a beast. I guess I would need:

fields
vector spaces
algebras
small groupoids
modules and their maps

I'll have to have a dig through mathlib to see what's there already, but I imagine a bunch of those (if not small groupoids) have been done.

[Mario Carneiro]

We have all of those except algebras and groupoids, although we have categories so it's not hard to state what a groupoid is.

[Reid Barton]

I have (small) groupoids in another project already which I could PR

[Reid Barton]

It's the most basic possible thing, but should get you started

[Mario Carneiro]

what is the convolution algebra?

[Mario Carneiro]

I guess the elements of the algebra are linear combinations of arrows of the groupoid, and multiplication involves the composition of arrows somehow?

[Kevin Buzzard]

what is an algebra in this context? The word is used in so many ways. In commutative ring theory "A is a B-algebra" is simply a long-winded say of saying f : B -> A

[David Michael Roberts]

Mario: Correct. Multiplication is the bilinear extension of f*g = f\circ g (if composable), 0 (if not)

[David Michael Roberts]

Kevin: a vector space with an associative bilinear multiplication—and I'm not going to assume unital.

[Kevin Buzzard]

Well making this definition is trivial, but Lean doesn't quite work like that; one also has to make a basic API for the definition, which means proving 20 trivial lemmas about it

[Kevin Buzzard]

and giving them names which computer scientists find acceptable

[Kevin Buzzard]

(something which I was initially skeptical about but now have very much come around to)

[Sean Leather]

computer scientists Mario and Johannes

[Kevin Buzzard]

Apologies for bad-mouthing the CS community in general :-)

[Johan Commelin]

Here a question that I don't know how to answer: are Lie algebras algebras?

[Johan Commelin]

Bourbaki says: yes

[Kevin Buzzard]

not in general I guess

[Johan Commelin]

But I think Lean will run into trouble with notation...

[Kevin Buzzard]

But it's completely consistent that Bourbaki have a different definition of algebra

[Johan Commelin]

I think if we want to use has_mul then the multiplication must be associative.

[Kevin Buzzard]

the word is used in so many ways. I think I once checked explicitly that the Lie bracket was not associative in general, even though there's a meta-proof of the form "if it were associative in general then someone would have pointed this out by now".

[Johan Commelin]

Otherwise brains will explode

[Kevin Buzzard]

has_mul is just notation, it doesn't have to be associative by definition

[Johan Commelin]

associative Lie brackets are trivial, right? So you get abelian Lie algebras

[Kevin Buzzard]

Notation is a minefield and it's now my opinion that this is to a large extent the fault of mathematics.

[Johan Commelin]

Sure, but non-associative has_mul might even create more problems then your int vs nat woes

[Kevin Buzzard]

We invented notation over the last few hundred years and some of it is awful. Quadratic Reciprocity is a statement about fractions in brackets.

[Johan Commelin]

Somehow even Lean depends on notation. When I first understood that the simplifier relied on notation I was really disturbed.

[Johan Commelin]

But notation seems to be more than just syntactic sugar

[Kevin Buzzard]

Unfolding is an art, this is my understanding of it. If you unfold everything then you have a complete mess which you cannot work with. But notation? Doesn't that just get unfolded by the parser right at square 1 so simp can't even notice it is there?

[Mario Carneiro]

there might be a terminological clash here - has_mul and such are often called "notation typeclasses" since they have a notation associated to them, but obviously simp knows about has_mul, even if it doesn't know that * is used to draw it

[Johan Commelin]

Aaah, so we can drop the associativity condition

[Johan Commelin]

And make [X,Y] notation for Lie_algebra.mul X Y

[Johan Commelin]

It's really sad that we can't bind notation to namespaces...

[Johan Commelin]

@Mario Carneiro Do you think this is a viable strategy? To have algebra and then is_unital, is_assoc, is_comm, etc...

[Johan Commelin]

Where algebra just means bilinear multiplication on a module.

[Mario Carneiro]

ironically, there is already is_comm, is_assoc etc in @[algebra]

[Mario Carneiro]

but I think that means something different

[Johan Commelin]

What do they mean?

[Mario Carneiro]

it is not bound to a notation

[Johan Commelin]

Ok, but we could have has_mul.is_assoc etc, right?

[Mario Carneiro]

what's the use case?

[Johan Commelin]

Well, there are entire fields of mathematics that work with associative algebras

[Johan Commelin]

But there are also entire books about non-associative algebras

[Mario Carneiro]

but you don't want to use * for them, right?

[Johan Commelin]

Sometimes the associative algebras are unital, and/or commutative

[Johan Commelin]

Why not use *?

[Mario Carneiro]

that's whatever

[Johan Commelin]

My proposal is to use has_mul for all of them

[Mario Carneiro]

If you want to use *, go ahead and define your typeclass based on has_mul

[Johan Commelin]

And then only for Lie algebras introduce a second notation, namely [X,Y] instead of X * Y

[Mario Carneiro]

the danger is if you need a conventional mul and also a lie bracket thing at the same time

[Johan Commelin]

I have never heard of that before

[Johan Commelin]

Ah, I do

[Johan Commelin]

Hmmm... that's nasty

[Johan Commelin]

Every ring gives a Lie algebra, via the commutator bracket

[Mario Carneiro]

yeah you probably don't want to confuse those

[Johan Commelin]

Hmmm... so we have algebra without notation. Just the op. And then assoc_algebra gets has_mul, and Lie_algebra gets has_bracket. Could that work?

[Johan Commelin]

Hmm... but then there would still be two instances of algebra on every ring.

[Johan Commelin]

And they aren't even equal.

[Mario Carneiro]

What about a translation wrapper like multiplicative?

[Johan Commelin]

What would that do?

[Mario Carneiro]

change the notation

[Mario Carneiro]

so you could develop the theory on has_mul, and then transfer any results to the has_bracket version

[Johan Commelin]

Ok, but then, suppose we have [ring R], this would give [algebra R]. And then? Something like [Lie_algebra (commutator R)]?

[Chris Hughes]

Isn't semigroup has_mul.assoc?

[Kevin Buzzard]

Yeah but the Lie algebra associated to a ring is a second "multiplication", defined as [a,b] = a*b-b*a. This is not associative.

[Kevin Buzzard]

It's not even a multiplication really, this conversation was started by the observation that Bourbaki apparently claims that Lie algebras are "algebras", whatever that word means.

[Mario Carneiro]

I think this is the wrong thread

[Ryan Smith]

Sorry for the slow response, went on vacation right after learning about Lean :). I read about the verification of Feit-Thompson and I was really impressed that compute checked proofs have come so far that such a thing was possible. That lead to doing a survey of proof checkers, and it seemed that Lean was a much more dynamic community than Coq and some of the others. If I needed any more proof that Lean is legit, seeing Kevin Buzzard here is a pretty strong endorsement.

I actually left academia a couple years ago for industry, and I've been thinking about find project that would allow me to be more involved with math and work on something that would useful to the community.

[Matthew Ballard]

Hi everyone. My name is Matthew Ballard. Currently I am based in South Carolina. I am teaching an intro to proofs course here in the fall which is following Jeremy's lead. I am also working on a proposal for an REU based whose theme formal verification in Lean of results on Noether's Problem (given G acting on k(x_1,...,x_d) is k(x_1,...,x_d)^G purely transcendental). The hope is to develop enough over the course of 3 years to produce a formal verification of Saltman's counterexample(s) over \C. I have been looking through mathlib to help plot a feasible course for this. I welcome any and all advice.

[Patrick Massot]

Welcome! Do you already know how to use Lean, or do you intend to learn now?

[Patrick Massot]

In case you need to learn or have colleagues who'd like to learn, have you heard of https://leanprover-community.github.io/lftcm2020/?

[Matthew Ballard]

Thanks. My level: the tutorials, the natural number game, and the exercises in Jeremy's online text. I've 'registered' for the conference myself also. Not helpless but still a novice.

[Patrick Massot]

Which one do you call Jeremy's online text? He is a rather prolific author of useful texts.

[Matthew Ballard]

Good point. https://leanprover.github.io/logic_and_proof/

[Matthew Ballard]

The community as a whole seems quite inviting and committed to supporting learning - which is greatly appreciated.

[Patrick Massot]

Ok, I thought you meant that one, but there are others.

[Matthew Ballard]

Yeah. I've encountered and browsed some.

[Matthew Ballard]

One precise question: what other repositories exist that might not yet (or never) be merged into mathlib?

[Patrick Massot]

Do you mind helping to evaluate the workshop communication? Could you please tell us whether the following was clear to you when reading the website:

• given what you just wrote, you can probably skip Monday and Tuesday and still enjoy Wednesday to Friday
• if you feel like helping others, you could come on Monday and Tuesday and help
• you could try to follow the alternative Monday afternoon about meta-programming, it would probably be quite tough but it wouldn't be a problem for the rest of the week.

[Matthew Ballard]

I would say those were clear.

[Patrick Massot]

About other repositories, you can get some answers by browsing https://leanprover-community.github.io/papers.html (or even the excerpt at the bottom of the home page). For instance that would tell you about the cap set repo, perfectoid spaces repo, continuum hypothesis repo.

[Rob Lewis]

Matthew Ballard said:

One precise question: what other repositories exist that might not yet (or never) be merged into mathlib?

@Kevin Buzzard 's Xena repo is one, I don't have the link handy. The published projects are mostly covered by Patrick's links.

[Patrick Massot]

Great, thanks Matthew.

[Patrick Massot]

Reid probably also has hidden treasures.

[Patrick Massot]

https://github.com/rwbarton/lean-homotopy-theory

[Matthew Ballard]

Thanks. I know from @Kevin Buzzard blog and locating the subsequent papers that group cohomology exists. Would anyone care to comment on the development of Galois theory?

[Adam Topaz]

This discussion happened recently:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Is.20there.20code.20for.20Galois.20theory.3F

[Bhavik Mehta]

Matthew Ballard said:

One precise question: what other repositories exist that might not yet (or never) be merged into mathlib?

A couple more things here - there's my combinatorics and topos theory repos which are very slowly being merged, and also Neil Strickland has a nontrivial maths repo too (which might be out of date)

[Kevin Buzzard]

One of my jobs this summer is to work on the schemes repository again