Looking for Mertens in and out of Mathlib; KWIC

Stream: new members

[J. J. Issai (project started by GRP)]

The immediate goal is to find and use in Lean a result of the following form: Given natural number k, $\sum_{p < k \le p^2} 1/p < 0.7$, where the sum runs over primes $p$. (I may have to settle for 0.71, the limiting value should approach log 2 $\approx 0.69$. If I want $k < 5$, I have to settle for 0.84.) With a lot of work and for large k, this is a consequence of one of Franz Mertens' theorems in number theory. (See this entry .) So I would like to find if this has been done in Lean

Using loogle and LeanExplore, nothing relevant seems to come up. (I will try some other searches as well.) However, I understand that these and other tools only look at databases for Mathlib. Do they also look at other repositories as well?

In olden times, something that I found useful was a KWIC (KeyWord-In-Context) file, which is an expanded index formed from a document that contains fragments which have the keyword in them. Is there a similar or equivalent feature for searching a repository other than Mathlib for what I seek? Does Github have a search option that provides a KWIC feature or equivalent? What would be a good way to search another github repository. Finally, can/should/does Mathlib have a (monthly) updated KWIC index? (I'm imagining the keywords are more natural language and do not include Lean language elements or theorem names; the index is primarily of the docstrings.)

[Snir Broshi]

https://deepwiki.com/AlexKontorovich/PrimeNumberTheoremAnd
Has the usual downsides of LLMs, but works for any repo, for free.

[Snir Broshi]

Example session: https://deepwiki.com/search/find-theorems-about-the-sum-of_5a8f143e-d3a9-412a-a88c-1bf424c0278c?mode=fast

[J. J. Issai (project started by GRP)]

This is more than I had before. Thanks.