We propose to create a new model for interactive, machine-based theorem proving that integrates collaboration as a core concept. For this, we shall take the lessons and technologies of interactive theorem proving (ITP) and integrate those stemming from the social web, in particular: 1) commons-based peer production and crowd-sourcing, 2) reputation systems and 3) recommender systems. Sites like Wikipedia, Stack Overflow and Math Overflow have proven that these three components of the social web can result in remarkable collaborative productivity. The focus of our research will be on how to harness this productivity so as to establish collaborative theorem proving as the social machine of ITP and thus tackle verification tasks on an unprecedented scale. This article was published on 2024-11-22
