Let me add another sentence from that Science News article, since not quite knowing what either "finite order arithmetic" or "simple type theory" means, this clarified things for me: ----- McLarty recently showed that Fermat’s Last Theorem can be proven using the ordinary axioms of mathematics, and even a bit less. ----- The article's author seems to say that the ordinary axioms of mathematics means "set theory", which I take to mean the ZF axioms, apparently without AC. --Dan On 2013-02-20, at 10:04 AM, Fred W. Helenius wrote:
On 2/19/2013 10:54 AM, Henry Baker wrote:
Q about the proof of FLT:
I realize that Fermat himself wouldn't recognize Wiles's proof, but would Fermat recognize the assumptions?
I.e., does the Wiles proof require any "exotic" assumptions -- e.g., axiom of choice, generalized Riemann hypothesis, etc. ?
When I answered this yesterday, I cited a 2010 article by Colin McLarty. He's been busy since, and my newsfeed this morning contained a headline from Science News about his work: "A mathematician puts Fermat's Last Theorem on an axiomatic diet" (http://www.sciencenews.org/view/generic/id/348403/description/A_mathematicia...). It's a fluffy article based on work McLarty announced at the recent Joint Meetings; here's the abstract for that talk, "Grothendieck's cohomology founded on finite order arithmetic":
Despite rumors to the contrary, Grothendieck and others published proofs using Grothendieck universes, which are sets so large that ZF does not prove they exist. Number theorists to this day cite those published proofs. More conservative references avoid universes but still use far stronger set theory than the number theory requires, such as large amounts of replacement. We describe the issues and show how to formalize the entire Grothendieck apparatus at the strength of finite order arithmetic (simple type theory with infinity) and describes progress towards yet weaker foundations. (Received September 18, 2012)
So he claims to have shown that Grothendieck's universes are not needed, but he's still a long way from Peano arithmetic.
-- Fred W. Helenius fredh@ix.netcom.com
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun