Une preuve correcte ?

Deux mathématiciens de l'Université de Liverpool, Alexei Lisitsa and Boris Konev, dans un préprint 
sur Arxiv soulèvent le problème suivant : Si une preuve d'un théorème, fournie par un ordinateur, 
est trop grosse pour être validée, doit on considérer le théorème comme prouvé ? Les deux 
mathématiciens ont prouvé à l'aide d'un code une partie du problème connu comme
"Erdős discrepancy problem"—mais le fichier produit occupe 13-gigabytes !! 
Plus de détails sur : 
http://phys.org/news/2014-02-math-proof-large-humans.html 

A pair of mathematicians, Alexei Lisitsa and Boris Konev of the University of Liverpool, U.K., have come up with an interesting problem—if a computer produces a proof of a math problem that is too big to study, can it be judged as true anyway? In a paper they've uploaded to the preprint server arXiv, the two describe how they set a computer program to proving a small part of what's known as "Erdős discrepancy problem"—the proof produced a data file that was 13-gigabytes in size—far too large for any human to check, leading to questions as to whether the proof can be taken as a real proof.

Read more at: http://phys.org/news/2014-02-math-proof-large-humans.html#jCp

A pair of mathematicians, Alexei Lisitsa and Boris Konev of the University of Liverpool, U.K., have come up with an interesting problem—if a computer produces a proof of a math problem that is too big to study, can it be judged as true anyway? In a paper they've uploaded to the preprint server arXiv, the two describe how they set a computer program to proving a small part of what's known as "Erdős discrepancy problem"—the proof produced a data file that was 13-gigabytes in size—far too large for any human to check, leading to questions as to whether the proof can be taken as a real proof.

Read more at: http://phys.org/news/2014-02-math-proof-large-humans.html#jCp