Replacing Git+GitHub

Stream: general

[Michael Nahas]

To become a contributor to mathlib, interested mathematicians must learn 3 tools: Lean, Zulip, and Git/GitHub. Git/GitHub are complicated and off-putting for mathematicians. It means fewer new mathematicians will contribute to mathlib. Moreover, those that have learned the 3 tools, make fewer contributions too, both because is a chore to use Git/GitHub and because those experienced contributors spend time teaching new people Git or answering their questions about Git/GitHub.

I think we can do better than Git/GitHub and I'm going to be submitting an NSF grant proposal on March 3rd to research a repository design for formal math. My basic idea is that the repository will store every proof ever written. That is, if you write a proof in Lean, it will be automatically added to the repository. Nothing would ever get lost. Proofs can then be searched for the theorem/type, and probably by tags/keywords associated with them.

"mathlib" --- the curated set of theorems and proofs that work well together and are the common language of formal math --- would be a subset of all theorems and proofs, and live in its own namespace. To add a theorem/proof to mathlib would be just assigning a name to it. And assigning a name should be a simpler operation than merging a pull request on GitHub .

I believe there are plenty of ideas to research in the space and a real practical benefit to be gained if something results. I'd love to hear people's thoughts on the idea.

[Ruben Van de Velde]

I use git/github for my day job, so my perspective is obviously skewed, but I think using well-known tools with an extensive ecosystem built around them is one of the main advantages of the current setup. I don't know if I'd have started contributing if mathlib was built in a completely custom ecosystem

[Oliver Nash]

Michael Nahas said:

if you write a proof in Lean, it will be automatically added to the repository.

It's not clear to me how this would work. Do you have something concrete in mind?

[Patrick Massot]

@Michael Nahas could you clarify how this question is related to what is written on your webpage:

In January of 2022, I started a business ProofShare. It's goal it to help mathematicians share formal proofs online.

Are you trying to sell us something? Or is it a strange way of asking us what we would be ready to buy?

[Ruben Van de Velde]

