Using HOL4 to prove Fermat's Little Theorem

nicta.com.au

29 pointsColinWright3 comments

For bonus points, use it to prove the "other" FLT...

Where the "bonus points" would probably be a Fields Medal if you could mechanically crank out a proof of Fermat's Last Theorem.

I read it as Fermat's Last theorem.