Zulip Chat Archive
Stream: new members
Topic: Lucas-Lehmer converse
Alastair Irving (Jun 20 2025 at 10:59):
I see that in NumberTheory.LucasLehmer the converse, necessity, direction is a TODO. If noone is currently working on this I was thinking of proving it. It doesn't look to difficult for my first contribution to Mathlib.
Kenny Lau (Jun 20 2025 at 11:00):
Welcome to mathlib!
Kevin Buzzard (Jun 20 2025 at 12:56):
Give it a try!
Alastair Irving (Jun 24 2025 at 16:06):
I've done this in #26272. It was rather longer than I'd expected.
Kenny Lau (Jun 24 2025 at 16:19):
Congratulations! :tada:
Last updated: Dec 20 2025 at 21:32 UTC