(And I don't even like git)

[Jireh Loreaux]

Just because mathematicians are unfamiliar with Git doesn't mean that's good for them. I've given several talks to mathematicians about using Git for their current research (i.e., for using version control for LaTeX manuscripts), and these seemed to be received favorably.

[Stuart Presnell]

Yeah, having a tool that's designed for hosting and jointly working on files of arbitrary type, rather than specifically proofs, means that the skills used in learning to use GitHub can be transferred to other files such as LaTeX documents. For similar reasons, many mathematicians may already have these skills, having learned them for other purposes, whereas no users will come to a brand new custom-made system with pre-established skills.

[Jireh Loreaux]

Michael Nahas said:

My basic idea is that the repository will store every proof ever written. That is, if you write a proof in Lean, it will be automatically added to the repository. Nothing would ever get lost. Proofs can then be searched for the theorem/type, and probably by tags/keywords associated with them.

That sounds like a search query nightmare. Hundreds of different versions of the theorem you want, all with slightly different hypotheses, and maybe the one you really want doesn't even show up in your search. Mathlib is a carefully curated collection of results with relatively uniform rules concerning naming, and even contributors still have trouble finding existing theorems. We have a whole stream "Is there code for X?" on Zulip dedicated to this purpose. I don't see how such a disorganized system can be useful. From my (admittedly limited) experience, one of the historical problems with formalized mathematics is interoperability. If you keep every theorem every proven, then you have essentially zero interoperability. Moreover, what about naming, or definitions? I don't understand how this would address any of these problems.

[Stuart Presnell]

Moreover, you complain that newcomers need to learn to use GitHub, but presumably some amount of effort would have to be spent in learning how to use your alternative system. Being a new and much less widely used system there will be orders of magnitude fewer resources for learning, and no counterpart to the huge community of GitHub users on e.g. Stack Overflow (which currently has around 30,000 answered questions tagged github).

[Stuart Presnell]

Another thing to consider is the integration in other software. For example, one of the more commonly used editors here is Visual Studio Code, which has extensive GitHub integration.

[Michael Nahas]

@Oliver Nash There are various ways a proof could be automatically added to the repository. The code doing the adding could be part of an editor. E.g., if VSCode sees a successful proof, it could submit it. Or, it could be a background process that monitors Lean files and, if one is changed, passes it to Lean and submits any successful proofs to the repository.

[Stuart Presnell]

Sorry that you've come here to present your idea and received nothing but a barrage of negative responses! I'm sure there are lots of us who also don't like GitHub and can imagine ways in which a hypothetical alternative could be better. But a lot of practical considerations such as those outlined above make it very difficult to migrate to another system, especially a brand new one.

[Frédéric Dupuis]

Michael Nahas said:

Oliver Nash There are various ways a proof could be automatically added to the repository. The code doing the adding could be part of an editor. E.g., if VSCode sees a successful proof, it could submit it. Or, it could be a background process that monitors Lean files and, if one is changed, passes it to Lean and submits any successful proofs to the repository.

This sounds like a recipe for disaster: while coding a proof, one routinely produces drafts that do compile but that are nowhere close to being presentable yet. We definitely wouldn't want those in a public repository.

[Stuart Presnell]

Michael Nahas said:

E.g., if VSCode sees a successful proof, it could submit it. Or, it could be a background process that monitors Lean files and, if one is changed, passes it to Lean and submits any successful proofs to the repository.

How would you distinguish what counts as a distinct proof? If I write a first draft proof that's messy and ugly, and then go through five rounds of re-writing it to tidy it up, does that count as six different proofs that should each be uploaded to the repository? I can't see how you could automatically discriminate in a suitable way. But then that only leaves manual submission of proofs that the user considers ready, which is what we have already.

[Jireh Loreaux]

Yes, this would mean there aren't hundreds of versions, but thousands. And how do you keep track of dependencies? Do you just store the proof term, or the sequence of tactics that produced it? If the former, yuck; if the latter, what about changes to the tactics themselves (e.g., the simp list)?

[Oliver Nash]

Michael Nahas said:

Oliver Nash There are various ways a proof could be automatically added to the repository. The code doing the adding could be part of an editor. E.g., if VSCode sees a successful proof, it could submit it. Or, it could be a background process that monitors Lean files and, if one is changed, passes it to Lean and submits any successful proofs to the repository.

Although I have concerns about what you have outlined, I salute the idea of trying to improve workflows. I think that an easier way to help might be something less drastic which targets particular frictions. For example there is a Firefox extension Refined GitHub that I believe several people here use. Perhaps you might consider it as a model and customising it for the Lean / Mathlib workflows.

[Michael Nahas]

@Patrick Massot I'm applying for a "Small Business Innovative Research" (SBIR) Grant from the NSF. The program's goal is to get technology out of the labs and into the hands of users. I'd like to help formal math get out of the lab, where it has been stuck for 50 years.

I need a business to apply for the grants. I don't know if there's a place for a business in formal math. But if there is, any future product would probably sold to people who use math: scientists and engineers. There are millions of them and only 80,000 mathematicians. So, no, I am not trying to sell you anything or asking you what you would be willing to buy. I'm trying to figure out how to be useful to the community, which should also let me win the grant.

[Yakov Pechersky]

Formal verification has a huge industry impact for chip design for CPUs and GPUs. There is a lot of tooling for versioning, testing, integrating, working with changing specs from chip manufacturers. You can take a look at Cadence (https://www.cadence.com/en_US/home/training/all-courses/82110.html) which seeks to be a one-stop-shop for handling all of these aspects.

[Michael Nahas]

@Oliver Nash My potential funding is from a research grant. I doubt that "improving workflows" would qualify as research. If the Hoskinson Center for Formal Math wants to fund me to improve workflows, I'm game.

[Michael Nahas]

@Jireh Loreaux @Stuart Presnell @Frédéric Dupuis Yes, the respository would hold lots of ugly proofs. Possibly thousands more than would show in mathlib. mathlib would be a subset that would be curated --- well named and designed to work together.

But, if you only care if a proof exists, it doesn't matter if it is "presentable". If someone at any place, at any time has proven what you want to prove, you're done. In each significant proof, there are many more little lemmas that don't deserve names but show up in proofs on a subject. A "repository of every proof" will hold those and prevent duplicated work.

[Yakov Pechersky]

Michael, how would your tool work with something like metamath? That database has a nice way of tracking the versions of proofs, and how they become obsolete. Metamath also has a very different tooling than Lean does.

[Eric Wieser]

But, if you only care if a proof exists, it doesn't matter if it is "presentable". If someone at any place, at any time has proven what you want to prove

The problem is that libraries of formalized mathematics aren't just proofs, they're definitions too. If you use a different definition of nat in your statement than "someone" did in the proofs you were hoping to use, then all their proofs about nat are useless to you.

Mathlib has 32780 definitions, for reference.

[Michael Nahas]

Jireh Loreaux said:

And how do you keep track of dependencies? Do you just store the proof term, or the sequence of tactics that produced it? If the former, yuck; if the latter, what about changes to the tactics themselves (e.g., the simp list)?

That's what makes this research. ;) Yes, there are arguments for storing either and, possibly, both. Perhaps it will be compressed content-addressed proof-terms. Perhaps it will be proof states and the tactics (with some encoding of dependencies) that map between them. There will probably have to be some accommodation for definitions too.

Another aspect is optimizations to have queries match the data being stored. If someone proves "A and B" and it is stored in the repository, can you make sure that someone who queries for "B and A" finds it?

[Marc Huisinga]

I think I'd feel uncomfortable if a tool immediately synced code of mine (even if it's a proof) into a global and immutable (?) database. Discomfort aside, what about licenses?

[Michael Nahas]

Eric Wieser said:

The problem is that libraries of formalized mathematics aren't just proofs, they're definitions too. If you use a different definition of nat in your statement than "someone" did in the proofs you were hoping to use, then all their proofs about nat are useless to you.

I don't worry about that problem. The dependencies can be stored with a proof in such a way that naming would not matter. So, if two people use two different definitions of "nat", but with the same name, the repository can tell them apart.

On the other hand, I do worry that if two people were using two different definitions of "nat" and the definitions are isomorphic. Then, we'd want the repository to be able to find a proof of one "nat" and return a modified version of that proof that works with the other "nat". That is a much harder problem.

[Michael Nahas]

Marc Huisinga said:

I think I'd feel uncomfortable if a tool immediately synced code of mine (even if it's a proof) into a global and immutable (?) database. Discomfort aside, what about licenses?

Obviously, the syncing could be controlled by the user. They can turn it off if they want.

As for licenses, that's something to worry about when I get something running. Obviously, it would be written to encourage people to add proofs to the repository. Ideally, it would funnel money from people querying for theorems to the people adding them to the repository.

[Michael Nahas]

Yakov Pechersky said:

Michael, how would your tool work with something like metamath? That database has a nice way of tracking the versions of proofs, and how they become obsolete. Metamath also has a very different tooling than Lean does.

For the grant, I would focus on Lean. It has the momentum behind it. I don't know Metamath, but the ideas that I am thinking of would work for Coq and Agda.

[Eric Wieser]

On the other hand, I do worry that if two people were using two different definitions of "nat" and the definitions are isomorphic. Then, we'd want the repository to be able to find a proof of one "nat" and return a modified version of that proof that works with the other "nat". That is a much harder problem.

