I believe this comment is meant to be a response to another post (https://news.ycombinator.com/item?id=18155410 https://news.ycombinator.com/item?id=18155410) w

I believe this comment is meant to be a response to another post (https://news.ycombinator.com/item?id=18155410 https://news.ycombinator.com/item?id=18155410) who pointed out a flaw (now fixed) in Coq that allowed false theorems to be proved. Github link: https://github.com/clarus/falso https://github.com/clarus/falso