ક્લાઉડે 11 દિવસમાં ફર્મેટ સાબિત કર્યું. ચુકાદો: SHIP IT.

આ વીડિયોમાં શું આવરી લેવામાં આવ્યું છે

• ક્લાઉડ લીન 4 માં ફર્મેટના છેલ્લા પ્રમેયને ઔપચારિક બનાવે છે
• ક્રોમિયમ સેન્ડબોક્સ RCE (CVE-2026-85046), વાસ્તવિકતામાં શોષણ કરાયેલ, $1,000 ઇનામ
• શિન જિન-સીઓ બે પથ્થરના હૅન્ડિકેપ સાથે કાટાગોને હરાવે છે

અનુવાદિત ટ્રાન્સક્રિપ્ટ

મૂળ અંગ્રેજી કથામાંથી અનુવાદિત. ઉપલબ્ધ ઑડિઓ અને કૅપ્શન્સ YouTube દ્વારા નિયંત્રિત થાય છે.

0:00 ફર્મેટે કહ્યું કે તેની અદ્ભુત સાબિતી માર્જિનમાં સમાશે નહીં, અને આજે એન્થ્રોપિકે માર્જિન પ્રકાશિત કર્યું: તેર મિલિયન લીન લાઇન્સ, મેથલિબના કદથી પાંચ ગણું, એક પ્રમેય સાબિત કરે છે જે દરેક ગણિતશાસ્ત્રી પહેલાથી જ માનતા હતા. જ્યારે એન્થ્રોપિકે પોસ્ટ કર્યું ત્યારે ટ્બિલિસીમાં દસથી અગિયાર વાગ્યા હતા, તો સ્વાભાવિક રીતે હું જાગતો હતો. ગઈકાલે ગૂગલે બાર સુરક્ષા સુધારાઓ સાથે ક્રોમ 152 મોકલ્યું, તેમાંથી એક V8 બગ વાસ્તવિકતામાં પહેલાથી જ શોષણ કરાયેલ, અને રિપોર્ટરને હજાર ડોલર ચૂકવ્યા, જે સેડાન કરતા ઓછું છે જેના પર આપણે પછીથી આવીશું.

0:26 ગઈકાલે પણ, મુલવાડે કહ્યું કે તે 2 નવેમ્બરના રોજ તેની જાહેર એન્ક્રિપ્ટેડ DNS બંધ કરી રહ્યું છે અને તેના બદલે ક્વાડ9 ને તે કરવા માટે ચૂકવણી કરી રહ્યું છે, અને આજે સવારે રસ્ટ રિએક્ટ કમ્પાઇલર વિટેમાં નેટિવ બન્યું, જ્યારે હેકર ન્યૂઝે IBM બોબ શોધ્યું, એક AI કોડિંગ એજન્ટ. પછી ક્લાઉડે ફર્મેટના છેલ્લા પ્રમેયને ઔપચારિક બનાવ્યું, અને તે જ પહેલા પાના પર એક કોરિયન ગ્રાન્ડમાસ્ટરે પૃથ્વી પરના સૌથી મજબૂત ગો એન્જિનને હરાવ્યું, તો આજે માનવતાએ બે માંથી એક મેળવ્યું. આ વિડિયોમાં: ક્લાઉડે ખરેખર શું સાબિત કર્યું, તેનો કેટલો ખર્ચ થયો,

0:52 શા માટે જે ગણિતશાસ્ત્રીએ પોતાની કારકિર્દી આના પર વિતાવી તે કહે છે કે તે કશું જ બદલતું નથી અને તેમ છતાં ઉત્સાહિત છે, અને કેવી રીતે એક માનવીએ ગો માં મશીનને હરાવ્યું. શુક્રવાર, 4 સપ્ટેમ્બર છે, અને આ છે ધ ડેઇલી ડિફ. ફર્મેટનો છેલ્લો પ્રમેય: કોઈ સકારાત્મક પૂર્ણાંક a, b, c n 2 થી ઉપરના કોઈપણ n માટે a ની n ઘાત વત્તા b ની n ઘાત c ની n ઘાત બરાબર થાય છે તેને સંતોષતા નથી. ફર્મેટે લગભગ 1637 માં એક માર્જિનમાં તે લખ્યું અને પોતાનું કાર્ય દર્શાવ્યા વિના મૃત્યુ પામ્યા, તેને પ્રથમ ડેવલપર બનાવ્યા જેણે મારી મશીન પર કામ કરે છે એમ કહીને ટિકિટ બંધ કરી. 1908 માં 100,000 સોનાના માર્ક્સનું ઇનામ તેના પ્રથમ વર્ષમાં 621 ખોટી

