Glacann Lean le Cruthúnas Fermat Claude

Tá glactha ag Lean, na bogearraí seiceála cruthúnas a úsáideann matamaiticeoirí ar fud an domhain, le leagan foirmiúil iomlán de Theoirim Dheireanach Fermat. Níl aon chéimeanna ionadchoinneála gan réiteach, aon aicsímí breise ná aon aicearraí ríomhaireachtúla lasmuigh de ghnáthbhunsraitheanna Lean san fhoirmliú, a chruthaigh córas Claude de chuid Anthropic agus a foilsíodh mar stór oscailte (stór). Rinne Kevin Buzzard, matamaiticeoir in Imperial College London a bhí i gceannas ar a iarracht fhoirmlithe féin, an tionscadal a thiomsú go neamhspleách agus dheimhnigh sé go n-éiríonn leis na seiceálacha, á thabhairt air mar “éacht urghnách uathfhoirmiúlaithe” (Buzzard).

Réitíodh an mhatamaitic féin fadó. Chruthaigh Andrew Wiles an teoirim in 1995, agus ní raibh aon mhatamaiticeoir dáiríre in amhras faoin toradh. Is é a bhí fós le déanamh ná an cruthúnas sin a athscríobh mar threoracha do sheiceálaí litriúil, agus gach sainmhíniú agus céim idirmheánach a d’fhéadfadh an t-údar bunaidh a fhágáil intuigthe a sholáthar. Deir Anthropic gur chuir na mórán gníomhairí intleachta saorga an t-aistriú seo i gcrích in aon lá dhéag i mí Lúnasa, agus iad ag obair go comhthreomhar trí ardán darbh ainm Prove2Me (Anthropic).

Mar sin féin, baineann an tréimhse ama sin le próiseas nach féidir le daoine lasmuigh den tionscadal a atáirgeadh. Ní cuid den eisiúint phoiblí iad an tsamhail inmheánach, an bonneagar comhordaithe, cinntí na n-oibreoirí ná an caiteachas ríomhaireachta. Is féidir an déantán críochnaithe a atáirgeadh, áfach: is féidir le duine ar bith a bhfuil crua-earraí leordhóthanacha aige tionscadal Lean a aththiomsú agus a dheimhniú go n-éiríonn leis an gcruthúnas sna seiceálacha. D’fhíoraigh seiceálaí ar leith a scríobh Anthropic in Rust an déantán foirmiúil céanna, agus dheimhnigh sé go bhfuil na 1,052,234 dearbhú ar fad comhsheasmhach (tuarascáil theicniúil). Is athléamh eile é seo ar an téacs céanna, seachas athchruthú neamhspleách ar fheachtas an aon lá dhéag.

An chaoi ar oibrigh na gníomhairí

Is éard atá i gceist le cruthúnas a fhoirmliú ná argóint mhatamaiticeora a athscríobh sa chaoi gur féidir le ríomhchlár nach bhfuil aon iomas matamaiticiúil aige gach céim loighciúil a dheimhniú. Tá cuma shimplí mhealltach ar an teoirim féin: i gcás aon easpónant slánuimhreach atá cothrom le trí nó níos mó, níl trí shlánuimhir dhearfacha ar bith ann a shásaíonn aⁿ + bⁿ = cⁿ. Téann an cruthúnas, áfach, trí shraitheanna doimhne de theoiric na n-uimhreacha thar na céadta leathanach.

Níor aimsigh Claude matamaitic nua. Chuir sé i bhfoirm fhoirmiúil an slabhra seanbhunaithe torthaí as a dtagann cruthúnas Wiles, agus lean sé cur síos leis na matamaiticeoirí Henri Darmon, Fred Diamond agus Richard Taylor (Anthropic, tuarascáil theicniúil). Ba le Wiles agus lena réamhtheachtaithe an léargas cruthaitheach. Ba é cion Claude an léargas sin a aistriú go thart ar 10.5 milliún líne de chód is féidir le meaisín a sheiceáil (tuarascáil theicniúil).

Roinn ardán Prove2Me, a dhear taighdeoir Anthropic Tianyi Peng agus comhoibrithe in Ollscoil Columbia, an cruthúnas ina ghraf spleáchais ina raibh thart ar 29,511 maíomh neamhspleácha (tuarascáil theicniúil). Roghnaigh na gníomhairí maímh a bhí réidh, scríobh siad cruthúnais Lean dóibh agus sheiceáil siad na ráitis a mhol a chéile, agus iad ag obair go comhthreomhar. D’úsáid an feachtas thart ar sé bhilliún comhartha aschuir ó shamhail inmheánach taighde (tuarascáil theicniúil).

De réir Anthropic, níor scríobh oibreoirí daonna aon chód Lean le linn an phróisis, cé gur roghnaigh siad an teoirim, gur sholáthair siad bealach aitheanta an chruthúnais, gur dhear siad bonneagar na ngníomhairí agus gur athraigh siad tosaíochtaí ó am go chéile (Anthropic). Níor nochtadh tras-scríbhinn iomlán na n-oibreoirí ná na costais ríomhaireachta.

Tógtha ar bhlianta d’obair bhunaidh dhaonna

Bhí an toradh ag brath ar Mathlib, an leabharlann mhór matamaitice foirmiúlaithe a chothaíonn an pobal, agus bhain sé leas díreach as dhá thionscadal roimhe seo. Bhí foireann Buzzard in Imperial ag forbairt foirmliú Lean de Theoirim Dheireanach Fermat ó dheireadh 2023, le maoiniú ó dheontas £1 mhilliún ón EPSRC a bhí beartaithe go dtí 2029 (dámhachtain EPSRC). Bhí teoirim na bhfo-thacar cásanna curtha i bhfoirm fhoirmiúil cheana féin ag tionscadal pobail ar leith. Aithnítear i gcomhad sannacháin Anthropic 106 chomhad ina bhfuil ábhar a tógadh nó a cuireadh in oiriúint ó na hiarrachtaí sin (sannachán).

Mar gheall ar an gcur i gcrích comhthreomhar, ní féidir an t-aon lá dhéag féilire a chur i gcomparáid leis na huaireanta oibre daonna a chaith foireann Buzzard, a bhí i mbun oibre ar feadh thart ar 22 mí mhaoinithe nuair a thosaigh feachtas Claude (dámhachtain EPSRC). Níor nocht Anthropic líon na n-uaireanta GPU ná na costais fuinnimh.

Roimh an eisiúint seo, ba í Teoirim Dheireanach Fermat an mhír dheireanach a bhí fágtha ar liosta Freek Wiedijk de 100 teoirim thábhachtacha a bhí fós le cur i bhfoirm fhoirmiúil, slat tomhais a bhfuil dul chun cinn á rianú aici le fiche bliain (Buzzard).

Is é an tástáil is láidre ar cibé acu is féidir an cur chuige seo a ghinearálú ná matamaitic nua, nach bhfuil chomh maith sin doiciméadaithe, a chur i bhfoirm fhoirmiúil nuair nach bhfuil treoirphlean, leabharlanna aibí ná obair fhoirmiúil roimhe seo ann. Sa phróiseas seo, tástáladh teoirim cháiliúil a raibh bonneagar suntasach i bhfeidhm cheana féin ina leith. Léiríonn sé gur féidir le gníomhairí intleachta saorga, má thugtar bealach aitheanta cruthúnais agus obair fhoirmiúil roimhe seo dóibh, foirmliú iomlán a chruthú a nglacann Lean leis agus ar féidir le daoine eile é a athsheiceáil. Ní féidir an feachtas giniúna féin a atáirgeadh ón ábhar foilsithe.