← Back to context

Comment by gtani

13 years 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

2 comments

gtani

Reply

dubya 13 years 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&#...

szany 13 years ago

There was a mention of dependent types.