Zsigmondy's theorem

Stream: Is there code for X?

[Ardith El-Kareh]

Is there some form of Zsigmondy's theorem in Mathlib? On the 1000+ Theorems page there's an entry for it but no link to code: https://leanprover-community.github.io/1000.html

[Yaël Dillies]

@Mantas Baksys was working on it three years ago. It didn't make it to mathlib, and all I am aware of is this Lean 3 file, but maybe he has a more recent version lying around?

[Mantas Baksys]

This is indeed the last version I worked on. The proof should be straight-forward to translate to Lean 4 if there is a desire to push it into Mathlib. I never aimed to polish the proof into a Mathlib ready version, so it never made it in as a result.

[Ardith El-Kareh]

Thanks. Are there any tips for translating Lean3 to Lean4?

[Kim Morrison]

https://github.com/leanprover-community/mathport

[Yury G. Kudryashov]

I have a proof in Lean 4 I wrote for Harmonic, and I've got a permission to opensource it. I'm going to open a sequence of PRs today and tomorrow.

[Yury G. Kudryashov]

See #28895. It still needs a lot of cleanup before merging.

[Yury G. Kudryashov]

@Mantas Baksys The Lean 3 file says (C) @Johan Commelin , then doesn't list Johan in Authors:. What's the right attribution?

[Yury G. Kudryashov]

For now, I copied the copyright header, then added @Alex J. Best and myself (we've ported/rewritten it in Lean 4 and more Mathlib-like style).

[Michael Rothgang]

Would you like to add your formalisation to 1000.yaml also?

[Mantas Baksys]

Yury G. Kudryashov said:

Mantas Baksys The Lean 3 file says (C) Johan Commelin , then doesn't list Johan in Authors:. What's the right attribution?

I think @Johan Commelin helped quite a bit with the proof IIRC, so should be added to Authors list too.