projects-using-mathlib

Stream: general

[Daniel Selsam]

I see that flypitch and lean-perfectoid-spaces live outside the mathlib repo. Are there any other big formalization projects that live elsewhere besides these two?

[Mario Carneiro]

I have a partial CompCert port (very old/outdated) on my GitHub, as well as a preservation and progress type safety proof for C0. These kinds of things tend to bit-rot though without a connection to mathlib to keep them alive

[Mario Carneiro]

There is also lean-stacks-project and its descendent lean-scheme

[Mario Carneiro]

There is of course the lean 2 HoTT library, as well as the lean 3 port; I don't know whether you are only looking for recent work

[Daniel Selsam]

@Mario Carneiro Thanks. I had no idea you had started porting CompCert. Wow, ambitious. My goal right now is just to visualize the mathlib&friends instance graph, so the programming language projects are less relevant to my current inquiry.

[Mario Carneiro]

It was a very early project, on Leo's recommendation. Mostly it taught me that C is a crazy language

[Daniel Selsam]

Mostly it taught me that C is a crazy language

Indeed :)

[Mario Carneiro]

I wouldn't guess that the global instance graph is much bigger than mathlib's. lean-perfectoid-spaces will probably be the biggest extension to that. I think Reid has some category theory library somewhere that might also involve a bunch of new instances? Also possibly Scott, although I think most of his work is now in mathlib

[Daniel Selsam]

@Mario Carneiro I suppose I will just start with mathlib for now. Thanks very much for your responses.

[Jesse Michael Han]

oh yeah, there's also reid's homotopy theory library

[Alex J. Best]

https://github.com/johoelzl/mason-stother and https://github.com/NeilStrickland/lean_lib come to mind

[Rob Lewis]

There's also https://github.com/lean-forward/cap_set_problem (which is relatively small).

[Simon Hudon]

@Daniel Selsam I'm in the planning phase of a stackage-like package repository. Having a central depot of package might make things easier for you. Right now, I'm wondering what service / technology to use to build all the projects. Do you have anything at your disposition?

[Daniel Selsam]

@Simon Hudon I have no insight here. For my inquiry last night, just an updated-once-a-month list of projects using mathlib (with their approximate statuses) on the GitHub README would have sufficed.