Discussion Thread for LeanDex

Stream: general

[Bolton Bailey]

Here is a discussion thread for the announcement of LeanDex
#announce > LeanDex

[Kevin Buzzard]

Hah I can now search FLT! Interesting -- thanks! Great to see it's on mathlib v4.24 -- will be interesting to see how long it keeps up (this seems to be the achilles heal with all previous semantic search engines).

[Kelly Davis]

Bolton Bailey said:

Here is a discussion thread for the announcement of LeanDex
#announce > LeanDex

Thanks!

Perfect timing! I had forked Justin's repo a few days ago and was working on modifications, but here they are!

A few questions come to mind...

1. Will one in future be able to select the lean-toolchain version one searches against? (Including older versions?)
2. Will the repo lean-explore reflect the deployed version?
3. Will there be a, say, Python client?
4. Will the repo lean-explore retain the MCP server?

I'm sure I'll have other questions too.

PS: I know selecting the lean toolchain version is a bit annoying to implement, e.g. the code in the extractor has to be modified for each lean toolchain version and also there's the time (and cost) spent running everything in extractor and scripts dir to create the vector DB's. But lots of AI provers are working off of slightly older versions. So having older versions around would help a lot! (I was running code in the extractor and scripts dir for v4.15 over the last days.)

[Bolton Bailey]

Will one in future be able to select the lean-toolchain version one searches against? (Including older versions?)

This is a good feature suggestion!

Will the repo lean-explore reflect the deployed version?

Yes, I think so

Will there be a, say, Python client? / Will the repo lean-explore retain the MCP server?

We have been thinking of developing our own MCP server with access to this and other tools (stay tuned). I don't know if we have plans for an independent separate Python client, but if that's something people would find useful we could consider it.

[Kelly Davis]

Bolton Bailey said:

Will there be a, say, Python client? / Will the repo lean-explore retain the MCP server?

We have been thinking of developing our own MCP server with access to this and other tools (stay tuned). I don't know if we have plans for an independent separate Python client, but if that's something people would find useful we could consider it.

Python or MCP, either works.

Would "this and other tools" include the kimina-lean-server? If so, it'd be a welcome addition.

PS: I extended the kimina-lean-server so that there are two extra endpoints:

1. api/ast that returns the abstract syntax tree (AST) of a particular module, e.g. Lean.Elab.Frontend
2. api/ast_code that returns the AST of the code submitted to the endpoint.

Maybe you could folds these in too.