{"id":36357,"date":"2026-03-18T16:46:48","date_gmt":"2026-03-18T15:46:48","guid":{"rendered":"https:\/\/xmau.com\/wp\/notiziole\/?p=36357"},"modified":"2026-03-18T16:46:48","modified_gmt":"2026-03-18T15:46:48","slug":"first-proof-quando-il-gioco-si-fa-duro","status":"publish","type":"post","link":"https:\/\/xmau.com\/notiziole\/2026\/03\/18\/first-proof-quando-il-gioco-si-fa-duro\/","title":{"rendered":"First Proof: quando il gioco si fa duro…"},"content":{"rendered":"

Un paio di settimane fa, nella mia rubrica su MaddMaths! (come? non la leggete? male!), scrissi<\/a> che il progetto First Proof aveva preparato dieci lemmi mai pubblicati da dimostrare in una settimana, e che gli LLM erano riusciti a farcela solo in due casi. A quanto pare questo era il risultato che gli ideatori della gara erano riusciti a fare con le versioni “ufficiali” dei programmi. In realt\u00e0 sia OpenAI<\/a> che Google<\/a> con il suo Aletheia dicono di aver risolto cinque (o sei, se si accetta una dimostrazione incompleta) problemi. E la cosa pi\u00f9 interessante \u00e8 che non sono gli stessi: insieme i due software hanno dimostrato otto dei dieci lemmi.<\/p>\n

Come riporta Scientific American<\/a>, non \u00e8 chiaro se questi risultati dipendano dal fatto che internamente queste aziende hanno modelli pi\u00f9 avanzati di quelli pubblicamente disponibili, oppure c’\u00e8 stato un qualche aiutino da parte di matematici umani, anche se Google lo ha decisamente negato. La domanda non \u00e8 affatto peregrina. Penso che ormai sia sdoganato il fatto che un’IA riesca a fare almeno in parte il lavoro di un dottorando – s\u00ec, devo ancora studiarmi i cicli di Claude<\/a> che sono piaciuti cos\u00ec tanto a Knuth – anche sfruttando la loro capacit\u00e0 di trovare nella vastissima letteratura idee simili da portare avanti. In fin dei conti \u00e8 ben noto questo racconto di Julia Robinson: “Luned\u00ec – cercato di dimostrare teorema. Marted\u00ec – cercato di dimostrare teorema. Mercoled\u00ec – cercato di dimostrare teorema. Gioved\u00ec – cercato di dimostrare teorema. Venerd\u00ec – il teorema \u00e8 falso”. Traduciamolo nel mondo degli LLM: essi possono produrre centinaia di “dimostrazioni” che si scopre poi essere false, perch\u00e9 assumono ipotesi non necessariamente vere. I sistemi di verifica automatica buttano via queste dimostrazioni errate e l’IA non si abbatte e ricomincia; diciamo per\u00f2 che se un essere umano vede quello che potrebbe essere un approccio interessante e spinge il sistema in quella direzione \u00e8 molto pi\u00f9 facile arrivare al risultato finale. <\/p>\n

Per ovviare a questo problema, il gruppo dietro First Proof sta preparando una seconda gara, ma questa volta chieder\u00e0 di poter far girare lui stesso i programmi, per essere certi che non ci sia aiuto esterno. Vedremo (a) se i produttori di questi sistemi accetteranno e (b) che succeder\u00e0. <\/p>\n","protected":false},"excerpt":{"rendered":"

anche i matematici cominciano a fare sul serio<\/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":false,"_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":3,"activitypub_interaction_policy_quote":"anyone","activitypub_status":"federated","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":[1023,30,1033,214],"tags":[],"class_list":["post-36357","post","type-post","status-publish","format-standard","hentry","category-ia-2026","category-ia","category-matelight-2026","category-matematica_light"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/phh2yV-9sp","jetpack-related-posts":[{"id":36830,"url":"https:\/\/xmau.com\/notiziole\/2026\/04\/20\/non-fatevi-creare-una-password-dalle-ia\/","url_meta":{"origin":36357,"position":0},"title":"Non fatevi creare una password dalle IA","author":".mau.","date":"2026-04-20","format":false,"excerpt":"almeno fino a quando non aggiungeranno una apposita routine","rel":"","context":"In "ia 2026"","block_context":{"text":"ia 2026","link":"https:\/\/xmau.com\/notiziole\/category\/ia\/ia-2026\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":32997,"url":"https:\/\/xmau.com\/notiziole\/2025\/07\/03\/si-puo-eliminare-ai-overview-dai-risultati-di-ricerca-google\/","url_meta":{"origin":36357,"position":1},"title":"Si pu\u00f2 eliminare AI Overview dai risultati di ricerca Google?","author":".mau.","date":"2025-07-03","format":false,"excerpt":"La risposta \u00e8 \"per il momento s\u00ec, anche se a fatica: in futuro chiss\u00e0\".","rel":"","context":"In "IA e informatica"","block_context":{"text":"IA e informatica","link":"https:\/\/xmau.com\/notiziole\/category\/ia\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":4810,"url":"https:\/\/xmau.com\/notiziole\/2007\/03\/11\/de_mauro_il_dizionario\/","url_meta":{"origin":36357,"position":2},"title":"De Mauro (il dizionario)","author":".mau.","date":"2007-03-11","format":false,"excerpt":"mistero informatico: tutto a un tratto il software decide di mangiarsi l'ultima lettera delle parole.","rel":"","context":"In "IA e informatica"","block_context":{"text":"IA e informatica","link":"https:\/\/xmau.com\/notiziole\/category\/ia\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":9504,"url":"https:\/\/xmau.com\/notiziole\/2013\/10\/16\/bussola_dantan\/","url_meta":{"origin":36357,"position":3},"title":"bussola d’antan","author":".mau.","date":"2013-10-16","format":false,"excerpt":"Occhei, oggi sono tutti a farsi la \"bussola politica\". Io l'avevo fatto dieci anni fa. Qualcuno sa dirmi se \u00e8 cambiato qualcosa? No, perch\u00e9 avrei altro da fare... Aggiornamento: (17 ottobre) ho perso dieci minuti di pausa pranzo per verificare se ero nato incendiario e morto pompiere. Dieci anni fa\u2026","rel":"","context":"In "io"","block_context":{"text":"io","link":"https:\/\/xmau.com\/notiziole\/category\/io\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":33070,"url":"https:\/\/xmau.com\/notiziole\/2025\/07\/12\/proof-ebook\/","url_meta":{"origin":36357,"position":4},"title":"Proof (ebook)","author":".mau.","date":"2025-07-12","format":false,"excerpt":"Cos'\u00e8 in effetti una dimostrazione?","rel":"","context":"In "rec-2025"","block_context":{"text":"rec-2025","link":"https:\/\/xmau.com\/notiziole\/category\/recensioni\/recensioni-2025\/"},"img":{"alt_text":"copertina","src":"https:\/\/i0.wp.com\/xmau.com\/notiziole\/wp-content\/uploads\/sites\/6\/2025\/07\/9781782838999.jpg?resize=350%2C200&ssl=1","width":350,"height":200},"classes":[]},{"id":20259,"url":"https:\/\/xmau.com\/notiziole\/2020\/04\/01\/il-mio-postino-ha-finito-la-quarantena\/","url_meta":{"origin":36357,"position":5},"title":"Il mio postino ha finito la quarantena","author":".mau.","date":"2020-04-01","format":false,"excerpt":"Dopo due settimane abbondanti, \u00e8 arrivata la posta.","rel":"","context":"In "milano"","block_context":{"text":"milano","link":"https:\/\/xmau.com\/notiziole\/category\/milano\/"},"img":{"alt_text":"","src":"https:\/\/i0.wp.com\/xmau.com\/notiziole\/wp-content\/uploads\/sites\/6\/2020\/04\/posta-1024x978.jpg?resize=350%2C200&ssl=1","width":350,"height":200,"srcset":"https:\/\/i0.wp.com\/xmau.com\/notiziole\/wp-content\/uploads\/sites\/6\/2020\/04\/posta-1024x978.jpg?resize=350%2C200&ssl=1 1x, https:\/\/i0.wp.com\/xmau.com\/notiziole\/wp-content\/uploads\/sites\/6\/2020\/04\/posta-1024x978.jpg?resize=525%2C300&ssl=1 1.5x"},"classes":[]}],"jetpack_likes_enabled":true,"jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/posts\/36357","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/comments?post=36357"}],"version-history":[{"count":1,"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/posts\/36357\/revisions"}],"predecessor-version":[{"id":36358,"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/posts\/36357\/revisions\/36358"}],"wp:attachment":[{"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/media?parent=36357"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/categories?post=36357"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/xmau.com\/notiziole\/wp-json\/wp\/v2\/tags?post=36357"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}