# Project Ideas

Now that you know the basics of Coq you are itching to prove something. Here are some ideas.

Other than formalizing existing proofs, one useful exercise is to update some of Coq's user-contributed libraries so that they build on the recent additions in the Coq StandardLibrary rather than their own foundations.

## Fermat Last Theorem for n = 3

### Statement

`forall (x y z:Z), x^3 + y^3 = z^3 -> x=0 \/ y= 0 \/ z=0`

### Resources

http://nshmyrev.narod.ru/temp/fermat4.tar.gz start of the proof.

### Estimated Difficulty

|{}| |{}| |{o}| |{o}| |{o}| |{o}| |{o}| |{o}| (change the estimate if you disagree)

(none)

## Fermat Last Theorem

### Statement

`forall (x y z:Z) (n:nat), x^(n+3) + y^(n+3) = z^(n+3) -> x=0 \/ y= 0 \/ z=0`

### Resources

Fermat's last theorem has been proven in Coq for the n=4 case. The proof is available in UserContributions/CNAM/Fermat4/ .

### Estimated Difficulty

|{}| |{}| |{}| |{}| |{}| |{}| |{}| |{}| (change the estimate if you disagree)

(none)

## Lusin Separation Theorem

### Informal Statement

Any strongly disjoint pair of analytic sets is strongly Borel sepearable.

Peter Aczel has a proof in constructive ZF. It should be possible to translate this proof into type theory.

### Estimated Difficulty

|{}| |{}| |{}| |{}| |{o}| |{o}| |{o}| |{o}| (change the estimate if you disagree)

## Conway's Cosmological Theorem

### Informal Statement

The maximal length of an atom in the splitting of a 50-day-old string is 74. Every such atom decays, in at most 17 days, into stable or transuranic elements.

### Estimated Difficulty

??? (change the estimate if you disagree)

(none)

# Completed Projects

## Tarski's Undefinability of Truth

This has now been completed by Wouter Stekelenburg.

## Elliptic Curve Primality Proving

This has now been completed. See http://coqprime.gforge.inria.fr/

##### Clone this wiki locally
You can’t perform that action at this time.
Press h to open a hovercard with more details.