1:25 સાબિતીઓને આકર્ષિત કર્યું, અને એન્ડ્રુ વાઇલ્સે આખરે 1995 માં તે મેળવ્યું, 129 પાનામાં જેને રેફરીઓને ચકાસવામાં મહિનાઓ લાગ્યા. ઔપચારિક બનાવવાનો અર્થ છે કે તે સાબિતીને ફરીથી લખવી જેથી લીન, એક પ્રૂફ સહાયક, દરેક પગલાને યાંત્રિક રીતે ચકાસી શકે, અને ઇમ્પિરિયલ ખાતેના કેવિન બઝાર્ડે 2024 થી બરાબર તે જ કરવા માટે માનવ પ્રયાસનું નેતૃત્વ કર્યું છે; એકલા બ્લુપ્રિન્ટ 86 પાનાની છે. એન્થ્રોપિક સંશોધક ટિયાનયી પેંગે તેના બદલે ડઝનેક ક્લાઉડ એજન્ટોને તેના પર નિર્દેશિત કર્યા પ્રોવ2મી નામની એક પ્લેટફોર્મ પર જે પ્રમેય નિવેદનોનો DAG રાખે છે જેથી એજન્ટોને ખબર પડે કે આગળ શું સાબિત કરવું, કારણ કે તેના વિના પ્રથમ

2:00 ટોળાઓ કોણ શું સાબિત કરી રહ્યું છે તેનો ટ્રેક ગુમાવી દીધો, જે ત્યારે થાય છે જ્યારે તમારું ઓર્કેસ્ટ્રેશન લેયર માર્કેટિંગ બજેટ સાથે રેગક્સ હોય. અગિયાર દિવસ પછી રૂટ નોડમાં PROVED લખ્યું: તેર મિલિયન લીન લાઇન્સ, 29,500 મધ્યવર્તી પ્રમેય, લગભગ છ અબજ આઉટપુટ ટોકન્સ એક આંતરિક મોડેલમાંથી જે ક્લાઉડ ફેબલ 5.1 જેવું જ છે. બિલ્ડ નિષ્ફળ જાય છે સિવાય કે સાબિતી બરાબર લીનના ત્રણ પ્રમાણભૂત સિદ્ધાંતો પર આધારિત હોય: ના સોરી, કોઈ નેટિવ ડિસાઇડ નહીં, કોઈ છેતરપિંડી નહીં. તેને તપાસવું પણ સસ્તું નથી: એક

2:29 શરૂઆતથી બિલ્ડ કરવામાં સાડા પાંચ કલાક લાગ્યા 96 કોર અને 153 ગીગાબાઇટ્સ RAM પર, અને પ્રમેયના નામો મશીન-જનરેટ થયેલા છે, તેથી રેપો પોતાને વાંચવાને બદલે ચકાસવા માટે લખાયેલું વર્ણવે છે, જે રીતે હું એન્ટરપ્રાઇઝ જાવાને પણ વર્ણવીશ. હવે વિરોધાભાસ. એન્થ્રોપિકની પોસ્ટ કહે છે કે લીન નિઃશંકપણે શુદ્ધતા દર્શાવે છે. કેવિન બઝાર્ડ, જે માણસને તેનાથી હરાવવામાં આવ્યો હતો, તેણે એન્થ્રોપિકે તેને ઉધાર આપેલ 500-ગીગાબાઇટ મશીન પર રેપો કમ્પાઇલ કર્યું, ખાતરી કરી કે તે તપાસે છે, અને પછી લખ્યું,

2:56 અવતરણ, ગાણિતીય રીતે આ કાર્ય આપણને આવશ્યકપણે કશું જ કહેતું નથી. તે પહેલેથી જ 99.9 ટકા ખાતરી હતી કે પ્રમેય સાચો હતો, અને સાબિતી કોઈ નવું ગણિત ઉમેરતી નથી; તે શું દર્શાવે છે કે સ્વતઃઔપચારિકકરણ હવે શું કરી શકે છે, અને તે ભાગ વિશે તે ખરેખર ઉત્સાહિત છે. તેને પાંચ વર્ષમાં દસ લાખ પાઉન્ડ આપવામાં આવ્યા હતા; એન્થ્રોપિકે અગિયાર દિવસ લીધા, અને એક ટિપ્પણી કરનારના નેપકિન ગણિત મુજબ સૂચિ કિંમત પર છ અબજ આઉટપુટ ટોકન્સનો અંદાજ છે આશરે 300,000 ડોલર, તેથી મશીન સસ્તું હતું, સિવાય કે તમે મશીનને તાલીમ આપવાનું ગણો, જે કોઈ કરતું નથી.

