Skip to content

A proof of Fermat's theorem on sum of two squares with mathcom using gaussian integers.

Notifications You must be signed in to change notification settings

thery/twoSquare

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

25 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

twoSquare

Docker CI

A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two files :


gauss_int.v : the definition of gaussian integers

fermat2.v : the proof of Fermat's theorem


The final statement reads:

From mathcomp.contrib.sum_of_two_square Require Import fermat2.

Check sum2stest.

sum2stest :

reflect (forall p, prime p -> odd p -> p %| n -> odd (logn p n) -> p %% 4 = 1) (n is a sum_of_two_square).

Meta

Building and installation instructions

To build and install manually, do:

git clone https://github.com/thery/twoSquare.git
cd twoSquare
make   # or make -j <number-of-cores-on-your-machine> 
make install