Zulip Chat Archive
Stream: FLT-regular
Topic: A paper mentioning formalizing FLT regular
Alex J. Best (Sep 05 2022 at 14:23):
I just stumbled across a master thesis that talks about the prospect of formalizing FLT regular in 2010! https://scholarworks.calstate.edu/downloads/3b591917r I don't think they did any formalization work, but just tried to give explicit proofs of some components, nevertheless quite funny that this has been on peoples minds for so long
Riccardo Brasca (Sep 05 2022 at 14:26):
It seems to only discuss case I, that is very natural once one have (as we do) unique factorization of ideals!
Riccardo Brasca (Sep 05 2022 at 14:27):
BTW I will resume working on the project tomorrow, I think we can finish case I pretty quickly now
Chris Birkbeck (Sep 06 2022 at 09:19):
Yeah hopefully case 1 is close. I should be able to get back to this in a couple of weeks. But my plan was to also start planning out a strategy for case 2 (or at least put some more details in the blueprint)
Alex J. Best (Sep 05 2022 at 14:23):
I just stumbled across a master thesis that talks about the prospect of formalizing FLT regular in 2010! https://scholarworks.calstate.edu/downloads/3b591917r I don't think they did any formalization work, but just tried to give explicit proofs of some components, nevertheless quite funny that this has been on peoples minds for so long
Riccardo Brasca (Sep 05 2022 at 14:26):
It seems to only discuss case I, that is very natural once one have (as we do) unique factorization of ideals!
Riccardo Brasca (Sep 05 2022 at 14:27):
BTW I will resume working on the project tomorrow, I think we can finish case I pretty quickly now
Chris Birkbeck (Sep 06 2022 at 09:19):
Yeah hopefully case 1 is close. I should be able to get back to this in a couple of weeks. But my plan was to also start planning out a strategy for case 2 (or at least put some more details in the blueprint)
Last updated: Dec 20 2023 at 11:08 UTC