Claude alithibitisha Fermat katika siku 11. Hukumu: SHIP IT.

Nini video hii inashughulikia

• Claude anafanya rasmi Nadharia ya Mwisho ya Fermat katika Lean 4
• Chromium sandbox RCE (CVE-2026-85046), iliyotumika vibaya, zawadi ya $1,000
• Shin Jin-seo amemshinda KataGo akiwa na kizingiti cha mawe mawili

Nakala iliyotafsiriwa

Imetafsiriwa kutoka simulizi asili ya Kiingereza. Sauti na manukuu yanayopatikana yanadhibitiwa na YouTube.

0:00 Fermat alisema uthibitisho wake mzuri haungefaa kwenye ukingo, na leo Anthropic imechapisha ukingo: mistari milioni kumi na tatu ya Lean, mara tano ukubwa wa Mathlib, ikithibitisha nadharia kila mwanahisabati tayari aliamini. Ilikuwa saa kumi au kumi na moja huko Tbilisi wakati Anthropic ilipochapisha, kwa hivyo nilikuwa macho. Jana Google ilisafirisha Chrome 152 na marekebisho kumi na mawili ya usalama, mojawapo ikiwa ni mdudu wa V8 tayari umetumiwa vibaya, na kumlipa mtoa taarifa dola elfu moja, ambayo ni chini ya gari tutakalolijadili baadaye.

0:26 Pia jana, Mullvad alisema inafunga DNS yake ya umma iliyosimbwa kwa njia fiche mnamo Novemba 2 na kumlipa Quad9 kufanya hivyo badala yake, na asubuhi hii Rust React Compiler iliingia asili huko Vite, huku Hacker News ikigundua IBM Bob, wakala wa kuweka nambari wa AI. Kisha Claude alifanya rasmi Nadharia ya Mwisho ya Fermat, na kwenye ukurasa huo wa mbele gwiji wa Kikorea alimshinda injini yenye nguvu zaidi ya Go Duniani, kwa hivyo leo binadamu walifanya moja kati ya mbili. Katika video hii: Claude alichothibitisha, iligharimu nini,

0:52 kwa nini mwanahisabati aliyetumia taaluma yake juu ya hili anasema haibadilishi chochote na amefurahi hata hivyo, na jinsi binadamu alivyoshinda mashine huko Go. Ni Ijumaa, Septemba 4, na hii ni The Daily Diff. Nadharia ya Mwisho ya Fermat: hakuna nambari kamili chanya a, b, c zinazokidhi a hadi n pamoja na b hadi n sawa na c hadi n kwa n yoyote zaidi ya 2. Fermat aliiandika kwenye ukingo karibu mwaka 1637 na akafa bila kuonyesha kazi yake, akimfanya kuwa msanidi programu wa kwanza kufunga tiketi na "works on my machine". Tuzo ya mwaka 1908 ya alama 100,000 za dhahabu ilivutia uthibitisho 621 mbaya

1:25 katika mwaka wake wa kwanza, na Andrew Wiles hatimaye aliipata mwaka 1995, katika kurasa 129 ambazo ziliwachukua waamuzi miezi mingi kuzithibitisha. Kufanya rasmi kunamaanisha kuandika upya uthibitisho huo ili Lean, msaidizi wa uthibitisho, aweze kuangalia kila hatua kiufundi, na Kevin Buzzard huko Imperial ameongoza juhudi za binadamu kufanya hivyo tangu 2024; mpango pekee unachukua kurasa 86. Mtafiti wa Anthropic Tianyi Peng alielekeza mawakala kadhaa wa Claude juu yake badala yake, kwenye jukwaa liitwalo Prove2Me ambalo lina DAG ya taarifa za nadharia ili mawakala wajue nini cha kuthibitisha kinachofuata, kwa sababu bila hiyo

2:00 makundi ya kwanza walipoteza uelewa wa nani alikuwa akithibitisha nini, jambo ambalo ndilo hutokea wakati safu yako ya uratibu ni regex yenye bajeti ya masoko. Siku kumi na moja baadaye nodi ya mizizi ilisomeka IMEKWISHATHIBITISHWA: mistari milioni kumi na tatu ya Lean, nadharia za kati 29,500, takriban tokeni bilioni sita za matokeo kutoka kwa modeli ya ndani inayofanana na Claude Fable 5.1. Ujenzi unashindwa isipokuwa uthibitisho unategemea kabisa aksimu tatu za kawaida za Lean: hakuna samahani, hakuna uamuzi wa asili, hakuna udanganyifu. Kuiangalia si bei rahisi pia: ujenzi

