Hacker News Reader

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

View on HN

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&#...

There was a mention of dependent types.

Reply on news.ycombinator.com