Software tool for formal proof collaboration

Stream: Carleson

[Iva Babukova]

Hi everybody,

I'm very interested in helping mathematicians organise formalisation projects by building productivity software tools that would allow them to more effectively collaborate on large-scale formal proofs.

My background is in scientific software development (mostly biology/ bioinformatics/ data science). I've worked at Harvard Medical School on open source software in the field of single cell transcriptomics, specifically on projects called Vitessce and Cellenics. I have a lot of experience designing and building software for researchers.

I follow the "lean startup" software product development methodology. I'm planning to put together a very minimally useful software product very quickly (in a matter of weeks). Before I even write any code I'd like to iterate on a couple of versions of mock-up designs (please see below for v1 wireframes):

Lean queue

I'd like to build a tool that fits well and improves on the existing formalisation collaboration workflow, which I understand is built on github, Blueprint/ dependency graph software and of course Zulip chat.

In the first iteration, I'd like to allow users to perform two actions:

• Submit "jobs" -- which I'd like to propose are initially only self-contained lemmas (with Mathlib as the only dependency), together with short informal description of what needs to be formalised.
• Allow users to claim these "jobs" and eventually resolve them as "done".

If this works well enough I will then get your feedback on various ideas for improvement and I'll start working on a feature roadmap.

More immediately, I'd really appreciate it if you could help me understand your workflows. I would really benefit from your personal perspectives on the following topics:

What are the current issues that you're facing when working on formalisation projects? How do these issues differ between "lean formaliser" and "task splitter" personas?

What are the limitations of existing tools that you work with on your formalisation projects (Github, Blueprint, Zulip, Loogle/Moogle, others?)

What do you think of the proposed wireframes? Am I prioritising the most essential feature set for the minimum viable product (MVP) of such a collaboration tool? Please remember that in the "lean startup" methodology the idea is to build a very scrappy MVP and then start adding features once the product gains initial userbase, based on the feedback from initial users.

Am I focusing on the right problem? Are there more pressing issues that a collaboration software should be addressing?

[Johan Commelin]

Welcome! There has been quite some discussion about workflows in the past 2 weeks on the #Equational channel.

I think there are at least two related, but maybe different, workflows:

• working on and maintaining projects like Carleson, Equational, FLT
• working on and maintaining mathlib. See https://jcommelin.github.io/queueboard/ for a recent attempt at a prototype to improve the mathlib review workflow. (Mathlib has > 1000 open prs of which > 200 ready for review.)

[Johan Commelin]

@Iva Babukova I didn't know that you double-posted. If you do that, please explicitly flag the other post.

[Iva Babukova]

Hi Johan! Your prototype looks very similar to what I was thinking that the community might find helpful -- it even has a similar name :) Looks really cool! Do you have an idea of its usage at the moment and what people's feedback has been so far?

Johan Commelin said:

Iva Babukova I didn't know that you double-posted. If you do that, please explicitly flag the other post.

I will make sure I flag the other post next time -- I am new here and didn't realise that lots of people are part of both channels.