[gavanwoolery]

I immediately recognized the headline even though its been 15 years since I last read up on Cyc.

I still think the potential of lambda calculus in knowledge representation and logical deduction is high and under-represented in research.

Just theorizing, but I think a large part of the problem is the difficulty in interfacing this knowledge base with manual, human entry. Another pitfall is the difficulty in determining strange or unanticipated logical outcomes, and developing a framework to catch or validate these.

[rademaker]

I have been working on that direction with Lean Theorem Prover (https://leanprover.github.io). There is also works using Coq (https://link.springer.com/chapter/10.1007/978-3-642-35786-2_...)