Vi ved fra Gödel at opgaven med et bevise sande matematiske udsagn ikke kan automatiseres, men dette resultat udelukker ikke muligheden af at man kan opnå interessante matematiske resultater, også i form af beviser, ved at benytte computere til at afsøge store datamængder. Det store spørgsmål er om et sådant bevis også kan føre til indsigt af værdi for det videre arbejde med at forstå de sammenhænge, der ligger bag et matematisk faktum.
Selv om dette spørgsmål har været diskuteret siden fremkomsten af Haken og Appels bevis for firefarvesætningen kan det ikke siges at være afklaret endnu, og indhenter man en mening herom fra en matematiker vil den formentlig i ret høj grad være ideologisk begrundet.
Nærværende skrift, og den tilhørende forelæsning, beskriver et eksperiment som berører denne problemstilling. Eksperimentet er uafsluttet og kan ikke siges at have ledt frem til nogen konklusion af værdi for afklaringen af det store spørgsmål herover.