Alex, Eric, and Jack,

Jack Park cited an article that discusses Doug Lenat's career and ends with a link to a Ted Talk that he presented ten years ago.  That article and Lenat's talk clarify the issues that Alex and Eric mentioned.   I suggest that people listen to it before continuing with my comments below:  https://www.sciencetimes.com/articles/45824/20230906/douglas-lenat-dead-ai-researcher-spent-40-years-building-computer.htm

The last paragraph in that article, just before the link to the Ted Talk, is "According to cognitive scientist Gary Marcus, he undertook an endeavor no one else dared to do. Although he failed, he had at least shown a portion of the route for those exploring the same path."

Instead of saying that Lenat failed, it's better to say that he succeeded in one important goal: Developing a huge ontology and reasoning system that covers a large part of human knowledge.  That is, in fact, the explicit goal of the ISO standard for a top-level ontology that is sufficient to support a very large number of practical applications.

Lenat failed for the same reason why I have been making negative comments about that ISO Standard:  it's impossible to have a consistent formal ontology of everything that people do or say or think.  If we all agree that Lenat failed, then it's time to declare that ISO standard is a  dead end.  

If anybody thinks that the ISO standard is still worthwhile, then they have to face an uphill battle:  Explain what Lenat might have done in the past 40 years that could have enabled the Cyc project to succeed.  Since I doubt that anybody can do that, I believe that we should switch our attention to two more achievable goals:  (1) Emphasize the DOL standard for supporting interoperability among multiple independently developed ontologies.  (2) Adopt ideas from the recent work on generative AI to develop natural language interfaces that can use and relate the ontologies supported by point #1.

Alex>  We have come close to my favorite topic: framework for theory (theoretical knowledge), which I propose to consider using the example of genomics. 

Good luck.   But I doubt that any framework based on any methodology can do what Lenat failed to do in 40 years with a large number of very good programmers, logicians, linguists, ontologists, and specialists in various subfields.  After the first 20 years, they had devoted one person-millennium of effort to the project (an average of 50 people for 20 years).

Eric> Mathematicians, unlike "Industrials" (for computers ... and so on) cannot admit "obsolescence" ! 

Yes.  A mathematical theorem, once it is proved, is true forever.  Further progress can build on, simplify, unify, or generalize the statement of the proof.  Some results may be forgotten or ignored, but nothing that has been proved can become false.

Goal:  Future developments must use the accuracy and reliability of mathematics and mathematical logic to evaluate and build on the often flaky results of the GPT-like systems.

John