Le Monde en Coq

Cette page présente une tentative de formaliser en Coq les problèmes proposées par le journal Le Monde en 2013 comme énigmes mathématiques. Pour chaque problème, nous présentons la vidéo qui décrit le problème et le fichier Coq correspondant. Ces fichiers utilisent l'extension Ssreflect.

Palindrome

La vidéo

alt : PalVilani.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves).

Cube

La vidéo

alt : CubeVilani.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves).

Grille

La vidéo

alt : cohen_grille.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves).

Allumette

La vidéo

alt : CohenAllumette.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves).

Cordes

La vidéo

alt : Cordes.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves).

Nombre mystère

La vidéo

alt : NombreMystere.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves).

Verre

La vidéo

alt : Verre.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves).

Chapeaux

La vidéo

alt : Chapeau.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves).

Parking

La vidéo

alt : Parking.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves [merci cyril!]).

Terre

La vidéo

alt : Terre.flv

Le fichier Coq

Le fichier avec définitions et théorèmes (+ les preuves).