Zulip Chat Archive
Stream: general
Topic: quadratic reciprocity
Kenny Lau (Oct 10 2018 at 20:19):
@Mario Carneiro do you feel like quadratic_reciprocity.lean has too many long theorems?
Chris Hughes (Oct 10 2018 at 20:33):
I wasn't too happy with that aspect of the proof, but it is quite difficult to avoid.
Last updated: May 02 2025 at 03:31 UTC