Zulip Chat Archive

Stream: triage

Topic: PR #7274: feat(archive/100-theorems-list): add proof of t...

Random Issue Bot (Oct 10 2021 at 14:18):

Today I chose PR 7274 for discussion!

feat(archive/100-theorems-list): add proof of thm 81
Created by @Manuel Candales (@manuelcandales) on 2021-04-20
Labels: awaiting-author, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

Scott Morrison (Oct 11 2021 at 01:22):

Random Issue Bot said:

Today I chose PR 7274 for discussion!

feat(archive/100-theorems-list): add proof of thm 81
Created by Manuel Candales (@manuelcandales) on 2021-04-20
Labels: awaiting-author, merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

Unfortunately the author disappeared. It's a complete proof, but we asked for some further documentation / human-readability.

Yury G. Kudryashov (Oct 11 2021 at 01:25):

BTW, I'd like to see a theorem saying that ∑k1pkr\sum_k \frac{1}{p_k^r} converges iff 1<r1 < r somewhere in src/analysis, not in archive.

Heather Macbeth (Oct 11 2021 at 01:33):

There was also a second attempt ongoing, right?
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20Reciprocal.20Series
which I think led to
#9457

Random Issue Bot (Nov 17 2021 at 14:19):

Today I chose PR 7274 for discussion!

feat(archive/100-theorems-list): add proof of thm 81
Created by @Manuel Candales (@manuelcandales) on 2021-04-20
Labels: awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

Last updated: Dec 20 2023 at 11:08 UTC