> That's just what I came up with after thinking on it for 2 minutes. I'm sure they have even better ideas. the thing is that ideas not necessary easy to imple

> That's just what I came up with after thinking on it for 2 minutes. I'm sure they have even better ideas. the thing is that ideas not necessary easy to implement. There will be many obstacles on route you described: - quality of provers, is there good ergo provers which also can run at large scales (say billions of facts) - you need some formalization approach, probably LLM will do some work, but we don't know what will be quality - LLM likely will generate many individual factoids, which are losely compatible, contradicting, etc, and untrivial effort is required to reconcile and connect them