7 ms·
Andrej Bauer and others are working on a kind of similar infrastructure, and developing a dedicated query language: https://math.andrej.com/2026/07/11/making-ai
by butokai 1mo ago
Andrej Bauer and others are working on a kind of similar infrastructure, and developing a dedicated query language: https://math.andrej.com/2026/07/11/making-ai-smarter-with-ai/ https://math.andrej.com/2026/07/11/making-ai-smarter-with-ai...
- vatsachak 1mo agoIs 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.