Right, this is what I was trying to draw attention to. Your library becomes useless if every proof about nat is about a different nat (at the extreme). While nat is a trivial case, showing that two definitions are equivalent can be arbitrarily mathematically involved.

[Marc Huisinga]

Michael Nahas said:

Marc Huisinga said:

I think I'd feel uncomfortable if a tool immediately synced code of mine (even if it's a proof) into a global and immutable (?) database. Discomfort aside, what about licenses?

As for licenses, that's something to worry about when I get something running. Obviously, it would be written to encourage people to add proofs to the repository. Ideally, it would funnel money from people querying for theorems to the people adding them to the repository.

I think I'll stick with Git.

[Mario Carneiro]

also, two definitions can be inequivalent for stupid reasons (like 1/0 equal to 0 or choice real or undefined)

[Henrik Böving]

I feel like the idea of sharing proofs in this way might not be a bad one but having it replace Git/Github is not what this idea should be used for (as others have pointed out above). Your concept of uploading proofs to a database to search for them and having mathlib be one curated list of things is not an alternative for Git/Github IMO, Git/Github is infrastructure we use to work on single project. What you are proposing sounds more like e.g. a crates.io or a pypi.org but for Lean proofs with a simple way to upload new content to it and Mathlib would basically be a meta package consisting of what people think is high quality enough to be put in there.

However even when viewing it from this perspective I see several issues:

• Mathlib was (afaik) on purpose not designed as a meta package for several sub packages because you pretty quickly run into versionining issues like this which is something even software engineers get annoyed by at times and would be a much bigger hassle for mathematicians who just want to get their work done. This is basically the approach Coq has taken.
• Versioning such proofs without something like git also seems like a horrible idea, what if I want to work on a refactor and show people my code but not upload it to the DB because its certainly not ready for that yet? What if I want to update an older version of my proof? How do I people make aware of that?

[Adam Topaz]

At some point a long time ago @Johan Commelin mentioned this experimental programming language where the code was stored in a content-addressable way based on the syntax tree or something like this. Can someone remind me of the name of this language?

[Henrik Böving]

Nix and NixOS?

[Adam Topaz]

No it's not nix.

[Mario Carneiro]

Unison

[Adam Topaz]

I haven't read all of the discussion in this thread, but it does seem that this language has tried (perhaps successfully?) some of what was suggested.

[Arthur Paulino]

How are you planning to deal with the mechanics of what happens with PRs? There is a certain level of intrinsic complexity that Git gracefully resolves for us. I am new here but I see that this community has grown a lot of momentum using the dynamics of branches, PRs, automated CI tests and code reviews. An old PR might eventually conflict with the master branch and this is an unavoidable issue in the realm of asynchronous development.

[Arthur Paulino]

When handling all these details, there's a chance you might end up with something just as complex as Git itself

[Eric Taucher]

My two cents. Just noting the obvious .
Microsoft acquires GitHub
Lean Theorem Prover Microsoft Research

[Mauricio Collares]

I find it hard to believe that Microsoft Research would care about a particular hosting provider, and Lean used GitHub years before it was acquired

[Mario Carneiro]

Also noting the obvious: https://i.imgur.com/XLuaF0h.png

[Patrick Stevens]

Eric Taucher said:

My two cents. Just noting the obvious .
Microsoft acquires GitHub
Lean Theorem Prover Microsoft Research

I'd go so far as to say that GitHub is the industry standard for Git repository hosting; there's GitLab, and then (struggles to keep from laughing) Bitbucket and Sourceforge, and a few self-hosted offerings (of course Git itself is distributed by design). The Wikipedia page on Git even has "Not to be confused with GitHub" at the top. There are other version control systems like Pijul, Bazaar, SVN, but at the moment it's overwhelmingly Git for software engineering.

[Michael Nahas]

Eric Wieser said:

Your library becomes useless if every proof about nat is about a different nat (at the extreme). While nat is a trivial case, showing that two definitions are equivalent can be arbitrarily mathematically involved.

Yes, it becomes useless at the extreme, but is the extreme the likely case? Work coalesces around a particular definition because either it is the easiest to use or someone else has done work with it ... which makes it the easiest to use. It is easiest for everyone to use the same definition. And, when it isn't, there are usually good reasons for that.

[Mario Carneiro]

It's not necessarily easiest for everyone to use the same definition. People have diverging ideas, and you usually get lots of enclaves if you don't do anything special. This is what the Coq ecosystem looks like

[Stuart Presnell]

Michael Nahas said:

Ideally, it would funnel money from people querying for theorems to the people adding them to the repository.

This remark hasn't been commented on, but this scenario seems very far from "ideal". I can imagine that there might be settings where a pay-for-code system based on micro-payments might make sense. A collaborative mathematics library such as mathlib is not one of them.

[Michael Nahas]

Henrik Böving said:

• Mathlib was (afaik) on purpose not designed as a meta package for several sub packages because you pretty quickly run into versionining issues like this which is something even software engineers get annoyed by at times and would be a much bigger hassle for mathematicians who just want to get their work done. This is basically the approach Coq has taken.
• Versioning such proofs without something like git also seems like a horrible idea, what if I want to work on a refactor and show people my code but not upload it to the DB because its certainly not ready for that yet? What if I want to update an older version of my proof? How do I people make aware of that?

What is being updated between "versions"? Is it Lean's syntax? Lean's type theory or kernel? Is it a definition in the library?

As for "not wanting to show people my code because it is not ready", that wouldn't be taken into consideration. Every version of the proof would be inserted into the repository. What you care about is the name in the library --- that is, when someone looks for your proof, how do they find it? When you were ready, you would change the "mathlib:fermats_last_theorem" tag to point to the version you wanted others to use.

[Mario Carneiro]

What is being updated between "versions"? Is it Lean's syntax? Lean's type theory or kernel? Is it a definition in the library?

