Is there any advantage of this over an agent using a Google search?

I feel like the main benefit of such an endeavor would be to create a centralized database of mathematical theorems. But why aren't we using Lean theorems as the nodes instead?

The holy grail would be constructing an encoder that takes in a lean theorem and produces a meaningful latent vector so that whatever future math AI can instantly look up previously used "tricks" as opposed to only theorems.

I've met Andrej and he's obviously a genius so I'm sure this is useful.