La última demostración matemática asistida por ordenador ocupa 16 Gb y es más grande que el contenido de toda la Wikipedia. Se trata de la demostración, para discrepancias de 1 y 2, del Problema de Larga Discrepancia de Erdős, propuesto en 1930 por el extravagante y prolífico matemático húngaro Paul Erdős. Estas "matemáticas no-humanas", en palabras de uno de los investigadores, son tan largas que no podrán ser revisadas por ningún ser humano por lo que algunos matemáticos se preguntan si deben formar parte de su disciplina.