theorems search engine

Stream: PhysLean

[Rein Zustand]

I just found out about PhysLean very recently. Thank you for doing this for humanity! I had similar idea in the past, where I started by formalizing EPR paradox. I wanted to know if this has already been implemented in PhysLean, but there is no search engine for the theorems.

I want to contribute by either formalizing an EPR paradox or implementing a search engine for the theorems.

[Rein Zustand]

Oh, nvm, there is already https://www.leanexplore.com/?pkg=PhysLean . I think the link and the link name would have been clearer if it directly links to https://www.leanexplore.com/?pkg=PhysLean instead of just https://www.leanexplore.com/. And call it "Search PhysLean" instead.

[Joseph Tooby-Smith]

There is also: https://leandex.projectnumina.ai which I believe is a newer version of leanexplore.

I think https://www.leanexplore.com/ allows you to search Mathlib and PhysLean simultaneously, whilst https://www.leanexplore.com/?pkg=PhysLean would only restrict you to PhysLean. I think most people would want the former (but I am happy to change this on the PhysLean website if not). I agree using "Search PhysLean" on the website would be better.

We also use to have a version of Loogle for PhysLean but it got too expensive to host.

Concerning EPR paradox - we do not currently have it, and I think it would be a great addition. It would also help us build more in the Quantum Mechanics direction.

[Rein Zustand]

I tried and I was able to add both Mathlib and PhysLean as contexts: https://www.leanexplore.com/?pkg=PhysLean&pkg=Mathlib.

[Rein Zustand]

https://leandex.projectnumina.ai/?pkg=Mathlib&pkg=PhysLean&use_llm=true is indeed better than leanexplore.com.

[Joseph Tooby-Smith]

Good to know - when I get chance I will update the website

[Joseph Tooby-Smith]

(I've updated the website, including the things discussed here)