3 ms·

Yeah, pretty fluffy article, no mention of HOL, dependent types, other camps. I was hoping to see libs like Isabelle, metaMath, Corbineau's coq lib etc mention

by gtani 14y ago

Yeah, pretty fluffy article, no mention of HOL, dependent types, other camps. I was hoping to see libs like Isabelle, metaMath, Corbineau's coq lib etc mentioned

szany 14y ago
There was a mention of dependent types.
dubya 14y ago
Isabelle was used for the proof of the prime number theorem. The link from the article: http://repository.cmu.edu/cgi/viewcontent.cgi?article=1032&context=philosophy http://repository.cmu.edu/cgi/viewcontent.cgi?article=1032&#...