Zulip Chat Archive

Stream: new members

Topic: Introductions


view this post on Zulip Xita Meyers (Sep 06 2018 at 12:48):

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.

view this post on Zulip Kenny Lau (Sep 06 2018 at 12:48):

Welcome!

view this post on Zulip Xita Meyers (Sep 06 2018 at 12:49):

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

view this post on Zulip Johan Commelin (Sep 06 2018 at 12:50):

Welcome Xita! Nice to meet you.

view this post on Zulip Johan Commelin (Sep 06 2018 at 12:50):

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

view this post on Zulip Xita Meyers (Sep 06 2018 at 12:53):

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.

view this post on Zulip Johan Commelin (Sep 06 2018 at 12:59):

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.)

view this post on Zulip Kenny Lau (Sep 06 2018 at 12:59):

or motivation

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 13:09):

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.

view this post on Zulip Xita Meyers (Sep 06 2018 at 15:32):

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

view this post on Zulip Harald Schilly (Sep 06 2018 at 15:43):

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 :-)

view this post on Zulip Patrick Massot (Sep 06 2018 at 15:56):

Welcome Harald!

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 17:06):

@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.

view this post on Zulip Harald Schilly (Sep 06 2018 at 17:34):

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 ?

view this post on Zulip Johan Commelin (Sep 06 2018 at 17:35):

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

view this post on Zulip Johan Commelin (Sep 06 2018 at 17:36):

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

view this post on Zulip Mario Carneiro (Sep 06 2018 at 17:36):

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

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 17:41):

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.

view this post on Zulip Tobias Grosser (Sep 07 2018 at 05:35):

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.

view this post on Zulip Tobias Grosser (Sep 07 2018 at 05:36):

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

view this post on Zulip Tobias Grosser (Sep 07 2018 at 05:36):

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

view this post on Zulip Tobias Grosser (Sep 07 2018 at 05:37):

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

view this post on Zulip Tobias Grosser (Sep 07 2018 at 05:38):

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

view this post on Zulip Simon Hudon (Sep 07 2018 at 05:39):

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

view this post on Zulip Tobias Grosser (Sep 07 2018 at 05:40):

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

view this post on Zulip Simon Hudon (Sep 07 2018 at 05:42):

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

view this post on Zulip Simon Hudon (Sep 07 2018 at 05:43):

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

view this post on Zulip Tobias Grosser (Sep 07 2018 at 05:48):

That's great.

view this post on Zulip Tobias Grosser (Sep 07 2018 at 05:48):

Let me know when you are back in Zurich

view this post on Zulip Simon Hudon (Sep 07 2018 at 05:49):

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

view this post on Zulip Corey Richardson (Sep 08 2018 at 05:15):

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!

view this post on Zulip Ryan Smith (Sep 21 2018 at 04:56):

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.

view this post on Zulip Johan Commelin (Sep 21 2018 at 04:56):

Cool, welcome! Where are you based?

view this post on Zulip Johan Commelin (Sep 21 2018 at 04:57):

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

view this post on Zulip Tobias Grosser (Sep 21 2018 at 06:08):

Welcome Ryan.

view this post on Zulip Tobias Grosser (Sep 21 2018 at 06:08):

Researcher at ETH Zurich here!

view this post on Zulip Patrick Massot (Sep 21 2018 at 07:06):

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

view this post on Zulip Sebastian Graf (Sep 21 2018 at 08:53):

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 :)

view this post on Zulip Johan Commelin (Sep 21 2018 at 09:02):

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

view this post on Zulip Sebastian Graf (Sep 21 2018 at 12:17):

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

view this post on Zulip Agnishom Chattopadhyay (Sep 21 2018 at 14:08):

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?

view this post on Zulip Alistair Tucker (Sep 21 2018 at 14:15):

I suggest homebrew if you are on a mac

view this post on Zulip Agnishom Chattopadhyay (Sep 21 2018 at 14:20):

I am on linux mint

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 17:31):

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

view this post on Zulip Kevin Buzzard (Sep 21 2018 at 17:32):

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

view this post on Zulip Robert Kornacki (Sep 21 2018 at 18:42):

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.

view this post on Zulip Andrew Ashworth (Sep 21 2018 at 20:00):

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++

view this post on Zulip Reid Barton (Sep 21 2018 at 20:35):

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

view this post on Zulip Simon Winwood (Sep 24 2018 at 22:03):

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.

view this post on Zulip Simon Hudon (Sep 25 2018 at 00:35):

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.

view this post on Zulip Simon Winwood (Sep 25 2018 at 03:46):

Ah, I thought I recognised your name,

view this post on Zulip David Michael Roberts (Sep 27 2018 at 11:23):

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...)

view this post on Zulip Kevin Buzzard (Sep 27 2018 at 11:54):

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".

