Get the latest tech news

Fermat's Last Theorem – how it’s going

So I’m two months into trying to teach a proof of Fermat’s Last Theorem to a computer. We already have one interesting story, which I felt was worth sharing.

The basic idea here is that the classical exponential and logarithm functions play a key role in differential geometry (relating Lie algebras and Lie groups, for example), and in particular in understanding de Rham cohomology, but they do not work in more arithmetic situations (for example in characteristic p); the theory of “divided power structures”, developed in the 1960s in a series of beautiful papers by Roby, play a crucial role in constructing an analogue of these functions which can be used in the arithmetic case. The thing I want to stress is that it was absolutely clear to both me and Antoine that the proofs of the main results were of course going to be fixable, even if an intermediate lemma was false, because crystalline cohomology has been used so much since the 1970s that if there were a problem with it, it would have come to light a long time ago. [For those that are interested in more technical details, here they are: Berthelot’s thesis does not develop the theory of divided powers from scratch, he uses Roby’s “Les algebres a puissances divisees”, published in Bull Sci Math, 2ieme serie, 89, 1965, pages 75-91.

Get the Android app