{"id":896,"date":"2016-10-10T16:31:57","date_gmt":"2016-10-10T15:31:57","guid":{"rendered":"http:\/\/xmau.com\/wp\/ilpost\/?p=896"},"modified":"2016-10-14T12:37:26","modified_gmt":"2016-10-14T11:37:26","slug":"dimostrazioni-umane","status":"publish","type":"post","link":"https:\/\/xmau.com\/ilpost\/2016\/10\/10\/dimostrazioni-umane\/","title":{"rendered":"Dimostrazioni “umane”?"},"content":{"rendered":"

Un paio di settimane fa Paolo Marino<\/a> mi ha segnalato questo articolo<\/a> in cui Sir Andrew Wiles (quello della dimostrazione dell’Ultimo teorema di Fermat, per chi non se lo ricordasse) parla di come lui vede le dimostrazioni di teoremi fatte al computer. Senza volere certo paragonarmi a Wiles, provo a raccontare come la penso io. Vi anticipo subito che non dir\u00f2 nulla di definitivo o troppo specifico.<\/p>\n

Per prima cosa, bisogna mettere in chiaro che “dimostrazione al computer” pu\u00f2 significare varie cose. Il grande pubblico – “grande” si fa per dire – ha scoperto questo concetto quando Kenneth Appel e Wolfgang Haken annunciarono di avere dimostrato il Teorema dei quattro colori<\/a> usando un computer per verificare tutte le possibili configurazioni. Detta cos\u00ec per\u00f2 la cosa non \u00e8 affatto vera: quello che i due matematici in realt\u00e0 fecero fu dimostrare (a mano, con qualche centinaio di pagine di testo) che esisteva un certo (grande) numero di “configurazioni inevitabili”, nel senso che se ci fosse stato un controesempio al teorema doveva contenere almeno una di tali configurazioni. La parte al computer \u00e8 servita a dimostrare che a partire da ciascuna configurazione inevitabile se ne poteva ricavare una con un numero minore di regioni che avrebbe fatto da controesempio, il che era assurdo per ipotesi. Una dimostrazione di questo tipo \u00e8 essenzialmente esaustiva: non nel senso che ci si esaurisce per farla ma che si limita a fare tanti, tanti calcoli che un essere umano non riesce a verificare ma un computer s\u00ec. Certo, il programma che fa questi conti potrebbe avere dei bachi: e infatti la dimostrazione \u00e8 stata fatta usando due computer con architetture hardware diverse, ciascuno dei quali usava un algoritmo essenzialmente diverso scritto da persone diverse. In questo modo la probabilit\u00e0 di avere un errore si riduce essenzialmente a zero, ed \u00e8 minore di quello di un errore in una dimostrazione “umana”. Ricordo tra l’altro che proprio il teorema dei quattro colori si \u00e8 creduto essere stato dimostrato tra il 1879 e il 1890, prima che ci si accorgesse che la dimostrazione non era completa.<\/p>\n

Nel campo dell’intelligenza artificiale esiste per\u00f2 un altro concetto di dimostrazione al computer, ed \u00e8 quella nel quale il computer applica una serie di passaggi logici per arrivare dalle ipotesi di un teorema alla tesi. Questo, se ho ben capito, \u00e8 il vero tema dell’articolo di Spektrum, e qui la cosa diventa in effetti pi\u00f9 interessante. I Principia Mathematica<\/a><\/i> funzionano in un certo senso in quel modo: \u00e8 notorio che per arrivare a dimostrare che 1+1=2 occorre arrivare a pagina 379 (nella prima edizione dell’opera: la seconda ha usato qualche scorciatoia e d\u00e0 la dimostrazione a pagina 362). Di nuovo, i singoli passi della dimostrazione sono chiaramente comprensibili a un essere umano, ma non credo che costui riesca a concepire la dimostrazione complessiva. Noi siamo abituati a saltare passaggi su passaggi, chi pi\u00f9 chi meno: \u00e8 vero che quello che per alcuni \u00e8 uno “sketch of proof” per altri \u00e8 una dimostrazione completa, ma anche la dimostrazione pi\u00f9 pedante d\u00e0 per scontati una serie di passaggi logici che non abbiamo certo voglia di esplicitare. Del resto, a meno che non ci chiamiamo Tristram Shandy, nemmeno nella vita reale specifichiamo mai completamente tutto quello che dobbiamo fare, no?<\/p>\n

Il vero problema che potremo avere nel futuro \u00e8 proprio questo. Un teorema dimostrato per esaustione \u00e8 un conto: un tipico matematico storcer\u00e0 il naso dicendo che la dimostrazione non \u00e8 elegante, magari potr\u00e0 mettersi a cercarne una migliore, ma il pi\u00f9 delle volte se ne far\u00e0 una ragione. In fin dei conti la sostanza gli \u00e8 chiara, e la parte al computer sono meri dettagli tecnici. Ma un computer che fa una dimostrazione logica la potr\u00e0 fare in maniera completamente incomprensibile per noi ad alto livello (ripeto: i singoli passi saranno sempre comprensibili). Questo perch\u00e9 noi umani ci organizziamo tipicamente per imitazione degli altri umani, e quindi abbiamo una linea comune di pensiero. Non \u00e8 un caso che Ramanujan, che non aveva questa educazione formale e anzi non aveva inizialmente nemmeno chiaro il concetto di dimostrazione, fu inizialmente snobbato da tutti, e Hardy decise di andare pi\u00f9 a fondo solo perch\u00e9 ritenne che nessuno si sarebbe potuto inventare quegli enunciati, e che valeva la pena di verificare se fossero dimostrabili oppure no. Un computer non opera per imitazione, lo vediamo con i sistemi di intelligenza artificiale che “imparano a giocare” a scacchi o a go e dei quali non abbiamo alcuna idea riguardo alla loro configurazione interna o al motivo per cui ogni tanto scelgono delle mosse incomprensibili. Se un computer facesse una dimostrazione che richiede decine di migliaia di passi logici dei quali noi non capiamo la logica sottostante, potremmo riconoscere che la dimostrazione \u00e8 corretta – ci sono tecniche standard per validare una dimostrazione – e quindi il teorema \u00e8 vero, ma non sapremmo affatto il perch\u00e9<\/i> \u00e8 vero. Finiremmo insomma nella situazione di chi sta vincendo a un gioco di cui non riesce a capire le regole, cosa che per un matematico \u00e8 una tragedia immane, visto che dal suo punto di vista il vero scopo della matematica \u00e8 appunto trovare le regole. \u00c8 bellissimo avere una struttura per un edificio pi\u00f9 leggera e allo stesso tempo pi\u00f9 robusta di quelle classiche, e un ingegnere giustamente non si preoccupa di come sia stata trovata tale struttura: ma un matematico si sentir\u00e0 a disagio. \u00c8 vero che questo scenario non pare ancora prossimo: ma ci pensate? Tra i tanti lavori che l’automazione soppianter\u00e0, potrebbe esserci anche quello del matematico!<\/p>\n","protected":false},"excerpt":{"rendered":"

Qual \u00e8 la vera differenza tra le dimostrazioni matematiche fatte dagli umani e dai computer? \u00c8 una questione complicata.<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"default","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","ast-disable-related-posts":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""}},"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":true,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"activitypub_content_warning":"","activitypub_content_visibility":"","activitypub_max_image_attachments":4,"activitypub_interaction_policy_quote":"anyone","activitypub_status":"","footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2},"jetpack_post_was_ever_published":false},"categories":[1],"tags":[54,162],"class_list":["post-896","post","type-post","status-publish","format-standard","hentry","category-uncategorized","tag-dimostrazioni-al-computer","tag-filosofia-della-matematica"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_shortlink":"https:\/\/wp.me\/phh2yP-es","jetpack-related-posts":[{"id":398,"url":"https:\/\/xmau.com\/ilpost\/2010\/07\/27\/il-teorema-di-pitagora\/","url_meta":{"origin":896,"position":0},"title":"Il teorema di Pitagora","author":".mau.","date":"27\/07\/2010","format":false,"excerpt":"Il teorema pi\u00f9 famoso della geometria merita indubbiamente una trattazione a s\u00e9.","rel":"","context":"In \"geometria\"","block_context":{"text":"geometria","link":"https:\/\/xmau.com\/ilpost\/tag\/geometria\/"},"img":{"alt_text":"[la costruzione euclidea del teorema di Pitagora]","src":"https:\/\/i0.wp.com\/xmau.com\/wp\/ilpost\/wp-content\/uploads\/sites\/4\/2014\/09\/pitagora-euclide.png?resize=350%2C200","width":350,"height":200},"classes":[]},{"id":2481,"url":"https:\/\/xmau.com\/ilpost\/2012\/02\/23\/quando-i-matematici-sbagliano\/","url_meta":{"origin":896,"position":1},"title":"Quando i matematici sbagliano","author":".mau.","date":"23\/02\/2012","format":false,"excerpt":"Perch\u00e9 preoccuparsi delle smentite in fisica? Persino in matematica una dimostrazione non \u00e8 sempre corretta.","rel":"","context":"Similar post","block_context":{"text":"Similar post","link":""},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":756,"url":"https:\/\/xmau.com\/ilpost\/2016\/03\/18\/il-premio-abel-2016-a-sir-andrew-wiles\/","url_meta":{"origin":896,"position":2},"title":"Il premio Abel 2016 a sir Andrew Wiles","author":".mau.","date":"18\/03\/2016","format":false,"excerpt":"Il suo contributo non sar\u00e0 forse stato \"profondo\", ma sicuramente ha avuto un'enorme influenza.","rel":"","context":"In \"Andew Wiles\"","block_context":{"text":"Andew Wiles","link":"https:\/\/xmau.com\/ilpost\/tag\/andew-wiles\/"},"img":{"alt_text":"[Mica capita a tutti di avere un edificio a proprio nome!]","src":"http:\/\/www.abelprize.no\/aim\/dnva\/75\/52\/storage\/file.image.jpg\/Scale?geometry=516x510","width":350,"height":200},"classes":[]},{"id":2614,"url":"https:\/\/xmau.com\/ilpost\/2013\/06\/03\/matematica-per-analogie\/","url_meta":{"origin":896,"position":3},"title":"Matematica per analogie","author":".mau.","date":"03\/06\/2013","format":false,"excerpt":"Non \u00e8 che i matematici predichino bene e razzolino male: il punto \u00e8 che loro sono inconsciamente abituati a distinguere la scoperta di una propriet\u00e0 dalla sua dimostrazione, ma si dimenticano di mostrare il momento della scoperta.","rel":"","context":"Similar post","block_context":{"text":"Similar post","link":""},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":445,"url":"https:\/\/xmau.com\/ilpost\/2011\/09\/13\/prima-di-godel\/","url_meta":{"origin":896,"position":4},"title":"Prima di G\u00f6del…","author":".mau.","date":"13\/09\/2011","format":false,"excerpt":"I teoremi di incompletezza di G\u00f6del hanno segnato la fine della sicurezza che i matematici hanno avuto per 2500 anni. Cosa \u00e8 successo prima che arrivasse lui?","rel":"","context":"In \"logica\"","block_context":{"text":"logica","link":"https:\/\/xmau.com\/ilpost\/tag\/logica\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":2648,"url":"https:\/\/xmau.com\/ilpost\/2013\/10\/26\/godel-dio-e-repubblica\/","url_meta":{"origin":896,"position":5},"title":"G\u00f6del, Dio e Repubblica","author":".mau.","date":"26\/10\/2013","format":false,"excerpt":"Stamattina mia moglie mi aveva detto di aver letto qualcosa oggi su Repubblica a riguardo di due ricercatori che avevano \"dimostrato il teorema di G\u00f6del\". Ammetto di non averci fatto troppo caso, non ero nemmeno troppo sveglio. Poi mi \u00e8 capitato di vedere su Facebook la condivisione di questo articolo\u2026","rel":"","context":"Similar post","block_context":{"text":"Similar post","link":""},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]}],"_links":{"self":[{"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/posts\/896","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/comments?post=896"}],"version-history":[{"count":2,"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/posts\/896\/revisions"}],"predecessor-version":[{"id":898,"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/posts\/896\/revisions\/898"}],"wp:attachment":[{"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/media?parent=896"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/categories?post=896"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/xmau.com\/ilpost\/wp-json\/wp\/v2\/tags?post=896"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}