கிளாட் 11 நாட்களில் பெர்மாட்டின் தேற்றத்தை நிரூபித்தது. தீர்ப்பு: SHIP IT.
கிளாட் 11 நாட்கள் மற்றும் சுமார் 6 பில்லியன் டோக்கன்களை செலவிட்டு, பெர்மாட்டின் கடைசி தேற்றத்தின் 13 மில்லியன் வரிகள் கொண்ட லீன் நிரூபணத்தை எழுதியது — இதுவே முதல் கணினி சரிபார்க்கப்பட்ட முடிவாகும் — அதே சமயம், 2024 முதல் இதை முறைப்படுத்தி வரும் கணிதவியலாளர் இது "கணித ரீதியாக எங்களுக்கு எதையும் சொல்லவில்லை" என்று கூறி, ஆனாலும் உற்சாகமாக உள்ளார்.
கிளாட் 11 நாட்கள் மற்றும் சுமார் 6 பில்லியன் டோக்கன்களை செலவிட்டு, பெர்மாட்டின் கடைசி தேற்றத்தின் 13 மில்லியன் வரிகள் கொண்ட லீன் நிரூபணத்தை எழுதியது — இதுவே முதல் கணினி சரிபார்க்கப்பட்ட முடிவாகும் — அதே சமயம், 2024 முதல் இதை முறைப்படுத்தி வரும் கணிதவியலாளர் இது "கணித ரீதியாக எங்களுக்கு எதையும் சொல்லவில்லை" என்று கூறி, ஆனாலும் உற்சாகமாக உள்ளார். அதே நாளில்: உலகின் நம்பர் 1 வீரர் ஷின் ஜின்-சியோ, இரண்டு கற்கள் குறைபாட்டுடன் கடாகோவை 2–1 என்ற கணக்கில் வென்றார். தீர்ப்பு: SHIP IT.
இந்த வீடியோ எதைப் பற்றி விவாதிக்கிறது
- கிளாட் பெர்மாட்டின் கடைசி தேற்றத்தை லீன் 4 இல் முறைப்படுத்துகிறது
- குரோமியம் சாண்ட்பாக்ஸ் RCE (CVE-2026-85046), நடைமுறையில் பயன்படுத்தப்பட்டது, $1,000 வெகுமதி
- ஷின் ஜின்-சியோ இரண்டு கற்கள் குறைபாட்டுடன் கடாகோவை தோற்கடித்தார்
மொழிபெயர்க்கப்பட்ட டிரான்ஸ்கிரிப்ட்
அசல் ஆங்கில விளக்கத்திலிருந்து மொழிபெயர்க்கப்பட்டது. கிடைக்கும் ஆடியோ மற்றும் தலைப்புகள் YouTube ஆல் கட்டுப்படுத்தப்படுகின்றன.
0:00 பெர்மாட் தனது அற்புதமான நிரூபணம் ஓரத்தில் பொருந்தாது என்று கூறினார், இன்று ஆந்த்ரோபிக் அந்த ஓரம்: பதின்மூன்று மில்லியன் வரிகள் கொண்ட லீன் நிரூபணத்தை வெளியிட்டது, இது மேத்லிப்பின் அளவை விட ஐந்து மடங்கு பெரியது, ஒவ்வொரு கணிதவியலாளரும் ஏற்கனவே நம்பிய ஒரு தேற்றத்தை நிரூபிக்கிறது. ஆந்த்ரோபிக் வெளியிட்டபோது திபிலீசியில் இரவு பத்து அல்லது பதினொரு மணி, அதனால் நான் இயல்பாகவே விழித்திருந்தேன். நேற்று கூகிள் க்ரோம் 152 ஐ பன்னிரண்டு பாதுகாப்பு திருத்தங்களுடன் வெளியிட்டது, அவற்றில் ஒன்று V8 பிழை ஏற்கனவே நடைமுறையில் பயன்படுத்தப்பட்டது, மேலும் புகாரளித்தவருக்கு ஒரு ஆயிரம் டாலர்கள் கொடுத்தது, இது நாம் பின்னர் பார்க்கும் செடானை விட குறைவு.
0:26 நேற்று, முல்வாட் தனது பொது மறைகுறியாக்கப்பட்ட DNS ஐ நவம்பர் 2 அன்று மூடப்போவதாகவும், அதற்கு பதிலாக குவாட்9 ஐ பயன்படுத்த உள்ளதாகவும் கூறியது, மேலும் இன்று காலை ரஸ்ட் ரியாக்ட் கம்பைலர் விட்டேவில் நேட்டிவ் ஆக மாறியது, அதே நேரத்தில் ஹேக்கர் நியூஸ் IBM பாபை ஒரு AI கோடிங் ஏஜென்ட் என்று கண்டுபிடித்தது. பின்னர் கிளாட் பெர்மாட்டின் கடைசி தேற்றத்தை முறைப்படுத்தியது, அதே முதல் பக்கத்தில் ஒரு கொரிய கிராண்ட்மாஸ்டர் பூமியில் உள்ள வலிமையான கோ எஞ்சினை தோற்கடித்தார், அதனால் இன்று மனிதகுலம் இரண்டில் ஒன்று என்ற கணக்கில் வென்றது. இந்த வீடியோவில்: கிளாட் உண்மையில் என்ன நிரூபித்தது, அதற்கு என்ன செலவானது,
0:52 இந்த விஷயத்தில் தனது வாழ்க்கையை செலவிட்ட கணிதவியலாளர் ஏன் இது எதையும் மாற்றவில்லை என்று கூறி ஆனாலும் உற்சாகமாக உள்ளார், மேலும் கோ விளையாட்டில் ஒரு மனிதன் இயந்திரத்தை எப்படி வென்றான். இன்று செப்டம்பர் 4, வெள்ளிக்கிழமை, இது The Daily Diff. பெர்மாட்டின் கடைசி தேற்றம்: எந்த நேர்மறை எண்கள் a, b, c n ஐ விட பெரிய எந்த n க்கும் a அடுக்கு n கூட்டல் b அடுக்கு n சமம் c அடுக்கு n ஐ பூர்த்தி செய்யாது. பெர்மாட் சுமார் 1637 இல் ஒரு ஓரத்தில் அதை கிறுக்கினார் மற்றும் தனது வேலையைக் காட்டாமல் இறந்தார், இது 'works on my machine' என்று கூறி ஒரு டிக்கெட்டை மூடிய முதல் டெவலப்பராக இவரை ஆக்கியது. 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 உடன், அதனால் அவர் அதை ஒரு பைத்தியக்காரத்தனமாகத் தள்ளிவிட்டார், ஒரு வாரம் கழித்து அதைப் படித்தார், இது எந்தவொரு தலைப்புக்கும் சரியான பதில் முழுமையான முறையான அமைப்பைக் கொண்டுள்ளது. இதற்கிடையில், மனிதர்கள் ஒரு புள்ளியைப் பெற்றனர். Go-வில் உலகின் நம்பர் ஒன் ஷின் ஜின்-சியோ, KataGo-வை தோற்கடித்தார், மிகவும் சக்திவாய்ந்த ஓபன் சோர்ஸ் Go எஞ்சினை, சியோலில் இரண்டு ஆட்டங்களுக்கு ஒன்று என்ற விகிதத்தில், இரண்டு கற்கள் ஹேண்டிகேப் உடன், இது ஒரு முன்னணி நிபுணருக்கும் ஒரு புதிய நிபுணருக்கும் இடையிலான இடைவெளி.
3:50 முடிவு 221 நகர்வுகளில் 11.5-புள்ளி வெற்றி, இது ஒரு நடு ஆட்டத்திலிருந்து 99 சதவீத வெற்றி நிகழ்தகவைக் கொண்டிருந்தது, அவர் 250 மில்லியன் வென்றார், சுமார் 170,000 டாலர்கள், மேலும் ஒரு Genesis G90, எனவே ஒரு மனிதநேயமற்ற AI-ஐ தோற்கடிப்பதற்கான வெகுமதி Google-ன் Chrome சாண்ட்பாக்ஸ் தப்பிப்பதற்கான வெகுமதியை விட 170 மடங்கு அதிகம். அவரது விளக்கம்: ஆரம்பத்தில் அவர் AI நகர்வுகளை நகலெடுத்து தோற்றார்; அவர் வென்றது தனது சொந்த பாணியில் பலகையை உருவாக்குவதன் மூலம், இது AI பற்றி நான் கேட்டதில் மிகவும் பயனுள்ள ஆலோசனை இந்த ஆண்டு முழுவதும் கேட்டேன், அது ஒரு பலகை விளையாட்டிலிருந்து வந்தது. மாறுதலில் மேலும் இரண்டு வரிகள்.
4:22 oxc-ன் Rust React Compiler இப்போது ஒரு கொடிக்குப் பின்னால் Vite-ல் நேட்டிவ் ஆக உள்ளது; ஒரு 1,036-கோப்பு குறியீடு 14.3 வினாடிகளிலிருந்து 0.81 ஆக மாறியது தொகுக்கும் படிநிலையில், பெரும்பாலும் Babel-ஐ நீக்குவதன் மூலம் package.json-லிருந்து, இது எனது தோல் பராமரிப்பு வழக்கமும் கூட. மேலும் IBM Bob-ஐ அறிமுகப்படுத்தியது, இது ஒரு AI குறியீட்டு பங்குதாரர், அது உங்களை ஹாய், நான் Bob, துணை முகவர்களை உருவாக்குகிறது, மெயின்பிரேம் குறியீட்டை நவீனமயமாக்குகிறது, மற்றும் Bobalytics எனப்படும் ஒரு பகுப்பாய்வு தயாரிப்பை அனுப்புகிறது, அதனால் எங்கோ ஒரு வங்கி மிகவும் உற்சாகமாக உள்ளது, மேலும் யாரும் உரிமத்தை படிக்கவில்லை.
4:51 ஒரு வெள்ளிக்கிழமைக்கு இது ஒரு பெரிய லாபம்; நான் சொல்வதை கேட்பதை விட இதை நீங்கள் படிக்க விரும்பினால், மாறுதல் ஒவ்வொரு காலையிலும் உங்கள் இன்பாக்ஸில் வரும் — daily diff dot-ல் இலவசமாக dev, இணைப்பு கீழே. ஆகவே, இன்றைய தீர்ப்பு: SHIP IT. கர்னல் ஆம் என்கிறது, Buzzard ஆம் என்கிறது, கணிதம் மாறவில்லை, ஆனால் நாம் கணிதத்தை சரிபார்க்கும் முறை இப்போது மாறிவிட்டது. இதுதான் இன்றைய வேறுபாடு. நான் Axrisi-யிலிருந்து Niko.
5:09 பொறுப்புடன் ஒன்றிணைக்கவும்.
ஆதாரங்கள்
- Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
- The proof (Lean 4, Apache-2.0)github.com
- Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
- HN threadnews.ycombinator.com
- KED Global — Shin defeats KataGowww.kedglobal.com
- HNnews.ycombinator.com
- Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
- NVDnvd.nist.gov
- Mullvad — shutting down public encrypted DNSmullvad.net
- Rust React Compiler native in Viteblog.master.dev
- IBM Bobbob.ibm.com