All of the above, actually (well, the type theory doesn't change much, but the other stuff does)

[Kevin Buzzard]

Sometimes there are huge refactors. The definition of group changed last year.

[Kevin Buzzard]

And both Antoine Chambert-Loir and Chris Hughes independently pointed out to me that we might want to change it again in the future (to add "operators")

[Julian Berman]

I think it's interesting that there are a decent number of other version control systems that are in ways nicer than git. Fossil was a great thing for a few minutes. Mercurial has a few things which are nice about it and still kind of sits on the sidelines churning along. There was some really nice VCS someone invented recently which even has some formal guarantees about it (which I'll have to go find). It's somewhat unfortunate in the software world that git has "won", but I don't know that I understand why mathematicians would need a drastically different class of tool. Certainly there are UX warts and complexities, but I think it's quite tenuous to try to tackle all 3 of version control, collaborative development and content addressing or sharing or whatever you want to call it in one tool.

[Julian Berman]

Even just fixing git's UX issues has been attempted 10 times or more and yet none of the attempts at "smoothing" it out have really caught on too much.

[Mauricio Collares]

Pijul?

[Julian Berman]

Thanks! Indeed that's the one I was trying to remember.

[Michael Nahas]

Mario Carneiro said:

It's not necessarily easiest for everyone to use the same definition. People have diverging ideas, and you usually get lots of enclaves if you don't do anything special. This is what the Coq ecosystem looks like

I believe enclaves develop when it is hard to share and communicate. Still, I can see the need for unity in a large library, like mathlib, which needs a dictator who says "this is the one common definition of X" so that it you don't have K versions of N concepts and end up with K^N different sharded worlds.

[Henrik Böving]

Just from the frontpage alone being focused on patches rather than branches sounds a bit like the git worklow Google's gerrit is enforcing, is it similar to it or should I dig further to get what's the gist here?
Mauricio Collares said:

Pijul?

[Julian Berman]

I don't think it should have much to do with Gerrit (at least what I know of Gerrit).

[Julian Berman]

So I'd say yeah worth a closer look personally, I found it interesting.

[Arthur Paulino]

Michael Nahas said:

Still, I can see the need for unity in a large library, like mathlib, which needs a dictator who says "this is the one common definition of X"

I'd say the community effort that's put into uniformization is being completely overlooked on that statement. I am not a professional mathematician, but I think the process of coming down to agreements is healthy to the development of mathlib. I wouldn't want a dictator saying that my definition would be the one staying in the lib. I would rather see the community changing and improving my definition for the better of the lib itself. It's a process that happens organically because it's too hard to foresee all the consequences of a design choice

[Michael Nahas]

Mario Carneiro said:

What is being updated between "versions"? Is it Lean's syntax? Lean's type theory or kernel? Is it a definition in the library?

