Comment by 0x3f

What exactly is 'merging' here? Existing formal knowledgebases with LLMs? I don't think that's anywhere near human knowledge and thus ability to make novel connections. And autoformalization is... basically not happening soon, so we're still ultimately bottlenecked there.