ProofWiki y la verificación de las demostraciones matemáticas

ProofWiki es un compendio de demostraciones matemáticas escritas de manera colaborativa en una wiki. Su objetivo es colecionar y clasificar demostraciones de teoremas matemáticos.

El proyecto empezó en marzo de 2008 y actualmente incluye 2.804 demostraciones escritas por sus 297 usuarios. Las demostraciones se encuentran clasificadas en 34 categorías. Una de las categorías particularmente interesante es la de teoremas con nombres en la que aparecen 247 teoremas. También es interesante la página de los teoremas más populares según el número de visitas.

ProofWiki podría servir de base para otro proyecto cuyo objetivo final fuese la verificación formal de las demostraciones matemáticas. Para ello se podría crear una wiki y, de forma colaborativa, escribir las verificaciones de las demostraciones de ProofWiki usando los distintos sistemas de razonamiento asistido por ordenador (como Isabelle/HOL/Isar, PVS, ACL2, Coq, HOL, HOL Light o Mizar).