Using ITPs for large scale collaborations

Stream: general

[Jason Rute]

On thing Terry Tao has talked about is that ITPs can act as a platform for large scale collaborations where many mathematicians can collaborate on the same project without having to understand or trust the work of their collaborators. (This could also be good for work connecting two or more disjoint fields.) To what extent has this idea been put to the test already (for large scale research/collaboration of new mathematics and not just formalization of existing work)?

[Daniel Weber]

I think the only large scale project so far is the Equational Theories project (see #Equational )