AlphaProof's Greatest Hits

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

So, you looking for Cyc [1], practically.

[1] https://en.wikipedia.org/wiki/Cyc

Does Cyc have proofs?

In a sense, yes, since it has a foundation in Prolog style facts and rules, and supposedly can output its reasoning.

Ok, sounds like in principle you could have proofs, but in practice, you don't?

Are there any checks for the consistency of all facts?

How could there be? Gödel gets in the way.

In most interactive theorem provers the check is simple: you single out the axioms you believe, and all other stuff you do is guaranteed to preserve consistency. That works in an ITP system because there are only a few axioms.

If Cyc has 100000 axioms/facts, then that's a problem.

It's not a theorem prover, it's more like a support system for decision making.

They can probably isolate 100k facts from some domain for you if you pay for it, but their idea is to run inference on millions of "common sense" and everyday facts and have been for decades.

That sounds to me like something that will be subsumed by the combination of ITP and AI.