Get the latest tech news
“Why not just use Lean?”
[ AUTOMATH LCF HOL system HOL Light Lean ] formalised mathematics I have been told that when proposing to formalise mathematics these days, you have to explain why you are not using Lean. And that reminds me why I left the dependent-typed world 40 years ago: its cultism, insularity and conformity.
None
Or read this on Hacker News