All of the above, actually (well, the type theory doesn't change much, but the other stuff does)

Any repository will have to address all 3 changes. But the changes may have very different solutions. A repository that only stored proof-terms in Lean's type theory would be resistant to changes in Lean's syntax, but not to @Kevin Buzzard 's redefinition of a group. A repository storing only tactics would be invalidated if Lean's syntax changed. I have a feeling that the solution will be to store both tactics and the proof-terms and some mapping between them.

[Eric Rodriguez]

this already is quite a large nontrivial problem

[Michael Nahas]

@Arthur Paulino Perhaps my use of the word "dictator" was wrong. All I meant to say was that it was good for a large library to have 1 single version of each concept.

[Mario Carneiro]

That's mathlib's approach, but reasonable minds can disagree about whether that is even a good idea

[Mario Carneiro]

I am reminded of the LATIN project, which was basically a catalog of a thousands of different logics and their interrelations

[Mario Carneiro]

that's embracing the opposite approach, you consider all the ways to define a thing and relate them

[Stuart Presnell]

Michael Nahas said:

Any repository will have to address all 3 changes. But the changes may have very different solutions. A repository that only stored proof-terms in Lean's type theory would be resistant to changes in Lean's syntax, but not to Kevin Buzzard 's redefinition of a group. A repository storing only tactics would be invalidated if Lean's syntax changed. I have a feeling that the solution will be to store both tactics and the proof-terms and some mapping between them.

Part of the way mathlib deals with this problem is that proofs and definitions are never considered to be finalised static objects. Anything in mathlib — like the definition of group, or even the definition of the placeholder sorry tactic that we use all the time — can be modified if it makes sense to do so. This seems to be quite different from the approach you're suggesting, in which (as I understand it) proofs just keep accumulating but are never subsequently edited, and so old proofs can easily go stale.

[Kyle Miller]

Michael Nahas said:

Every version of the proof would be inserted into the repository. What you care about is the name in the library --- that is, when someone looks for your proof, how do they find it? When you were ready, you would change the "mathlib:fermats_last_theorem" tag to point to the version you wanted others to use.

I'm wondering, at a high level, what's the difference between this and git? A branch on git is a tag that points to a commit, which points to a file tree, which points to all the files in a content-addressed way. In the end, the process of updating a branch amounts to creating a new commit that points to a new list of files. If mathlib took the approach of one lemma or definition per file, then individual contributions could really just be modeled as changing what the file tree points to. If manipulating git is really the hard part to contributing formal mathematics (though I think learning Lean dwarfs the challenges of git), then giving people an editor that automatically force-pushes their work to a branch on github seems like it would do essentially what you're wanting.

Beyond that, one of the things that makes mathlib great is the PR process, where changes are evaluated with a fine-toothed comb, and everyone's differing ideas and viewpoints are forced to find a way to coexist. I like to think about it as we're all throwing in rocks that we think contain something worthwhile, and after they tumble around, bumping into each other, we're left with polished gems.

There is a problem related to your idea, though, that would probably be worth investigating. We tend to have a number of branches we've worked on that contain experiments or partially worked-out changes or additions, and these can be forgotten about. I don't think it's a very big deal that work is sometimes lost or accidentally re-done for a few reasons, one being that independent reformalization can give evidence something was designed well or provide new ideas to consider, but, still, sometimes it's better to dig into the archives, blow off the dust, and use that as a starting point for new work.

[Michael Nahas]

@Julian Berman "I don't know that I understand why mathematicians would need a drastically different class of tool"

I looked into other community projects --- Linux kernel, Wikipedia, etc. --- and saw that the easier it was to contribute, the more contributors the project had. And when I looked at the process to contribute to mathlib, I saw that Git/GitHub was the most obvious step to make easier. Or, at least, one I could get a grant to make easier.

I think formal math does have different properties than programming language source code. PL source code cares more about the chain of functions being called and the exact code in each function is important. In contrast, formal math is focused more around the inductive type definitions and, in many instances, proofs are interchangeable. I don't think formal math requires new repository software --- mathlib has gotten along well with Git and will continue to do so --- but if a new style of repository makes it easier for new contributions to mathlib, it will be good for the formal math community.

[Kyle Miller]

Michael Nahas said:

in many instances, proofs are interchangeable

It might would be interesting evaluating this for a large formalization project (like mathlib). I suspect most changes are not limited to changing proofs of theorems, and instead they're intrinsically interface-breaking. But that's just a guess from having reviewed PRs. Granted, many PRs do just introduce new material that builds on previous material, or move things around, or simplify proofs.

[Stuart Presnell]

But if we're thinking about the size of the obstruction for a newcomer to contribute, learning the intricacies of Lean (and the conventions of the mathlib project) is about 95% and figuring out how to use GitHub is 5% or less. Put another way: in a race between a Lean expert who has never used GitHub and a GitHub expert who has never used Lean, I'll bet on the former every time!

[Michael Nahas]

Kyle Miller said:

I'm wondering, at a high level, what's the difference between this and git? A branch on git is a tag that points to a commit, which points to a file tree, which points to all the files in a content-addressed way. In the end, the process of updating a branch amounts to creating a new commit that points to a new list of files. If mathlib took the approach of one lemma or definition per file, then individual contributions could really just be modeled as changing what the file tree points to.

That would work at the granularity of lemmas. A repository could do it for every subgoal inside a proof too.

But, yes, it could be built very close to what you say. But Git was designed for a certain set of interactions. E.g., git is designed to work detect and handle merge conflicts. A different style of repository would facilitate different interactions. E.g., ones where merges never conflict. The research goal would be to find a set of interactions that were easy for users to work with (auto-add and a good search feature) and could be implemented efficiently.

Kyle Miller said:

If manipulating git is really the hard part to contributing formal mathematics (though I think learning Lean dwarfs the challenges of git), then giving people an editor that automatically force-pushes their work to a branch on github seems like it would do essentially what you're wanting.

I agree that learning Lean is harder than learning Git. We should make both as easy as we can, shouldn't we? (FWIW, I wrote a tutorial for Coq to make that easier to learn. I need to make a version for Lean.)

[Stuart Presnell]

But your proposal isn’t to make what we’re using easier to work with, it’s to start a completely independent project that could, inter alia, swallow mathlib

[Michael Nahas]

Stuart Presnell said:

But if we're thinking about the size of the obstruction for a newcomer to contribute, learning the intricacies of Lean (and the conventions of the mathlib project) is about 95% and figuring out how to use GitHub is 5% or less. Put another way: in a race between a Lean expert who has never used GitHub and a GitHub expert who has never used Lean, I'll bet on the former every time!

If someone wants to pay me to make it easier to learn Lean, I'll be glad to spend my time doing that.

But the consequences of Git are not just for new people. How much time is spent by experienced people trying to teach new users how to use Git? And how much math is never shared because the Git is complicated and mathlib has a very high bar for any contribution?

In one video, @Kevin Buzzard talked about a student who had written proofs on Hilbert's Geometry: "It was amazing. That's one of the many things we learned, all unpublished, all on some private GitHub repository completely unavailable.'' https://youtu.be/Dp-mQ3HxgDE?t=4095 That student knew Git. And, still, those proofs will have to be rewritten by someone else, because they are locked on some hard-drive somewhere.

My goal with this repository design is to make it very very easy to share and store proofs. So nothing will be lost and people will not have to waste their time reproving what someone else has already proven.

[Yaël Dillies]

I think the main problem with your approach is that you're conflating "storage" and "knowledge".

[Yaël Dillies]

Nobody cares about a mass of theorems. What they care about is a tidied mass of theorems.

[Yaël Dillies]

Essentially, Github already "stores everything so that nothing can be lost". So what's the problem? The problem is that most of this code is barely known about and, more crucially, will not interact well with the rest of the library. That's why mathlib has standards.

[Yaël Dillies]

That makes a good motto: Code that compiles is not code that works.

[Stuart Presnell]

Michael Nahas said:

How much time is spent by experienced people trying to teach new users how to use Git? And how much math is never shared because the Git is complicated and mathlib has a very high bar for any contribution?

These are good questions. They seem like questions you should try to get some approximate answers to before embarking on an enormous project to replace Git. We have a large community here, many of whom have had to teach students how to use Git to a level of proficiency where they can use it for their own projects or contribute to mathlib. They may be able to tell you how much of an obstacle Git was.

[Kyle Miller]

@Michael Nahas Have you heard about the mathzoo? It's very new, and I think one of the reasons for its existence is to collect things that people think are good enough to share, but which, for whatever reason, the author doesn't want to have it clear the bar for mathlib quality.

[Michael Nahas]

Yaël Dillies said:

Nobody cares about a mass of theorems. What they care about is a tidied mass of theorems.

That's a cogent point.

I believe that people do care about a large mass of messy theorems. Obviously, they would prefer a tidy mass of theorems of the same size, but I don't think that messy theorems have zero or negative value.

I definitely believe that mathlib and its heavily curated set of definitions and proofs is valuable. I'm not trying to get rid of that. But I believe we can store and share other theorems too.

[Michael Nahas]

Stuart Presnell said:

These are good questions. They seem like questions you should try to get some approximate answers to before embarking on an enormous project to replace Git. We have a large community here, many of whom have had to teach students how to use Git to a level of proficiency where they can use it for their own projects or contribute to mathlib. They may be able to tell you how much of an obstacle Git was.

I'd love to hear that. I am also working on a draft of a letter to the Hoskinson Center, where I recommend they do a survey of new and experienced mathlib contributors, to see what might make the most impact. Unfortunately, that letter is on hold with the March 3rd NSF grant deadline.

[Michael Nahas]

Kyle Miller said:

Michael Nahas Have you heard about the mathzoo? It's very new, and I think one of the reasons for its existence is to collect things that people think are good enough to share, but which, for whatever reason, the author doesn't want to have it clear the bar for mathlib quality.

Thanks. Yes, Mario Carneiro mentioned mathzoo to me.

[Stuart Presnell]

Michael Nahas said:

how much math is never shared because the Git is complicated and mathlib has a very high bar for any contribution?

The fact that mathlib has a high bar for contributions is nothing to do with "Git is complicated". It's, as Yaël said, because we think an integrated and curated library of definitions and theorems is more valuable than a jumbled random assortment.

[Kyle Miller]

I'm sort of reminded of the infamous comments under this Hacker News post about Dropbox, back when it was just an application to Y Combinator.

I have my doubts that making git easier will mean there will be more formalized math that people will want to use (I speculate there's a correlation between having spent the time to get proficient enough in git and producing well-engineered theorem statements that are usable by others), but, who knows, maybe a "dropbox for lean" will be much more useful than all of us technically adept specialists are able to see, just like in some of those HN comments.

[Eric Rodriguez]

not to speak for people, but I know for example Bhavik has a lot of formalized stuff that hasn't really ended up anywhere except some random branch somewhere or whatever. it'd be nice just to check it in. i'm personally more diligent about trying to PR most of what I do to mathlib, but I'd argue stuff like #12197 maybe has a better home in somewhere like this than in mathlib as a whole (who cares that all infinite cardinals are prime and not irreducible!?)

[Eric Rodriguez]

so a drop-and-go method for dropping formalized files? that could have potential... but it really could bitrot at a very unsustainable way

[Yaël Dillies]

For the record, I'm spending a good deal of my time moving Bhavik's stuff towards mathlib. #11248 for example is taken from #2770.

[Stuart Presnell]

Is that something we could easily accommodate in mathlib? Perhaps as another subfolder of archive (“for formalizations which don't have a good place in mathlib”)?

[Eric Rodriguez]

i think that's the goal of mathzoo

[Stuart Presnell]

But if that were (somehow) more integrated into mathlib then we could, for example, have a version of library_search that could reveal that someone has proved the theorem you need but not yet made it ready for mathlib

[Yaël Dillies]

That's what draft PR are for

[Stuart Presnell]

True, but evidently people (and students in particular) are doing work that they don't plan to PR and leaving it in private repos (as suggested by the quote from Kevin that Michael cites above: "It was amazing. That's one of the many things we learned, all unpublished, all on some private GitHub repository completely unavailable.'')

[Arthur Paulino]

@Yaël Dillies I think they are talking about code that actually goes to master or becomes accessible from other branches somehow

[Kyle Miller]

@Stuart Presnell That entails additional maintenance overhead -- everything that's inside the mathlib repo needs to compile with bleeding-edge mathlib. The tradeoff is that then making sweeping changes to mathlib design becomes just that much more labor-intensive.

[Stuart Presnell]

Yeah, I was trying to think about what would need to be done to make this at all feasible.

[Stuart Presnell]

Basically the aim is to have the ability to see unpolished code in a way that allows a new variant of library_search to access it, but still allow that code to be out of date, incomplete, and imperfect in other ways in order to make the barrier to entry sufficiently low.

[Arthur Paulino]

I think the developers of the gptf tactic are making http requests or something like that. Maybe you're talking about something of the kind?

[Stuart Presnell]

Ah, that's not what I was thinking of, but that's another interesting way around the problem

[Jireh Loreaux]

Michael Nahas said:

Obviously, they would prefer a tidy mass of theorems of the same size, but I don't think that messy theorems have zero or negative value.

I'm not sure, but I don't think I agree with this. From various discussions with software engineers in industry, I think there is a strong argument to be made that unmaintained or poorly written code does have negative value. Of course, this is likely obvious if you have to use the code, but you might make the argument: "if it's garbage code, then no one has to use those results." My counterpoint is that you still have to filter out that garbage code to see the diamond in the rough.

@Michael Nahas, to be clear: I'm pushing back hard not because I think there are no improvements to be made, only because I don't yet see your proposed project as a viable improvement. Perhaps with more clarity about the potential for solving many of the issues described above I might be convinced (not that persuading me matters to anyone :laughing:).

[Stuart Presnell]

Yes, I don't think anyone here is saying "Don't do this". The pushback you're getting is:
(a) from the experience of this community your project may be considerably more difficult to do well;
(b) you seem to be overstating the barrier that GitHub presents, while failing to match the advantages that it has (e.g. a large user-base to provide support)

(and also this business about "funnel[ing] money from people querying for theorems to the people adding them to the repository" sits badly with me, but that's presumably not an integral part of your proposal)

[Matthew Ballard]

For example in the opposite direction, we replaced Maple with Python (Sage) for the lab components in our calculus sequence here. Why? Maple is great for math. It’s easier to use than Python because math is its purpose. The problem is that Maple skills did not translate as directly to other domains as Python. Appreciation for Python is much more widely spread. If we are teaching skills, it just makes more sense.

Git is between meh and annoying but is what everyone uses for better or worse. If I want my students to take away the most useful skill set, I want them to to learn git. Moving away from git will make teaching with Lean less useful pedagogically rather than more.

[Arthur Paulino]

More examples of b from Stuart's comment:

• mathlib's doc page, hosted as a GitHub Page, is updated automatically on every merge that's performed on the master branch (via a GitHub action I think)
• We're able to use bors
• The interface for PR reviews is not perfect, but it already does wonders as it is

[Matthew Ballard]

I should say while git is what it is I :heart: GitHub. I have my PhD students PRing their comprehensive exam papers. I don’t know of any other interface with threaded line specific commenting.

[Yakov Pechersky]

I would love to have a better version control system for proofs. One that isn't word/line based, but is Lean aware. Such that renaming variables is one type of change, generalizing or weakening lemmas, tracing dependency graphs, seeing cross library correlations in development.

[Yakov Pechersky]

For sure git is intimidating when you see huge diffs over something like "I made a helper notation for this object" or "I removed repetitive code, thus generalizing many lemmas". In a certain sense, number of lines changed vs "weight of mathematical content" might actually be inversely correlated! Here I mean changed specifically, not lines added.

[Eric Wieser]

Strictly git isn't word/line-based, it's just the default diff/merge tools that are. Semantic diff tools exist in some settings, but they're not widely adopted and certainly almost no existing tools will support lean out of the box.

[Michael Nahas]

@Jireh Loreaux "My counterpoint is that you still have to filter out that garbage code to see the diamond in the rough." But computers are great at filtering!

So imagine this: You're trying to prove something and getting stuck. But you have a friend who just proved something similar, so you message him what you're trying to prove. And you just fill in "sorry" or "by library search" or something else in your Lean file. And you continue on, and work on the next theorem you're trying to prove. And, whenever your friend every proves it (or if they prove it), your Lean file gets updated automagically with the proof.

Or, imagine the same scenario, but you post the difficult theorem to a large group on Zulip. And anyone, anywhere, at anytime --- even the past --- has solved it, and your file automatically updates with the proof.

Or, imagine you're working on a large proof project, like FlySpeck or the Liquid Tensor Experiment. There is a complicated core proof that needs expert attention, but also a few hundred lemmas at the fringe that just need to be proven. There's a bunch of fans of math who would love to help on a large project, if only to say they did it or have their named listed in the "Thanks to:" section of the paper. And for a large project, it isn't hard to generate the current list of theorems that still need to be proven and post it on a webpage. But would you want to handle a hundred PR requests from a hundred fans each, possibly, proving a tiny theorem? Or do you want a system that find "any proof written anywhere by anybody at any time" and automatically updates your code with the proof?

Are those viable improvements over Git+GitHub?

[Yakov Pechersky]

How does your "auto lookup of relevant proof" compare/contrast with Copilot or the other crowdsourced code completion tools? I imagine yours is better at relevant code. Because you have on-the-fly compilation and proving?

[Patrick Stevens]

Michael Nahas said:

But would you want to handle a hundred PR requests from a hundred fans each, possibly, proving a tiny theorem? Or do you want a system that find "any proof written anywhere by anybody at any time" and automatically updates your code with the proof?

Honestly, the answer from me is that I want the PRs. My entire contribution to Mathlib has been around one single not-very-difficult theorem, which I chip away at whenever I have some spare energy, and so many times the PR process has correctly prevented me from just dumping garbage into mathlib. Garbage that compiles and proves what it says it proves, but garbage nonetheless. In a world which automatically syncs everyone's proofs, you'd have immediate access to about 3000 lines of my case-bashing and overly specific lemmas, that takes 30secs to type-check. Is that better than having access to a 200-commit years-old PR which is slowly shrinking, becoming more sane, and having its lemmas appropriately generalised and absorbed deeper into the heart of mathlib? I honestly think I prefer the world with the PR.

[Arthur Paulino]

Michael Nahas said:

"any proof written anywhere by anybody at any time"

If the proof is too old, it might be incompatible with my current Lean/mathlib environment. Breaking changes are too common and would potentially kill many of the stored proofs.

As I mentioned a few comments ago, I think your idea can be put to experiment with a tactic that searches an online database and suggests something in the form of "Try this: ..." or "Result shown at ...". You might want to feed your database with several GitHub repos and the technical issues of resolving multiple Lean/mathlib versions will show up right away.

You'd be able to build PoC's for different aspects of your pipeline: processing/compiling Lean code, serving/consuming data, searching/filtering/matching. And you wouldn't need to rely on having an entire community changing their modus operandi for your tests.

[Patrick Stevens]

I could easily believe that mathlib is a special case, though. It hopes to be a library on which all mathematics can be built, which means it has very strong internal-consistency and design requirements. Perhaps other, less grandiose, projects can get away with less in the way of design, and more in the way of "a hundred randomers yeet their proofs into prod". That's a choice for the maintainers of those projects to make. (It's a general question that any open-source maintainer must answer: do I accept random PRs, and if so, what requirements do I insist on before I accept a random PR?)

[Michael Nahas]

I typed up a summary of the conversation for myself. I thought I should post it here, in case someone wanted a recap. Many of these are comments by a single person and don't represent any group concensus.

Priorities:

• Lean is much harder to learn than Git. So, this is small potatoes.
• There are more painful things in the contribution process that can be fixed without replacing Git.

Git comments:

• Git+GitHub have lots of documentation, so users can get help many places.
• Git is useful for mathematicians to know, because they can use it elsewhere (e.g., LaTeX documents)
• Git is useful for students to know, because they can use it elsewhere.
• Git works with other tools, like GitHub's PR interface and bors.
• Git is disliked (mostly because of a bad user interface)
• Git is not "Lean aware". E.g., changing a variable name results in large diff.

Mathlib comments:

• Interoperability of its many parts is important.
• Having a single definition of a concept in mathlib is important.
• That the community decides (and not a dictator) on that single definition is important
• Versioning is a big problem in trying to hold mathlib together. (It hurt Coq's library.)
• mathlib authors care about a "presentable" version of code. (Even desiring not to release some versions that compile.)
• Definitions and tactics are not static: "group" or "sorry" can change.
• Search in mathlib right now is difficult, as demonstrated by the "Is there code for X?" Zulip thread.
• Contributors do worry about work forgotten in the archives, which could be the basis for new work. Some cared about work lost because of difficulties getting things into mathlib.

Thoughts on my project:

• A disorganized system is not useful. This is "storage" not "knowledge".
• Search would be difficult. (so much crap returned in search)
• A repository that supports lots of definitions could cause "enclaves". (This caused problems for Coq's library, but LATIN's seemed okay.)
• Will supporting lots of definitions mean that things don't work well together?
• Dependency tracking is a problem.
• Naming is a problem.
• How does it handle multiple definitions with same name? (E.g., "nat" or "group")
• If you have multiple proofs, how do you select "good" proofs? E.g., not "3000 lines of my case-bashing and overly specific lemmas, that takes 30secs to type-check."
• In this design, proofs and definitions are static. That is different from mathlib, where "group" or "sorry" can change. How does this affect the library? Can "old proofs go stale" or suffer "bitrot"?
• There are many version control programs. Git "won". Why does math need a different tool?
• You can use Git to imitate content-addressed storage. How is this different?
• We could write a tool to automatically add proofs to Git (assigning unique names, etc.). That solves the "new users don't know Git" problem. Why do we need to do more than that?
• There are two separate arguments: "Git is complicated, therefore new people don't add stuff" and "mathlib has standards, therefore stuff is not added".
• What is the set of actions supported by the library? How do you expect users (new and experienced) to use those actions in practice?
• How do you update an older version of a proof? How does someone inform people of it?
• If the library has "A and B", will a search of "B and A" find something?
• How does it work with the code review ("Pull Request") process?
• How does it handle changes to a definition?
• How does it handle changes to Lean's syntax?
• How does it handle changes to Lean's type theory (or kernel)?
• How does this compare to code completion tools, like Copilot?
• Is this like a package manager, with mathlib being a special package?
• Can you prove properties about it, like Pujil?
• Can it handle other proof languages, like Metamath?
• Will your tool be "Lean aware"?
• How is this different from mathzoo ?
• Will this "swallow" mathlib?
• mathlib's requirements might be different from a project like FlySpeck or the Liquid Tensor Experiment.

TODO:

• look at Unison programming language
• look at Pujil source control
• look at the Refined GitHub extension
• Talk to organizers of large non-library proof projects, like the Liquid Tensor Experiment.
• Ask teachers about their difficulties with teaching Git to students

I want to thank everyone for their comments. And I want to thank everyone who said the encouraging words. It definitely felt like my idea was the rock in @Kyle Miller 's tumbler --- it got a lot of bumping. I doubt it's a gem yet, but your comments will definitely sharpen my grant proposal. I found a lot of hole in my argument that I need to fill. And I have a better understanding of your priorities, your vision for mathlib and the role that a repository plays it in all.

[Eric Wieser]

(typo: Pijul not Pujil)

[Sebastian Reichelt]

A bit late, but: It was mentioned that the set of contributions living in not-yet-merged branches is actually quite close to what you are proposing. Surely any improvement on being able to find and integrate such contributions would be quite welcome?

[Heather Macbeth]

Typically, this is not a technology problem but a human resources problem. Such a branch often has an associated PR with 10 unaddressed review comments from 14 months ago, and neither the author nor anyone else currently has the energy to make the requested changes.

[Eric Wieser]

If a tool were available that was like library_search but worked on dead branches somehow, that might also double up as a contributor_search that steers the searching user to revive the dead PR.

[Heather Macbeth]

Still, the scale we're talking about is not large. The collective memory of the people online on Zulip in a 4-hour period is almost always large enough to answer the question "Is there, or was there ever an attempt at, code for X"?

[Heather Macbeth]

I'm not sure this needs a technological solution when we have an efficient (and typically more powerful, since it allows for mathematical "fuzzy matching") human one.

[Wrenna Robson]

(I also have a definition of bind in my framework, though I haven't quite finished the proof of normality - it's easy on pen and paper but it's slightly fiddly somehow.)

[Eric Wieser]

(wrong thread @Wrenna Robson ? You can edit the title of your message to move it)

[Michael Nahas]

Heather Macbeth said:

I'm not sure this needs a technological solution when we have an efficient (and typically more powerful, since it allows for mathematical "fuzzy matching") human one.

Google is a horrible replacement for a good reference librarian, but it sure gets used. ;)

[Mac]

One major technological idea that seems nested in this discussion that seems important for any kind of proof library for Lean is content addressed definitions (and syntax, extensions, etc.). That is the key idea behind Unison, and it would be of great benefit to Lean. Such a feature would be quite valuable in other use cases (e.g., building, dependency resolution, etc.) and solves many of the "How to handle changes to X?" questions. Thus, I think it would be an ideal target for anyone wanting to doing some research in this area and potentially make a useful contribution to the Lean ecosystem.