Ongoing Lean formalization of the proof for Fermat's Last Theorem
1–10 of 81 posts
Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem
#2Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?
Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem
#3Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?
You're either underestimating the length of the proof, or overestimating the length of tasks that models can currently accomplish.
Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem
#4Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?
You're either underestimating the length of the proof, or overestimating the length of tasks that models can currently accomplish.
The blueprint is a step-by-step outline.
Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem
#5This is a nice overview of what this is, why they're doing it and why it's many years of work:
https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER...
Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem
#6Are there any graphics that show the massive progress to date in some symbolic form?
Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem
#7Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem
#8Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?
This is a significantly harder problem than winning gold in IOM. A large part of it is figuring out how to represent some of the relevant ideas in Lean at all.
Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem
#9Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?
"The International Mathematical Olympiad (IMO) is the World Championship Mathematics Competition for High School students", so not to undermine it but it's below university or graduate level.
Research level mathematics like this is as hard as it gets, and this proof is famously difficult: uses many branches of advanced mathematics, required thousands of pages of proofs, years of work.
Re: Ongoing Lean formalization of the proof for Fermat's Last Theorem
#10Since the proof already exists in human-written form, I'm wondering, can't OpenAI's IOM gold winning algorithm not translate the blueprint to lean?
"The International Mathematical Olympiad (IMO) is the World Championship Mathematics Competition for High School students", so not to undermine it but it's below university or graduate level. Research level mathematics like this is as hard as it gets, and this proof is famously difficult: uses many branches of advanced mathematics, required thousands of pages of proofs, years of work.
Yes but the hard work (coming up with a human-readable proof) has already been done.