Theorem Search

Stream: Machine Learning for Theorem Proving

[Vasily Ilin]

We release a theorem search engine over all arXiv, Stacks Project, and a few other sources (9.3 million research-level theorems). We expect it to be useful for theorem proving AI agents. We have a website, an API, and an MCP server.
Project page: https://theoremsearch.com/

P.S. Is this the right channel to put this announcement in?

[Ralf Stephan]

Do you plan to include sources where you need to do OCR?

[Vasily Ilin]

@Ralf Stephan , not in the next couple months. Later yes.

[Bas Spitters]

@Vasily Ilin Since this is the lean zulip. Have you tried making connections with existing Lean formalizaion, or perhaps only the definitions?
I know there are various autoformalization projects out there that could also be interested in this.

[Vasily Ilin]

@Bas Spitters , yes! We are linking the theorems in natural language to the corresponding theorems in Lean, using the existing blueprints. When we release the next version of the dataset, we will include these links.