> It seems like encoding ‘all of math so far’ in some theorem prover seems like an ideal open source project... Is there such an effort now? Yes. Metamath's s

> It seems like encoding ‘all of math so far’ in some theorem prover seems like an ideal open source project... Is there such an effort now? Yes. Metamath's set.mm is expressly such a project, and I recently created a Gource visualization of set.mm's progress over time. For the first few years it was basically one person, but that increased over time and there have now been 48 different contributors. See: https://www.youtube.com/watch?v=XC1g8FmFcUU https://www.youtube.com/watch?v=XC1g8FmFcUU