How to get a quick overview of what's proved?

Stream: new members

[Joseph Corneli]

Hi, I'm new to Lean. Specifically, I'm working my way through Chapter 3 of "Theorem Proving in Lean" at the moment, having also installed mathlib and and the xena-UROP-2018 work in progress. Is there an efficient and meaningful way to get an overview of what has been proved in Lean to date? I've run find ./ | xargs grep "theorem" in the mathlib directory, and adding a grep -c "." tells me roughly how many theorems have been proved, but the data is otherwise a bit hard to navigate. It occurs to me that perhaps this question is most conveniently asked relative to some extrinsic knowledge base or bases, though something intrinsic, like the pictures of the Linux Kernel, would also be interesting. In addition to studying the TPiL book, it's also nice to learn by reading the source. I look forward to getting to the point where I can contribute!

[Kenny Lau]

welcome

[Joseph Corneli]

Thanks!

[Kenny Lau]

you can look at the names of the files if you want to know what is in Lean... other than that I don't really know.

[Patrick Massot]

At some point @Kevin Buzzard started to try to document this at https://github.com/leanprover/mathlib/blob/master/docs/theories.md, with some help from Chris. But it didn't go very far. You're welcome to contribute to this effort!

[Joseph Corneli]

@Patrick Massot thanks I'll look (and perhaps add) there. It might be interesting to have a version with "red links" (like on Wikipedia), to specifically indicate the things that people are interested in working on (rather than trying to sum up the totality of all mathematical theories that aren't yet defined).

[Patrick Massot]

Do you mean something like https://github.com/leanprover/mathlib/blob/master/docs/wip.md?

[Patrick Massot]

We should update it by the way

[Joseph Corneli]

Yes that's what I meant by "red links", thanks.

[Sean Leather]

Do you mean something like https://github.com/leanprover/mathlib/blob/master/docs/wip.md?

@Patrick Massot Thanks for pointing that out. I PR'd an update to add myself.

[Patrick Massot]

We could even have a list of results that are very much proved: https://github.com/leanprover/mathlib/issues/216

[Kevin Buzzard]

Brief overview: it's a bit random. Let me stick to maths. For example in ring theory we have rings, modules, and for commutative rings we have localisation, tensor products, and some stuff about Spec of a ring. There's currently a debate ranging about what the correct definition of Euclidean domain should be. For vector spaces we don't even have the equivalence between finite-dimensional vector spaces and k^n and all the consequences (linear maps = matrices etc); we don't have det(AB)=det(A)det(B) or anything like that -- we don't have signature of a permutation. On the other hand we have a bunch of stuff on Pell's equation and on Matiyesevich's proof that Diophantine = r.e. . For measure theory there is a whole bunch of stuff on measurable subsets of the reals -- however we don't have the definition of a differentiable function from R to R. No exp or sin or cos (although there is a PR), no proof that exp is continuous. I should say that I'm sticking here to what's in mathlib -- there are a bunch of random other things floating around, e.g. I have some repo which claims to define schemes (and even prove that an affine scheme is a scheme), and a bunch of students at Imperial College are working on completely random things (like finite-dimensional vector spaces, Sylow's theorems [done], fundamental groups). We're trying for perfectoid spaces but it's been slow going recently.

[Kevin Buzzard]

Oh -- topology, there's stuff like completeness and compactness and various basic facts about these things. One vague aim of mine is to make coverage of the basics (by which I mean the material covered in the pure maths course in the first year or two of a university maths course) a little more consistent. Although I've heard terrifying things about the Cauchy integral formula...

[Joseph Corneli]

Hi @Kevin Buzzard thanks for the comprehensive answer! I've found another answer that's less comprehensive, but integrated with Lean in an interesting way: https://hanoifabs.wordpress.com/2018/06/14/mario-lean-catalog-june-13-2018/ -- I'm on Emacs, and browsing the file there with a Lean+mathlib installation causes lots of informative messages to appear in the *Flycheck errors* buffer.

[Mario Carneiro]

It just so happens that I am presenting a talk today at ICMS which aims to answer exactly this question, so hopefully you will have some more stuff to look at soon

[Patrick Massot]

Great!

[Patrick Massot]

Do you have slides of your talks? I was just reminded of ICMS because a colleague attending ICMS just emailed me to tell he heard of a Lean conference in Amsterdam that I might be interested in :smile:

[Simon Hudon]

I used Leo's slides from his Oxford talk as an introduction and the rest of the talk happened in emacs

[Simon Hudon]

I'm really unhelpful, aren't I?

[Mario Carneiro]

That would be Rob's talk, which ended with an ad for Lean Together

[Patrick Massot]

This was my guess indeed