LeanExplore update

Stream: general

[Justin Asher]

I am updating LeanExplore. The server may be down or things may not be working properly for the next few hours (or days).

[Justin Asher]

Any feedback is appreciated! As always.

[Kim Morrison]

Could the results also link to the Mathlib docs, as well as the Mathlib sources?

e.g. with a query like https://leanexplore.com/?pkg=Batteries&pkg=Init&pkg=Lean&pkg=Mathlib&pkg=Std&q=How+to+I+talk+about+the+Riemann+integral+in+Mathlib%3F, I need some sequence of clicks that will show me the definition/doc-string of IntegrationParams before I've learnt anything.

[Justin Asher]

Thanks for the feedback! Actually, this should already be available:

• The name (e.g., BoxIntegral.integral) links to the Mathlib docs (example)
• The file path (e.g., In: Mathlib.Analysis.BoxIntegral.Basic) links to the source file (example)
• You can also "View dependencies" to explore things like IntegrationParams without leaving LeanExplore

That said, if this isn't discoverable enough or you had something different in mind, I'm happy to revisit the UI to make it clearer.

[Kim Morrison]

Oops, that's great. I guess I was distracted by the "in:" link, and since I (idiosyncratically) always jump to the source in preference to the docs, I must have thought that the documentation link would come after the source link, and it didn't occur to me to try clicking the title! But I don't think this is a failure mode that will affect other people. :-)

[Justin Asher]

Happy to hear that.

[Yicheng Tao]

I got into trouble when trying to search with local service. See this issue. @Justin Asher

[Justin Asher]

@Yicheng Tao I fixed it. Upgrade the package and try again.

[Yicheng Tao]

@Justin Asher Thanks for the quick response. There is still a small problem, but it can work now. See the issue for details.

[Justin Asher]

@Yicheng Tao Great. Will fix that later too to be clearer.

[Malvin Gattinger]

In the Gemini description of Relation.ReflTransGen there is a mistake in the order of a and b in the part " if either , or if there exists some element such that is related to by the reflexive transitive closure" - also, copying from there should also give me the math mode letters :wink:

[Justin Asher]

@Malvin Gattinger Good catch! I am surprised Gemini missed that.

I might add a system that allows people to report incorrect informalizations.

[Justin Asher]

@Yicheng Tao I fixed the API issue. Please let me know if anything else comes up.

[Justin Asher]

I put the LeanExplore dataset on Hugging Face:

https://huggingface.co/datasets/justinasher/lean-explore