3:24 શ્રેષ્ઠ વિગત: ઇમેઇલ તેને વેલ્સમાં એક સંગીત મહોત્સવમાં હતો ત્યારે મળ્યો, જ્યાં 4G નો એક જ બાર હતો, અને તે એક અજાણ્યા નામ તરફથી હતો, તેથી તેણે તેને એક બકવાસ માની લીધો અને એક અઠવાડિયા પછી વાંચ્યો, જે કોઈપણ વિષયની લાઇન માટે યોગ્ય પ્રતિક્રિયા છે જેમાં "એન્ડ-ટુ-એન્ડ ફોર્મલાઇઝેશન" હોય. દરમિયાન, માણસોએ એક વાપસી કરી. ગોના વિશ્વના નંબર વન, શિન જિન-સેઓ, કાટાગોને હરાવ્યા, સૌથી શક્તિશાળી ઓપન-સોર્સ ગો એન્જિન, સિઓલમાં બે રમતોથી એકમાં બે-પથ્થરના હેન્ડિકેપ સાથે, જે લગભગ એક ટોચના પ્રોફેશનલ અને એક રૂકી પ્રોફેશનલ વચ્ચેનું અંતર છે.

3:50 નિર્ણાયક 221 ચાલમાં 11.5-પોઇન્ટની જીત હતી, જેમાં તેણે મધ્ય-રમતથી 99 ટકા જીતની સંભાવના જાળવી રાખી, અને તેણે 250 મિલિયન વોન, લગભગ 170,000 ડોલર, વત્તા એક જેનિસિસ G90 ઘરે લઈ ગયા, તેથી સુપરહ્યુમન AI ને હરાવવા માટેનું ઇનામ Google ના ક્રોમ સેન્ડબોક્સ એસ્કેપ માટેના ઇનામ કરતાં 170 ગણું છે. તેની સમજૂતી: શરૂઆતમાં તેણે AI ની ચાલ કોપી કરી અને હારી ગયો; તેણે પોતાની શૈલીમાં બોર્ડ બનાવીને જીત્યો, જે AI વિશેની સૌથી ઉપયોગી સલાહ છે જે મેં આ આખા વર્ષમાં સાંભળી છે, અને તે એક બોર્ડ ગેમમાંથી આવી છે. ડિફમાં વધુ બે લીટીઓ.

4:22 oxc માંથી Rust React Compiler હવે Vite માં એક ફ્લેગ પાછળ મૂળભૂત રીતે ઉપલબ્ધ છે; એક 1,036-ફાઇલનો કોડબેઝ કમ્પાઇલ સ્ટેપમાં 14.3 સેકન્ડથી ઘટીને 0.81 થયો, મોટે ભાગે package.json માંથી Babel ને ડિલીટ કરીને, જે મારી સ્કિનકેર રૂટિન પણ છે. અને IBM એ બોબ લોન્ચ કર્યો, એક AI કોડિંગ પાર્ટનર જે તમને 'હાય, હું બોબ છું' કહીને આવકારે છે, સબએજન્ટ્સ બનાવે છે, મેઇનફ્રેમ કોડને આધુનિક બનાવે છે, અને બોબાલિટિક્સ નામનું એક એનાલિટિક્સ પ્રોડક્ટ શીપ કરે છે, તેથી ક્યાંક એક બેંક ખૂબ જ ઉત્સાહિત છે અને કોઈએ લાયસન્સ વાંચ્યું નથી.

4:51 એક શુક્રવાર માટે આ ઘણો માર્જિન છે; જો તમે મને આ કહેતા સાંભળવાને બદલે આ વાંચવાનું પસંદ કરો છો, તો ડિફ દરરોજ સવારે તમારા ઇનબોક્સમાં આવે છે — The Daily Diff dot dev પર મફત, લિંક નીચે આપેલી છે. તો, આજનો ચુકાદો: SHIP IT. કર્નલ હા પાડે છે, બઝાર્ડ હા પાડે છે, ગણિત બદલાયું નથી, પરંતુ આપણે ગણિત કેવી રીતે તપાસીએ છીએ તે હમણાં જ બદલાઈ ગયું. આજનો diff આ છે. હું Axrisi માંથી Niko છું.

5:09 જવાબદારીપૂર્વક મર્જ કરો.

સ્ત્રોતો

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