view this post on Zulip David Michael Roberts (Sep 27 2018 at 12:29):

OK, thanks. :-)

view this post on Zulip Kevin Buzzard (Sep 27 2018 at 15:50):

...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.

view this post on Zulip Kevin Buzzard (Sep 27 2018 at 15:52):

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.

view this post on Zulip Scott Morrison (Sep 27 2018 at 21:55):

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

view this post on Zulip David Michael Roberts (Sep 27 2018 at 22:45):

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.

view this post on Zulip Mario Carneiro (Sep 27 2018 at 22:48):

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

view this post on Zulip Reid Barton (Sep 27 2018 at 22:48):

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

view this post on Zulip Reid Barton (Sep 27 2018 at 22:48):

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

view this post on Zulip Mario Carneiro (Sep 27 2018 at 22:49):

what is the convolution algebra?

view this post on Zulip Mario Carneiro (Sep 27 2018 at 22:50):

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

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:08):

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

view this post on Zulip David Michael Roberts (Sep 28 2018 at 08:23):

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

view this post on Zulip David Michael Roberts (Sep 28 2018 at 08:24):

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

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:27):

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

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:27):

and giving them names which computer scientists find acceptable

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:28):

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

view this post on Zulip Sean Leather (Sep 28 2018 at 08:28):

computer scientists Mario and Johannes

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:28):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:29):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:29):

Bourbaki says: yes

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:29):

not in general I guess

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:29):

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

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:29):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:31):

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

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:31):

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".

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:31):

Otherwise brains will explode

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:31):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:31):

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

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:32):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:32):

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

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:32):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:34):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:34):

But notation seems to be more than just syntactic sugar

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 08:37):

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?

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:38):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:39):

Aaah, so we can drop the associativity condition

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:40):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:40):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:45):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:45):

Where algebra just means bilinear multiplication on a module.

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:46):

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

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:46):

but I think that means something different

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:46):

What do they mean?

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:46):

it is not bound to a notation

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:46):

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

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:47):

what's the use case?

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:47):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:47):

But there are also entire books about non-associative algebras

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:47):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:47):

Sometimes the associative algebras are unital, and/or commutative

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:48):

Why not use *?

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:48):

that's whatever

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:48):

My proposal is to use has_mul for all of them

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:48):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:48):

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

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:48):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:49):

I have never heard of that before

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:49):

Ah, I do

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:49):

Hmmm... that's nasty

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:49):

Every ring gives a Lie algebra, via the commutator bracket

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:49):

yeah you probably don't want to confuse those

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:50):

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?

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:51):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:51):

And they aren't even equal.

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:51):

What about a translation wrapper like multiplicative?

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:52):

What would that do?

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:52):

change the notation

view this post on Zulip Mario Carneiro (Sep 28 2018 at 08:53):

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

view this post on Zulip Johan Commelin (Sep 28 2018 at 08:54):

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

view this post on Zulip Chris Hughes (Sep 28 2018 at 09:07):

Isn't semigroup has_mul.assoc?

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 09:08):

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.

view this post on Zulip Kevin Buzzard (Sep 28 2018 at 09:09):

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.

view this post on Zulip Mario Carneiro (Sep 28 2018 at 09:34):

I think this is the wrong thread

view this post on Zulip Ryan Smith (Oct 01 2018 at 03:46):

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.

view this post on Zulip Matthew Ballard (Jul 07 2020 at 14:32):

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.

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:34):

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:35):

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

view this post on Zulip Matthew Ballard (Jul 07 2020 at 14:37):

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.

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:38):

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

view this post on Zulip Matthew Ballard (Jul 07 2020 at 14:38):

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

view this post on Zulip Matthew Ballard (Jul 07 2020 at 14:40):

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:40):

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

view this post on Zulip Matthew Ballard (Jul 07 2020 at 14:41):

Yeah. I've encountered and browsed some.

view this post on Zulip Matthew Ballard (Jul 07 2020 at 14:43):

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

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:44):

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.

view this post on Zulip Matthew Ballard (Jul 07 2020 at 14:47):

I would say those were clear.

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:47):

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.

view this post on Zulip Rob Lewis (Jul 07 2020 at 14:48):

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.

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:48):

Great, thanks Matthew.

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:49):

Reid probably also has hidden treasures.

view this post on Zulip Patrick Massot (Jul 07 2020 at 14:49):

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

view this post on Zulip Matthew Ballard (Jul 07 2020 at 14:54):

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?

view this post on Zulip Adam Topaz (Jul 07 2020 at 14:56):

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

view this post on Zulip Bhavik Mehta (Jul 07 2020 at 15:01):

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)

view this post on Zulip Kevin Buzzard (Jul 07 2020 at 18:08):

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


Last updated: May 14 2021 at 22:15 UTC