QED manifesto revisited

Stream: general

[Kevin Buzzard]

I was looking through Freek Wiedijk's "The QED manifesto revisited". A quote from it:

Finally, a multi-contributor library of formal mathematics should be created
that is well-organized. As I claimed in Section 2, the sociological puzzle has
not been solved yet of how to set up a library in such a way that it both
admits many contributors, but also stays well-organized. Current attempts
that have not yet been very successful in this respect are:

• multi-contributor, but not really well-organized:
  ∗ MML
  ∗ Coq contribs
  ∗ AFP

• well-organized, but not really multi-contributor:
  ∗ HOL Light library
  ∗ C- CoRN [4]
  A good first goal for this library will be to formalize ‘all of undergraduate
  mathematics’. This will take more than a hundred man-years [20], which
  means that it will need the involvement of a non-trivial number of con-
  tributors. Also, with something like that it will be clear whether it is well-
  organized or not.

The success of Wikipedia suggests that it might be possible to solve the
puzzle of having both many contributors and still also have a well-organized
whole. However, aiming for a ‘Wikipedia for formalized mathematics’ is for
me too much like hoping that someone else will do the work. I will believe
that such an approach can be successful when I see it happening.

I guess the next time I see him I should ask him whether he can see it happening. He asked me in Pittsburgh how much of our 1st and 2nd year material had not yet been formalised in Lean, and Chris Hughes gave him a very complete answer. The big hole is complex analysis.

[Kevin Buzzard]

@Freek Wiedijk do you see these notifications?