Noong Mayo, nagbunga ng di-inaasahang sagot ang tanong tungkol sa mga tuldok sa isang patag na ibabaw. Pagsapit ng Setyembre, naglalathala na ang mga AI laboratoryo ng mga argumento tungkol sa mga singularidad ng likido, kasama ang mga file na magagamit ng mga kompyuter para suriin ang mga patunay. Sa pagitan ng mga anunsiyong iyon, lumitaw ang mga bagong kontra-halimbawa, mas mahigpit na hangganan at pormalisasyon ng Huling Teorema ni Fermat.
Higit pa sa sunod-sunod na bilang ng mga napabulaang haka-haka ang nararapat na pagsusuri sa pagbabago ng matematikang AI. Magkakaibang tanong ang sinasagot ng mga resultang ito, iba-iba ang ebidensiya at may sari-sariling hindi pa tapos na gawain. Maaaring mapabagsak ng kontra-halimbawa ang isang paniniwala nang hindi nito nahahanap ang pinakamainam na sagot. Maaaring mahalaga ang pinahusay na hangganan habang bukas pa rin ang tanyag na haka-haka. Maaaring magpatunay ang kompyuter sa isang pahayag nang hindi ipinapaliwanag kung bakit kapaki-pakinabang sa ibang lugar ang mga ideya nito.
Sinusuri namin dito ang mahahalagang pag-unlad mula sa anunsiyo ng OpenAI noong Mayo 20 tungkol sa unit distance hanggang sa pahayag nitong Navier–Stokes noong Setyembre, batay sa pag-uulat hanggang Setyembre 22, 2026. Kasama rito ang mahahalagang anunsiyo sa pagitan at pananaliksik na sumunod sa mga ito. Mapa ito ng magkakaugnay na pangyayaring iyon, hindi kumpletong imbentaryo ng bawat papel sa matematika na tinulungan ng AI. Binasa namin ang mga binanggit na anunsiyo, kaugnay na pahayag ng mga teorema, pambungad ng pananaliksik at dokumentasyon ng beripikasyon. Hindi namin malayang sinuri bilang tagahatol ang mga patunay o muling binuo ang mga pormalisasyon.
Dalawa ang pinakamalakas na ebidensiya ng pag-unlad, sa aming pagtatasa: lumilikha ang mga makina ng mga argumentong matematikal na nararapat suriing mabuti, at nakabuo na ang mga tao ng karagdagang matematika mula sa ilan sa mga argumentong iyon. Nakadepende sa pondong ilalaan sa pagsusuri, pagpapaliwanag at pagpapalawak kung magiging tuluy-tuloy ang pag-unlad.
Mayo: nagbubukas ng bagong landas sa heometriya ang isang kontra-halimbawa
Madaling isipin ang problema sa unit distance. Maglagay ng magkakahiwalay na punto sa patag na ibabaw at bilangin ang mga pares na eksaktong isang yunit ang pagitan. Habang nagdaragdag ka ng mga punto, gaano karami ang pinakamataas na maaaring maging bilang?
Iniugnay ng anunsiyo ng OpenAI noong Mayo 20 ang bagong konstruksyon sa isang panloob na modelong pangkalahatang pangangatwiran na sinubok sa koleksiyon ng mga problema ni Erdős. Naglathala rin ito ng hiwalay na kasamang papel ng mga matematikong mula sa labas na nagsuri sa argumento. Mahalaga ang ikalawang dokumento: makikita ng mga mambabasa kung ano ang naunawaan at muling binuo ng mga matematikong iyon, lampas sa salaysay ng laboratoryo tungkol sa modelo nito. Anunsiyo ng OpenAI.
Bumubuo ang orihinal na manuskrito ng walang-hanggang dami ng hanay ng mga punto na may hindi bababa sa n^(1+δ) pares na may unit distance, para sa isang nakapirming positibong δ. Sa payak na pananalita, nananatili ang pagbuti sa eksponente habang lumalaki ang mga halimbawa. Sumasalungat ito sa ipinagpalagay na halos linyar na paglaki. Hindi nito tinutukoy ang eksaktong pinakamataas na bilang ng unit distance para sa bawat bilang ng mga punto, at nagpapatuloy ang mas malawak na paghahanap sa pinakamainam na hangganan. Manuskrito tungkol sa unit distance.
Nakagugulat kung saan nagmula ang konstruksyon. Inuugnay ng kasamang papel ang resultang heometriko sa masalimuot na teorya ng alhebraykong bilang at pinapangalanan ang mga naunang ambag sa matematika. Nagmumungkahi ang mga may-akda nito ng pinasimple at bahagyang pinalawak na muling pagbubuo. Kapaki-pakinabang itong halimbawa ng gawaing pantao matapos ang tuklas ng AI: tukuyin ang mekanismo, ilantad ang mga pinagkakabatayang ideya at gawing kayang hawakan ng ibang mananaliksik ang argumento. Kasamang papel ng mga matematiko.
Dapat samakatuwid na sundan ng mambabasang gustong maunawaan ang halaga ng resulta noong Mayo ang mga sumunod na papel kasinlapit ng unang anunsiyo. Nagkakaroon ng ibang uri ng kredibilidad ang bagong teknik kapag ginagamit ito ng mga mananaliksik para magtanong at sumagot ng mga karagdagang tanong.
Mayo hanggang Hulyo: nagsisimulang kumalat ang mga ideya
Noong Mayo 27, naglabas sina Thomas Bloom, Will Sawin, Carl Schildkraut at Dmitrii Zhelezov ng kontra-halimbawa sa haka-hakang sum-product sa mga tunay na bilang. Sa pangkalahatan, tumutukoy ito sa laki ng paglaki ng isang hanay kapag pinagdaragdag o pinaparami ang mga elemento nito. Pinahihintulutan ng kanilang konstruksyon na manatiling mas maliit sa ipinagpalagay na halos kuwadratikong sukat ang dalawang resultang hanay. Tahasang sinabi ng mga may-akda na nag-udyok sa kanilang muling isaalang-alang ang mga field ng bilang na may mataas na antas ang kontra-halimbawa sa unit distance. Ipinaliwanag din nilang mas kaunting teorya ng bilang ang kailangan ng pinal nilang konstruksyon kaysa sa naunang resulta. Papel tungkol sa sum-product.
Kongkretong halimbawa ito ng resultang nagmula sa AI na nagpasigla ng matematikang isinulat ng tao. Hindi nito pinatutunayang AI ang sumulat sa kasunod na papel, at hindi natin dapat burahin ang mga may-akda nito sa pamamagitan ng pagsama sa kanilang gawain sa bilang ng tagumpay ng laboratoryo.
Iniuugnay ng preprint ni Cosmin Pohoata, unang isinumite noong Hunyo 11 at binago noong Hunyo 28, ang sunod-sunod na pag-unlad sa problema ni Elekes–Rónyai. Nagbibigay ito ng halimbawa ng polinomyal na mas mabagal lumaki ang mga halaga sa angkop na mga hanay kaysa sa inaasahan, gamit ang mga sangkap mula sa kamakailang mga konstruksyon ng unit distance at sum-product. Tahasang ipinakikita sa papel ang ugnayan ng mga problema. Papel ni Pohoata.
Noong Hulyo 6, naglabas sina Sungchul Lee, Pohoata at Daniel Zhu ng karagdagang resulta tungkol sa grid ni Minkowski. Napapanatili ng kanilang konstruksyon ang katangian ng paulit-ulit na distansiya sa loob ng mga subset, na may mga implikasyon sa mga tanong tungkol sa paulit-ulit na distansiya at mga tatsulok na isosceles. Mas matibay na estruktura ito kaysa pagpapakita ng iisang di-pangkaraniwang saganang ayos ng mga punto nang hindi sinusuri ang panloob na asal nito. Papel tungkol sa grid ni Minkowski.
May ebidensiya rito para sa positibong pagbasa. Nagbigay ang resulta noong Mayo ng materyal na naibago at nagamit muli ng ibang mananaliksik sa loob lang ng ilang linggo. Iminumungkahi naming sukatin ang tagumpay batay sa pagbuo ng gayong mga paraang magagamit, kasabay ng pagsisikap na kailangan para maunawaan ang mga ito. Hindi makukuha ang pagkakaibang ito sa basta pagbibilang ng mga nalutas na problema.
Hulyo: ipinakikita ng kontra-halimbawa sa haka-hakang Jacobian kung bakit mahalaga ang saklaw
Tungkol naman sa haka-hakang Jacobian ang ikalawang kapansin-pansing pangyayari. Sinusuri sa paliwanag matematikal ni Terence Tao noong Hulyo 21 ang kontra-halimbawang nabuo sa tulong ng Fable AI: isang polinomyal na pagmamapa sa tatlong kompleks na baryable na umaasal na baligtarin sa maliit na paligid pero nagpapadala ng magkakaibang punto sa iisang kalalabasan sa kabuuan. Hindi totoo ang pangkalahatang pahayag ng haka-haka sa tatlo o higit pang dimensiyon; nananatiling bukas ang kasong may dalawang dimensiyon. Nagbibigay si Tao ng tahasang mga pormula at nagpapaliwanag sa heometriya ng konstruksyon. Paliwanag matematikal ni Tao.
Dahil tahasan, maaaring mas madaling kalkulahin ang mahalagang pagsasalungat sa isang kontra-halimbawa. Nangangailangan ng karagdagang gawaing matematikal ang pagtuklas kung bakit dapat umiral ang gayong halimbawa at kung paano bumuo ng kaugnay nito. Ipinakikita sa inilathalang materyal tungkol sa Jacobian ang pagkakaiba ng mga gawaing iyon.
Mahalaga pa rin ang pagkakaibang ito noong Setyembre. Nagmumungkahi ang preprint ni Arno van den Essen noong Setyembre 15 ng payak na landas tungo sa kontra-halimbawang katumbas, matapos baguhin nang linyar ang mga koordinado, ng halimbawang natagpuan ni Levent Alpöge. Bagong paliwanag ito sa konstruksyon, hindi ikalawang malayang pagpapabagsak sa orihinal na haka-haka. Papel ni van den Essen.
Para sa tagapamahala ng pananaliksik, nagmumungkahi ito ng praktikal na pagbabago sa dapat gantimpalaan. Maaaring makapagbukas ng kasindaming kasunod na gawain ang pagpopondo sa taong nagpapauunawa sa masalimuot na tuklas at pagpopondo sa isa pang paghahanap ng resultang bibida sa balita. Pagtataya namin ito sa serye ng mga pag-unlad, hindi pahayag na binago na ng mga unibersidad ang kanilang mga insentibo.
Agosto: mas malawak na hanay ng mga pahayag sa matematika
Nagpakita ang inilabas ng OpenAI noong Agosto 1 ng sampung pangkat ng resulta sa matematika at teoretikal na agham pangkompyuter. Ayon sa kumpanya, panloob na bersiyon ng Astra ang bumuo ng mga argumento; nakipagtulungan ang mga tao sa modelo para ihanda ang mga manuskrito, at gumawa ng mga Lean certificate ang modelo. Naiiba ang salaysay na ito ng paggawa sa nag-iisang resulta noong Mayo, at tahasan nitong inilalarawan ang ambag ng paghahanda sa manuskrito. Anunsiyo noong Agosto.
Inilalahad sa kasamang koleksiyon, na in-update noong Agosto 6, ang mga sumusunod. Paglalarawan ito sa mga pahayag ng manuskrito, hindi sampung magkakahiwalay na sertipikasyon ng BIG CHANGE:
- Pagkakasiksik ng mga esfera: mas matalas na asimptotikong itaas na hangganan sa matataas na dimensiyon.
- Mga binary at spherical code: mas mahihigpit na limitasyon sa laki ng code sa mga tinukoy na pagitan.
- Teorya ng grupo: konstruksyon ng grupong hindi sofic.
- Mga alhebra ng operator: mga kontra-halimbawa sa haka-haka sa rigididad ni Connes.
- Kompleksidad sa aritmetika: mas mahihigpit na ibabang hangganan ng sirkito at pormula para sa permanente.
- Mga larong quantum: teorema ng eksponensiyal na paulit-ulit na paralelismo.
- Mga problema sa lattice: mas mahihigpit na resultang mahirap lapitan sa tantiya ng problema sa pinakamalapit na bektor.
- Kombekso na heometriya: patunay sa haka-haka sa bolyum ni Ehrhart.
- Teorya ni Ramsey: super-eksponensiyal na ibabang hangganan sa mga bilang ni Ramsey para sa maraming kulay ng tatsulok.
- Teorya ng ekstremal na grap: mga kontra-halimbawa sa mga haka-haka sa compactness at degeneracy.
Koleksiyon ng pananaliksik sa sampung resulta.
Mahalaga ang lawak ng mga paksang ito, pero nagiging mapanlinlang din ang iisang pinagsama-samang bilang. Magkakaiba ang implikasyon ng paghahanap ng kontra-halimbawa, pagpapahusay sa hangganan at pagpapatunay ng pangkalahatang teorema. Hindi rin awtomatikong katibayan ng pag-atake sa aktuwal na sistemang kriptograpiko ang resulta tungkol sa hirap ng problemang matematikal. Kailangan ng sariling hanay ng pangangatwiran at ebidensiya ang mga aplikasyon.
Noong Agosto 10, naglathala ang Anthropic ng mas makitid na tinukoy na pagsulong na may kaugnayan sa haka-haka ni Riemann. Ayon dito, pinahusay ng hindi pa inilalabas na modelo ng Claude ang ibabang hangganan sa proporsiyon ng mga serong zeta na nasa kritikal na linya. Sinuri ng mga matematiko ng Anthropic ang gawain, nirepaso ng mga espesyalista mula sa labas ang papel, at nagawa ang pormalisasyon. Tahasang sinasabi ng kumpanya na hindi nilutas ni Claude ang haka-haka ni Riemann at hindi rin nito inaasahang malulutas ito ng mga teknik na iyon. Paliwanag ng Anthropic.
Nagtatakda ang naka-link na papel ng hangganang bahagyang mas mataas sa dalawang-katlo, mga 67.25%, at tinutukoy ang naunang resultang analitikal na ginamit nito. Pahayag ito sa asimptotikong matematika, hindi pahayag na napapatunayan ang haka-haka sa pagsuri ng malaking may hangganang sampol ng mga sero. Mahalaga ang pagkakaiba: hindi nangangahulugan ang ibabang hangganan sa proporsiyon na nasa linya ang bawat serong may kaugnayan. Manuskrito tungkol sa mga sero ng zeta.
Umiikot din ang iba pang ambisyosong manuskrito. Nagmumungkahi ang dokumentong inilagay sa website ni Alpöge ng kompleks na estruktura sa anim-na-dimensiyong esfera. Maaaring suriin ang konstruksyon nito, pero hindi tinutukoy sa kopyang na-access namin ang maaasahang petsa ng anunsiyo o kumpletong salaysay sa ambag ng AI. Isinasama namin ito bilang panukalang maaaring siyasatin ng mga mambabasa, nang hindi ito itinataas bilang hiwalay na napatunayang mahalagang yugto sa kronolohiyang ito. Manuskrito tungkol sa anim-na-dimensiyong esfera.
Unang bahagi ng Setyembre: inilalantad ng mga agwat sa prime ang hangganan ng beripikasyon
Umabot din ang sunod-sunod na anunsiyo sa mga agwat sa pagitan ng mga prime number. Sinasabi sa paunang papel ng kolaborasyong Axiom noong Setyembre 3 na hindi lalampas sa 212 ang agwat ng walang-hanggang dami ng magkasunod na pares ng prime. Kinikilala nito ang analitikal na gawain ni Julia Stadlmann at ng naunang proyektong Polymath. Ipinagpapalagay din ng Lean certificate nito ang mga analitikal na tantiya at hiwalay na napatunayang certificate ng baryasyon. Isinusulong nito ang tanong tungkol sa may-hanggang agwat; hinihingi naman ng haka-haka sa kambal na prime ang walang-hanggang dami ng agwat na eksaktong dalawa. Papel ng pangkat ng Axiom.
Nagpapakita ang pampublikong imbakan ng PrimeGaps186 ng OpenAI ng mas maliit pang hangganan, pero may mahalagang paglilinaw. Nakabatay sa tatlong panimulang aksioma ang Lean development nito: dalawang tantiya mula sa literatura at mga numerikal na hangganan ng integral. Ayon sa imbakan, hindi pinatutunayan ng numerikal na certificate ang mga aksiomang iyon. Dapat samakatuwid ibukod ng mga mambabasa ang iminungkahing argumentong matematikal sa bahaging pormal na nasuri batay sa tinukoy na mga input. Hindi wastong ilarawan ang artifact na ito bilang walang-kondisyong ganap na pormal na patunay mula lang sa mga pundamental na aksioma. Imbakan ng PrimeGaps186.
Tinutugunan naman ng isa pang manuskrito ng OpenAI ang mahahabang agwat: kung gaano kalaki ang maaaring maging mga pagitan ng magkasunod na prime. Iniuulat nito ang pinahusay na ibabang hangganan para sa pinakamahabang agwat sa ibaba ng lumalaking hangganan. Hiwalay na tanong sa ekstremal na matematika ito sa paghahanap ng walang-hanggang dami ng magkalapit na pares ng prime; hindi dapat ituring na solusyon sa isa ang pag-unlad sa isa pa. Manuskrito tungkol sa mahahabang agwat.
Dahil sa mga detalyeng ito, partikular na kapaki-pakinabang ang pangyayari tungkol sa agwat ng mga prime. Maaaring magmukhang simpleng paligsahan ang dalawang bilang sa isang headline. Kapag nakita na ang mga pinagbabatayang kailangan ng patunay, mas mabuting itanong kung aling hakbang ang napatunayan sa anong paraan. Kapaki-pakinabang ang tahasang paglalahad ng mga palagay kahit hindi pa kumpleto ang pormalisasyon.
Setyembre 4: nagiging bahagi ng kuwento ng tuklas ang pormalisasyon
Tungkol sa teoremang alam na ang patunay sa matematika ang anunsiyo ng Anthropic noong Setyembre 4: ang Huling Teorema ni Fermat. Ang ipinapahayag na tagumpay ay kumpletong pormalisasyon sa Lean na halos kusang ginawa ni Claude sa loob ng labing-isang araw. Inilalarawan ng kumpanya ang patnubay ng tao at plataporma ng kolaborasyong tumulong sa mga agent na subaybayan ang mga dependency. Kinikilala rin nito ang tradisyon ng patunay sa matematika na pinagbabatayan ng gawain. Anunsiyo tungkol sa pormalisasyon.
Nagbibigay ang pampublikong imbakan ng mas tiyak na ebidensiya kaysa sa headline. Inilalahad nito ang teorema, itinatala ang mga dependency at dinodokumento ang mga pagsusuri laban sa mga karaniwang aksioma ng Lean at bersiyon ng pahayag sa Mathlib. Inilalarawan din nito ang sarili bilang artifact ng pananaliksik na hindi pinananatili. Sinuri namin ang dokumentasyong ito; hindi namin muling pinatakbo ang build. Imbakan ng FLT.
Kung makatutulong sa pormalisasyon ang mga kaparehong tool na lumilikha ng mas maraming posibleng argumento, maaari ring lumaki ang kapasidad para sa pagsusuri. Malaking dahilan ito para umasa. Nagkakaroon ang mga susunod na mananaliksik ng kongkretong susuriin. Kailangan pa rin nilang malaman kung madaling gamitin muli ang mga pansamantalang resulta, kung maaari pang buuin ang mga dependency at kung sino ang nagpapanatili sa artifact. Hindi masasagot ng dami lang ng nalikhang code ang mga tanong na ito.
May mahalagang pasiyang institusyonal dito. Maaaring ilabas ng laboratoryo ang patunay bilang tapos nang pagpapamalas sa modelo nito, o suportahan ito bilang imprastrakturang gagamitin pa ng iba. Magkaibang obligasyon pagkatapos ng araw ng paglulunsad ang lilitaw sa bawat pamamaraan. Dapat isama sa badyet ng pananaliksik ang pagpapanatili, mga halimbawang nagpapaliwanag at matatag na reperensiya.
Setyembre 8: ano talaga ang sinasabi ng resulta tungkol sa Navier–Stokes
Mas malinaw na naitutuon ng resulta tungkol sa likido ang mga tanong na ito. Inilalahad sa anunsiyo ng OpenAI noong Setyembre 8, na in-update noong Setyembre 10, ang iminungkahing solusyon sa problema ng pag-iral at pagiging makinis ng Navier–Stokes. Iniuugnay nito ang gawain sa panloob na modelong nagpapatakbo sa pamamagitan ng mga nag-uugnayang agent, at inilalabas nito ang nakasulat na argumento at pormalisasyon sa Lean. Sinasabi ng OpenAI na hindi nito balak angkinin ang Millennium Prize. Anunsiyo.
Paggalaw ng di-nasisiksik na likido sa tatlong dimensiyon, may positibong lagkit at maingat na binuong panlabas na puwersa ang saklaw ng manuskrito. Mula sa pahinga, nagkakaroon umano ng walang-hanggang bilis ang iminungkahing solusyon sa loob ng takdang panahon habang nananatiling may hangganan ang kabuuang enerhiya nito. Makinis ang puwersa at limitado ito sa espasyo at panahon. Gumagamit ang matematikal na konstruksyon nito ng bumabagsak na puyo at mga pagwawastong inayos para manatiling makinis ang natitirang puwersa. Mga pahayag ito tungkol sa solusyon sa mga ekwasyon, hindi obserbasyon mula sa pisikal na eksperimento o bagong simulator sa engineering. Manuskrito tungkol sa Navier–Stokes.
Mahalaga ang panlabas na puwersa para maunawaan ang saklaw. Pinahihintulutan ng opisyal na paglalarawan ni Charles Fefferman sa problema ng Clay ang makinis na puwersa sa mga alternatibong pagkabigo C at D. Tungkol naman ang mga alternatibong global na pagkamakinis A at B sa mga ekwasyong walang panlabas na puwersa. Kaya maaaring tumugon sa alternatibong tahasang pinahihintulutan ng Clay ang balidong resultang ganitong uri, habang nananatiling hindi nalulutas ang tanong sa global na regularidad na walang panlabas na puwersa. Magpapalaki sa teorema ang pagtawag na walang saysay sa puwersa; ilalarawan naman nang mali ang tuntunin kung tatanggihan itong labas sa nakasaad na problema. Opisyal na pahayag ng problema.
Naglabas din ang OpenAI ng hiwalay na argumento tungkol sa Euler, na tumatalakay sa idealisadong likidong walang lagkit. Iminumungkahi sa manuskrito nito ang pagkabigo sa loob ng takdang panahon mula sa makinis na panimulang datos at walang panlabas na puwersa. Magkaugnay na ekwasyon ang Euler at Navier–Stokes, pero dapat panatilihing magkahiwalay ang mga palagay at kongklusyon sa dalawang papel na ito. Manuskrito tungkol sa Euler.
Mahalaga ang kasaysayan ng nakapaligid na pananaliksik. Kinikilala sa pahayag ng European Mathematical Society noong Setyembre 10 ang mga ambag nina Córdoba, Martínez-Zoroa at Zheng, kasama nina Alpöge at Buckmaster at mga naunang ambag sa matematika. Nagtatanong din ito tungkol sa access, pag-akda at pagkilala. Nawawala ang naipong mga ideyang nagbigay-daan sa gawain sa salaysay na diretsong tumatalon mula sa pangalan ng modelo tungo sa teorema. Pahayag ng EMS.
Noong Setyembre 11, maingat na nagpahayag ng kasiyahan ang Clay tungkol sa tila resolusyon at sinabing sadyang hindi ito magmamadali sa pagsusuri at paghahati ng pagkilala. Makabuluhang tugon ito ng institusyon. Hindi ito paggawad ng premyo o pahayag na tapos nang repasuhin ang bawat bahagi ng gawain. Anunsiyo ng Clay.
Sapat na ang masusing kongklusyong ito para sa mga mambabasa nang walang dagdag: naglabas ang isang AI laboratoryo ng iminungkahing patunay para sa kinikilalang problema ng Millennium, kasama ang mga matematikal at pormal na artifact na maaaring siyasatin, at seryoso itong tinatalakay ng malalaking institusyon. Kailangan pang pagtrabahuhan ang mas malawak na pagtanggap, pagkilala at pag-unawa.
Tiyak na tanong ang sinasagot ng pagsusuri sa patunay
Binabago ng pormal na beripikasyon ang ebidensiyang makukuha ng mga reviewer. Dapat din nitong gawing mas tiyak ang pag-uulat.
Ibinubukod sa sariling dokumentasyon ng Lean ang balidong patunay sa kahulugan ng pahayag na pinatutunayan. Itinatatag ng matagumpay na batayang pagsusuri na sumusunod ang pormal na pahayag sa mga depinisyon at palagay nito. Maaaring ilantad ng karagdagang pagsusuri ang di-natapos na mga dependency, i-audit ang mga aksioma at ihambing ang patunay sa pahayag na tinukoy nang hiwalay. Inilalarawan sa dokumentasyon ang mas matibay na beripikasyon gamit ang panlabas na checker at tinutukoy pa rin nito ang mga natitirang palagay. Gabay ng Lean sa pagpapatunay.
Isipin ang mananaliksik na nangangailangan ng hangganang naaangkop sa bawat input ng algorithm. Nagbibigay ang assistant ng pormal na tamang teorema, pero hindi kasama sa depinisyon nito ng katanggap-tanggap na input ang mahirap na kategorya. Maaaring tama ang patunay habang wala pa ring suporta ang aplikasyon ng mananaliksik. Kathang-isip na halimbawa ito kung bakit kailangang suriin ang pagsasalin ng tanong tungo sa pormal na pahayag nito.
May ibang uri ng pagsusuri para sa pagiging bago ng tuklas. Hindi napagpapasiyahan ng sistema ng patunay kung lumitaw na ang parehong argumento sa ibang katawagan sa mas lumang papel, kung kumpleto ang pagkilala sa mga may ambag o kung may mahalagang binabago sa aplikasyon ang ipinahayag na pagbuti. Nangangailangan ng pagsusuri sa literatura at kaalaman sa larangan ang mga hatol na iyon.
Hihilingin namin samakatuwid sa laboratoryong naglalabas ng mahalagang resulta na magbigay ng matibay na pakete: eksaktong pahayag sa karaniwang wikang matematikal, katapat nitong pormal na pahayag kung mayroon, patunay at mga dependency, malinaw na paglalahad sa ambag ng tao at modelo, at talaan ng mga nasuri at nabagong bahagi. Iminungkahing pamantayan namin ito sa pag-uulat. Nagbibigay ito sa ibang mananaliksik ng paraan para matukoy ang pananagutan at ulitin ang kaugnay na mga pagsusuri.
Tinutugunan ng grupong tagapayo ang lumalaking hamon sa koordinasyon
Inilunsad ang Advisory Group on Mathematics and Artificial Intelligence noong Setyembre 21 sa gitna ng mga pangyayaring ito. Ayon sa grupo, malaya ito, walang bayad at handang magpayo sa sinumang kaugnay na kompanya ng AI. Agad nitong pinapayuhan ang OpenAI tungkol sa paglulunsad ng mga karagdagang resultang sinasabi ng kumpanya na nakuha nito. Nangangako ito ng pampublikong rekomendasyon at tahasang sinasabing wala itong kapangyarihang magpasya sa loob ng mga kumpanya. Panauhing post ng grupo ang anunsiyo sa blog ni Terence Tao. Pahayag ng grupo.
Inilalarawan ng OpenAI ang mandato bilang pagsusuri, komunikasyon, kahalagahan at pagpapakalat. Sinasabi rin nitong hindi tungkulin ng grupo na magpayo sa bilis ng panloob nitong pag-unlad sa matematika. Dapat samakatuwid unawain ang tungkulin ng tagapayo bilang daluyan ng pagsisiyasat at koordinasyon, habang nananatili sa kumpanya ang mga pasiya. Anunsiyo ng OpenAI tungkol sa grupong tagapayo.
May dahilan para ikatuwa ang kaayusang ito. Maaaring mabawasan ng mas mahusay na koordinasyon ang dobleng gawaing pagsusuri, matukoy ang angkop na mga espesyalista at matiyak na tugma ang paglalarawan ng resulta sa suportang ebidensiya. Gayundin kalinaw ang mga limitasyon nito: kailangan ng tugon sa payo, at hindi sapat ang pagiging malaya lang para maipatupad ito. Dapat subaybayan ng mga mambabasa ang inilalathalang rekomendasyon at ginagawa ng mga kumpanya tungkol dito.
Tungkol din sa layunin ng pananaliksik ang mapagdudang pananaw. Ikinakatuwiran sa pahayag na Math and AI noong Setyembre 11 na maaaring mapabayaan ng paligsahang lutasin ang mga nakalistang problema ang paglinang ng pag-unawa at pagsasanay sa mga susunod na matematiko. Ipinakikita ng mga lumagda ang panganib sa mga prosesong ginagawang madaling ituro at kapaki-pakinabang ang mga ideya. Seryosong paninindigan ito ng mga kalahok sa disiplina, hindi sukat na nagpapatunay na napinsala na ng lahat ng paggamit ng AI ang larangan. Pahayag.
Pinaunlad ni Henry Cohn ang kaugnay na argumento sa panauhing sanaysay niya noong Setyembre 15 sa blog ni Tao: maaaring magpataw ng malaking trabaho sa komunidad na sasalo sa mga resulta ang mga paliwanag na hindi malinaw. Kabilang sa pangamba niya ang mga insentibo para sa mga gumagawa ng gawaing nagpapaliwanag. Mahalaga rin dito ang wastong pagkilala; sanaysay ito ni Cohn kahit naka-host sa blog ni Tao. Sanaysay ni Cohn.
Dapat mas madaling magamit ng iba ang susunod na pagsulong
Sinusuportahan ng kongkretong mga halimbawa ang positibong pagbasa sa serye mula Mayo hanggang Setyembre. Nagpasigla ng karagdagang konstruksyon ang isang kontra-halimbawa sa heometriya. Nakahanap ang mga mananaliksik ng mas malinaw na paraan para ipaliwanag ang nakakagulat na polinomyal na pagmamapa. Nagluwal ang pormalisasyon ng karagdagang artifact na magagamit para siyasatin ang masalimuot na pangangatwiran. Nakikita na ang mga sangkap para sa mabungang ugnayan ng output ng modelo at gawaing matematikal.
Praktikal din ang pesimistikong senaryo. Maaaring mas mabilis lumikha ng mga iminungkahing resulta ang mga laboratoryo kaysa maunawaan ng iba ang mga ito, at ituring na tapos nang ambag sa agham ang mga anunsiyo. Maaaring ipapasan sa maliit na pangkat ng mga espesyalista ang pagsusuri habang dumadaloy naman sa mga sistemang lumilikha ng backlog ang mga mapagkukunan at prestihiyo. Maaari pang palalimin ng limitadong access sa mga modelo ang agwat ng mga lumilikha ng tuklas at mga inaasahang susuri rito.
Sa pananaw namin, dapat sukatin ng mga laboratoryo, tagapondo at journal ang magkabilang panig ng proseso. Subaybayan ang mga posibleng tuklas, pero subaybayan din ang malayang pagsisiyasat, kapaki-pakinabang na pagpapasimple, pagkukumpuni sa mga argumento, pormal na library na maaaring gamitin muli at kasunod na gawain. Kilalanin ang mga taong nagpapauunawa sa resulta. Ilathala ang mga pagwawasto nang kasingdalas ng mga anunsiyo.
Para sa mambabasang sumusubaybay sa susunod na malaking tuklas, tiyak ang pinakanakapagbibigay-liwanag na tanong: ano na ang kayang gawin ngayon ng ibang mananaliksik na hindi nila kayang gawin noon? Maaaring bumuo sila ng kontra-halimbawa, magtatag ng mas matibay na garantiya, magsuri ng mahirap na argumento o magturo ng bagong paraan. Dito nagiging pag-unlad sa matematika ang pag-unlad ng matematikang AI.
