Very exciting. I wished there would also be room for a group at YCR/HARC working on collaborative theorem proving (CTP) as proposed here: http://arxiv.org/abs/1

Very exciting. I wished there would also be room for a group at YCR/HARC working on collaborative theorem proving (CTP) as proposed here: http://arxiv.org/abs/1404.6186 http://arxiv.org/abs/1404.6186 :-)