2:29 kutoka mwanzo ulichukua saa tano na nusu kwenye cores 96 na gigabaiti 153 za RAM, na majina ya nadharia ni yanayotokana na mashine, kwa hivyo hifadhi inajieleza kama imeandikwa ili ichunguzwe badala ya kusomwa, ambayo pia ndivyo ningeelezea Java ya kampuni. Sasa utata. Chapisho la Anthropic linasema Lean inaonyesha usahihi bila shaka. Kevin Buzzard, mwanamume aliyechoshwa na hilo, alikusanya hifadhi kwenye mashine ya gigabaiti 500 Anthropic aliyemkopesha, alithibitisha inathibitishwa, kisha akaandika,

2:56 nukuu, kihisabati kazi hii haituelezi chochote muhimu. Alikuwa tayari na uhakika wa asilimia 99.9 kuwa nadharia ilikuwa kweli, na uthibitisho hauna hisabati mpya; inachoonyesha ni kile ambacho uwekaji rasmi wa kiotomatiki unaweza kufanya sasa, na sehemu hiyo amefurahishwa kweli. Alipewa pauni milioni moja kwa miaka mitano; Anthropic ilichukua siku kumi na moja, na hesabu ya leso ya mtoa maoni inaweka tokeni bilioni sita za matokeo kwa bei ya orodha. takriban dola 300,000, kwa hivyo mashine ilikuwa nafuu, isipokuwa uhesabu mafunzo ya mashine, ambayo hakuna anayefanya.

3:24 Maelezo bora: barua pepe ilifika akiwa kwenye tamasha la muziki huko Wales akiwa na 4G bar moja, kutoka kwa jina ambalo hakuwahi kulisikia, kwa hivyo aliichukulia kama utapeli na kuisoma wiki moja baadaye, ambayo ni jibu sahihi kwa kichwa chochote cha somo kilicho na uundaji rasmi wa mwisho-hadi-mwisho. Wakati huo huo, wanadamu walipata ushindi mmoja. Shin Jin-seo, nambari moja duniani katika Go, alimshinda KataGo, injini ya Go yenye nguvu zaidi ya chanzo wazi, michezo miwili kwa mmoja huko Seoul na jiwe la handicap mbili, takriban pengo kati ya mtaalamu wa juu na mtaalamu mgeni.

3:50 Uamuzi ulikuwa ushindi wa pointi 11.5 katika hatua 221, akishikilia uwezekano wa ushindi wa asilimia 99 kutoka katikati ya mchezo na kuendelea, na alichukua nyumbani milioni 250 won, takriban dola 170,000, pamoja na Genesis G90, kwa hivyo zawadi kwa kushinda AI isiyo ya kibinadamu ni mara 170 ya zawadi ya Google kwa sandbox ya Chrome kutoroka. Maelezo yake: mapema alinakili hatua za AI na kupoteza; alishinda kwa kujenga bodi kwa mtindo wake mwenyewe, ambayo ni ushauri muhimu zaidi kuhusu AI niliyosikia mwaka mzima, na ulitoka kwenye mchezo wa bodi. Mistari mingine miwili katika mabadiliko.

4:22 Kompailaji wa Rust React kutoka oxc sasa ni asili katika Vite nyuma ya bendera moja; msimbo wa faili 1,036 ulitoka sekunde 14.3 hadi 0.81 katika hatua ya kukompaila, hasa kwa kufuta Babel kutoka package.json, ambayo pia ni utaratibu wangu wa utunzaji wa ngozi. Na IBM ilizindua Bob, mshirika wa usimbaji wa AI anayekusalimu na Hujambo, Mimi ni Bob, huzalisha wasaidizi wadogo, huweka msimbo mkuu wa mainframe kisasa, na husafirisha bidhaa ya uchanganuzi iitwayo Bobalytics, kwa hivyo mahali fulani benki inafurahi sana na hakuna mtu aliyesoma leseni.

4:51 Hiyo ni faida kubwa kwa Ijumaa moja; ikiwa ungependa kusoma hii badala ya kunisikia nikisema, mabadiliko hufika kwenye kikasha chako kila asubuhi — bure kwenye the daily diff dot dev, kiungo hapa chini. Kwa hivyo, uamuzi wa leo: SHIP IT. Kernel inasema ndiyo, Buzzard anasema ndiyo, hesabu haikubadilika, lakini njia tunayochunguza hesabu imebadilika. Hayo ndiyo mabadiliko ya leo. Mimi ni Niko kutoka Axrisi.

5:09 Unganisha kwa uwajibikaji.

Vyanzo

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com