முப்பரிமாண கிஸ் அனுமானத்தை நிரூபிக்க சீன செயற்கை நுண்ணறிவு மாதிரி உதவி; கணிதத்தை லீன் சரிபார்த்தது

1995ஆம் ஆண்டின் கணிதப் பிரச்சினை புதிய மைல்கல்லை எட்டியது

1995ஆம் ஆண்டு முன்வைக்கப்பட்ட கணித அனுமானத்துக்கு, சிக்கலெண் பரிமாணம் மூன்றை உள்ளடக்கிய நிரூபணம் கிடைத்துள்ளது. கணிதவியலாளர்களுக்கும் ஷாங்காய் செயற்கை நுண்ணறிவு ஆய்வகத்தின் Intern-S2 மாதிரிக்கும் இடையிலான கூட்டுப்பணியைத் தொடர்ந்து இது நிகழ்ந்தது. பின்னர், பீக்கிங் பல்கலைக்கழகக் குழு ஆய்வுக் கட்டுரையின் நான்கு முக்கிய தேற்றங்களையும் கணிதப் பகுத்தறிவைச் சரிபார்க்க வடிவமைக்கப்பட்ட கணினி அமைப்பான Lean மூலம் சரிபார்க்கப்பட்ட நிரூபணங்களாக மாற்றியது.

இந்தச் சாதனையை ஷாங்காய் செயற்கை நுண்ணறிவு ஆய்வகம் 2026 அக்டோபர் 15 அன்று அறிவித்தது. கிரேட் பே பல்கலைக்கழகப் பேராசிரியரும் ஆய்வகத்தின் வருகைதரு ஆய்வாளருமான டிஷெங் சூ தலைமையிலான குழுவுக்கு அது பாராட்டு தெரிவித்தது. ‘கோடிமானம்-ஒன்று ஹோலோமார்பிக் அனோசோவ் வேறுபகரணங்கள்’ என்ற ஆய்வுக் கட்டுரையில், ஸ்வீடனின் KTH ராயல் தொழில்நுட்பக் கழகத்தைச் சேர்ந்த ஜியேசோங் ஜாங் மட்டுமே ஆசிரியராகப் பட்டியலிடப்பட்டுள்ளார்.

இந்த முடிவு, பிரெஞ்சு கணிதவியலாளர் எத்தியென் கிஸ் முன்வைத்த அனுமானத்தின் கோடிமானம்-ஒன்று நிலையைத் தீர்க்கிறது; இதில் சிக்கலெண் பரிமாணம் மூன்றாக இருக்கும் நிலையும் அடங்கும். இது இயக்கத்துக்கும் வடிவத்துக்கும் இடையிலான வியப்பூட்டும் தொடர்பைப் பற்றியது: ஒரு குறிப்பிட்ட வகையான குழப்பமான இயக்கத்தை ஆதரிக்கும் வெளி, தானும் மிக ஒழுங்கமைந்த கணிதக் கட்டமைப்பைக் கொண்டிருக்க வேண்டுமா என்பதே கேள்வி.

ஆய்வாளர்களுடனான தொடர்ச்சியான உரையாடல்களின் மூலம் கருத்துகளையும் வாதங்களையும் உருவாக்க Intern-S2 உதவியது. செயற்கை நுண்ணறிவைப் பயன்படுத்தியது குறித்த தனது அறிவிப்பில், கணிதம் அனைத்தையும் தாமாகவே சரிபார்த்ததாக ஜாங் தெரிவித்துள்ளார். இந்தக் கூட்டுப்பணி, இயந்திரம் வழியிலான ஆய்வு, மனிதத் தீர்மானம், தனியான முறையான சரிபார்ப்பு ஆகியவற்றை ஒருங்கிணைத்தது.

இந்த நிலைமையிலான கணிதப் பிரச்சினையைத் தீர்க்க சீன செயற்கை நுண்ணறிவு மாதிரி ஒன்று உதவியது இதுவே முதன்முறை என ஆய்வகம் இந்தச் சாதனையை விவரிக்கிறது. இதன் நேரடியான விளைவு ஒரு வகைப்பாட்டுத் தேற்றம்; அதனுடன் பொதுவெளியில் கிடைக்கும் முன்வெளியீடும், பொதுவெளியில் வெளியிடப்பட்ட முறையாக்கக் குறியீடும் உள்ளன.

இயக்கத்தையும் வடிவத்தையும் பற்றி நிரூபணம் கூறுவது என்ன?

கிஸின் அனுமானம் சிக்கலெண் இயக்கவியலைச் சார்ந்தது. சிக்கலெண்களின் விதிகளுக்கு ஏற்ப ஆயத்தொலைவுகள் மாறும்போது, கணித அமைப்புகள் எவ்வாறு மாறுகின்றன என்பதை இந்தத் துறை ஆய்வு செய்கிறது. ஒரு சிக்கலெண்ணில் இரண்டு மெய்யெண் கூறுகள் இருப்பதால், சிக்கலெண் பரிமாணம் மூன்று என்பது உள்ளூரில் ஆறு மெய்ப் பரிமாணங்களுக்குச் சமம். இது ஓர் அறைக்குள் நகரும் சாதாரண பொருளைவிட மிகவும் அருவமான சூழலாகும்.

அனோசோவ் அமைப்பில் நீட்டித்தலும் சுருக்குதலும் துல்லியமான முறையில் இணைந்திருக்கும். மீண்டும் மீண்டும் இயக்கப்படும்போது, சில திசைகள் சுருங்க, மற்றவை விரிவடையும். ஒவ்வொரு படியையும் வழிநடத்தும் விதி துல்லியமானதாக இருந்தாலும், அருகருகே தொடங்கும் புள்ளிகள் விரைவாகப் பிரிந்து குழப்பமான நடத்தையை உருவாக்கலாம்.

ஒரு வடிவத்தை மீண்டும் மீண்டும் நீட்டி மடிக்கும் செயல்முறையை இதற்கான எளிய சித்திரமாகக் கொள்ளலாம். இங்கு ஆய்வு செய்யப்படும் கணித அமைப்பு இதைவிடக் கட்டுப்பாடுகள் அதிகமுடையது: நீட்டித்தலும் சுருங்குதலும் ஒரே சீரான நிபந்தனைகளைப் பூர்த்தி செய்ய வேண்டும்; மேலும், அதன் இயக்கம் சிக்கலெண் ஆயத்தொலைவுகள் வழங்கும் கட்டமைப்பைப் பாதுகாக்க வேண்டும்.

குறுகிய சிக்கலெண் பன்மடங்குகளில் இத்தகைய அமைப்புகள் வழக்கமான இயற்கணித விளக்கத்தைக் கொண்டிருக்கும் என்று கிஸ் முன்மொழிந்தார். ஒரு பன்மடங்கு என்பது, அதன் முழு வடிவம் சிக்கலானதாக இருந்தாலும், சிறிய சுற்றுப்பகுதியில் எளிமையாகத் தோன்றும் வெளி. இச்சூழலில், அந்த வெளி முடிவின்றி விரிவடையாமல் இருப்பதைச் சுருக்கத்தன்மை என்ற கணித நிபந்தனை உறுதிப்படுத்துகிறது.

குறுகிய சிக்கலெண் பன்மடங்கு ஒன்றில் உள்ள ஒவ்வொரு கோடிமானம்-ஒன்று ஹோலோமார்பிக் அனோசோவ் வேறுபகரணமும், ஒரு சிக்கலெண் டோரஸின் மிகைபரவல் தன்னுருமாற்றத்துடன் இருமுறையும் ஹோலோமார்பிக்காக இணையாக இருக்கும் என ஜாங்கின் தேற்றம் கூறுகிறது. எளிமையாகச் சொன்னால், சிக்கலெண் கட்டமைப்பைப் பாதுகாக்கும் தலைகீழாக்கக்கூடிய ஆயத்தொலைவு மாற்றம், அந்த இயக்கத்தை மிகவும் ஒழுங்கான வெளியில் நடைபெறும் வழக்கமான இயற்கணித மாற்றமாக மாற்றுகிறது.

மீண்டும் மீண்டும் அமைந்துள்ள வலைப்பின்னலின் கூறுகளால் வேறுபடும் சிக்கலெண் வெளியிலுள்ள புள்ளிகளை ஒன்றாக அடையாளம் காண்பதன் மூலம் சிக்கலெண் டோரஸை உருவாக்கலாம். சிக்கலான இயக்கவியல் இந்த ஒழுங்கான வடிவியல் விளக்கத்தை கட்டாயமாக்குகிறது என்பதே இந்த முக்கியச் சாதனையாகும்.

துல்லியமான வரம்பு ஏன் முக்கியம்?

இந்த ஆய்வுக் கட்டுரை கோடிமானம்-ஒன்று சூழலைக் கையாள்கிறது. இத்தகைய அமைப்புகளில், சுருங்கும் அல்லது விரிவடையும் பகுதிகளில் ஒன்று சிக்கலெண் பரிமாணம் ஒன்றைக் கொண்டிருக்கும். இந்த வரம்புக்குட்பட்ட குடும்பத்தைப் பொதுவாகத் தேற்றம் உள்ளடக்குகிறது; மேலும், சிக்கலெண் பரிமாணம் மூன்றில் அனுமானத்திற்குத் தீர்வு அளிக்கிறது.

கிஸின் விரிவான அனுமானம், பலவகையான சிக்கலெண் பன்மடங்குகளில் உள்ள ஹோலோமார்பிக் அனோசோவ் அமைப்புகளைக் குறித்தது. சிக்கலெண் இன்ஃப்ரா-நில்மடங்கு எனப்படும் வெளிகளில் உள்ள வழக்கமான இயற்கணித மாதிரிகள் மூலம் அவற்றை விவரித்தது. ஜாங்கின் முடிவு, ஆய்வு செய்யப்பட்ட நிலைக்கு மிகவும் கட்டுப்பாடான பதிலை வழங்குகிறது: ஒரு சிக்கலெண் டோரஸும் ஒரு மிகைபரவல் தன்னுருமாற்றமும்.

இந்த நிலையை ஆய்வு செய்யும் கணிதவியலாளர்களுக்கு, தெரியாத வெளி மற்றும் இயக்கத்தைக் கண்டறிவதிலிருந்து வழக்கமான மாதிரியை ஆய்வு செய்வதற்கு இந்தத் தேற்றம் சிக்கலை மாற்றுகிறது. சிக்கலெண் வடிவியலைப் பாதுகாத்தபடி, ஆயத்தொலைவு மாற்றம் அசல் அமைப்பை அந்த மாதிரியுடன் இணைக்கிறது.

இந்தப் பிரச்சினையைச் சூ பல ஆண்டுகளாக ஆய்வு செய்து வந்தார். முன்னதாக, ஃபீல்ட்ஸ் பதக்கம் பெற்ற ஆர்துர் அவிலா என்ற தனது முன்னாள் ஆலோசகருடன் இணைந்து பரிமாணம் மூன்று உள்ள நிலையை ஆய்வு செய்தார். பின்னர், சூவும் ஜாங்கும் தொடர்புடைய பகுதி முடிவுகளைப் பெற்று, அவை Journal of the European Mathematical Society இதழில் வெளியாயின. அதே கணிதக் கேள்வியில் நீண்டகாலமாகச் செலுத்திய கவனத்தின் தொடர்ச்சியே இந்தப் புதிய ஆய்வு.

ஒலிம்பியாட் தேர்விலிருந்து ஆய்வுக் கூட்டுப்பணி வரை

2025 சீனக் கணித ஒலிம்பியாடில் Intern-S1 பெற்ற முந்தைய முடிவைத் தொடர்ந்து Intern-S2-ன் பங்கு அமைந்தது. அந்த ஆண்டில், இடைநிலைப் பள்ளிக் கணிதப் போட்டிகளுக்குப் பொறுப்பான சீனக் கணிதச் சங்கக் குழு செயற்கை நுண்ணறிவுத் தேர்வை அறிமுகப்படுத்தியது. மனிதப் போட்டியாளர்களுக்கு வழங்கப்பட்ட அதே காலவரம்புக்குள் சிக்கல்களைத் தீர்க்குமாறு மூன்று சீன மாதிரிகளுக்கு அழைப்பு விடுக்கப்பட்டது.

அதே மதிப்பீட்டு அளவுகோலின்படி Intern-S1 102 புள்ளிகள் பெற்று, பங்கேற்ற மூன்று மாதிரிகளில் முதலிடம் பிடித்தது. தங்கப் பதக்கத்துக்கான வரம்பு 78 புள்ளிகளாக இருந்தது. அதைவிட 24 புள்ளிகள் அதிகம், அதாவது சுமார் 31 சதவீதம் கூடுதலாக அது பெற்றது.

ஆய்வு கணிதத்தில் இந்த மாதிரிக் குடும்பத்தைப் பயன்படுத்துவதற்கான சாத்தியத்தைச் சூ கண்டார். தீர்க்கப்படாத கேள்விகளுக்கு நகர்வதற்குப் போட்டிப் பிரச்சினைகளைத் தாண்டிச் செல்ல ஷாங்காய் செயற்கை நுண்ணறிவு ஆய்வகம் விரும்பியது. 2026ஆம் ஆண்டின் தொடக்கத்தில் அவர்களின் கூட்டுப்பணி தொடங்கியது. மாதிரியின் பணிகளையும் ஆய்வாளர்களுடனான உரையாடல்களையும் ஒழுங்குபடுத்தும் ‘ஹார்னஸ்’ என விவரிக்கப்பட்ட மென்பொருள் அமைப்பை உருவாக்குவதும் இதில் அடங்கியது.

முக்கிய கட்டங்கள்:

• 1995: எத்தியென் கிஸ் அனுமானத்தை முன்வைத்தார்.
• 2025: சீனக் கணித ஒலிம்பியாட் செயற்கை நுண்ணறிவுத் தேர்வில் Intern-S1 102 புள்ளிகள் பெற்றது.
• 2026ஆம் ஆண்டின் தொடக்கம்: சூவும் ஷாங்காய் செயற்கை நுண்ணறிவு ஆய்வகமும் மாதிரிப் பயிற்சிக் கூட்டுப்பணியைத் தொடங்கின.
• 2026 மார்ச்: சூ ஆய்வகத்தின் வருகைதரு ஆய்வாளரானார்.
• 2026 ஆகஸ்ட்: உள்நாட்டில் உருவாக்கப்பட்ட Intern-S2 பதிப்பும் அதற்குத் துணையான அமைப்பும் தீவிரக் கணித ஆய்வுக்குப் பயன்படுத்தப்பட்ட நிலையை எட்டின.
• செப்டம்பர் 29: ஜாங்கின் ஆய்வுக் கட்டுரை arXiv-இல் வெளியிடப்பட்டது; அதைத் தொடர்ந்து அக்டோபர் 13 அன்று திருத்தப்பட்ட பதிப்பு வெளியானது.
• 2026 அக்டோபர் 15: சாதனை பொதுவெளியில் அறிவிக்கப்பட்டது.

கணிதவியலாளர்கள் செயற்கை நுண்ணறிவுக்கு வழிகாட்டிய விதம்

இந்தப் பிரச்சினையை Intern-S2 முதன்முறையாக ஆராய்ந்தபோது, சுமார் 400 பக்கங்கள் கொண்ட தருவிப்பு அறிக்கை உருவானது. சூ, தனது முன்னாள் மாணவரும் KTH-இல் முதுமுனைவர் ஆய்வாளருமான ஜாங்கை வருகைதரு ஆய்வாளராகப் பணியில் இணைய அழைத்தார். முனைவர் பட்ட ஆய்வுக் காலத்திலிருந்தே கிஸ் அனுமானத்தை ஜாங் தொடர்ந்து கவனித்து வந்தார்.

மாதிரியின் முன்மொழிவுகளைச் சூவும் ஜாங்கும் ஆராய்ந்து, நம்பிக்கையளிக்கும் தொடக்கக் குறிப்புகளைக் கண்டறிந்து, அடுத்தடுத்த ஆய்வுகளுக்கு வழிகாட்டும் பின்னூட்டங்களை வழங்கினர். இயந்திரம் பல்வேறு பகுத்தறிவுப் பாதைகளைத் தொடர்ந்து வாதங்களை உருவாக்கியது; எந்தத் திசைகளில் கூடுதல் ஆய்வு தேவை என்பதை கணிதவியலாளர்கள் முடிவுசெய்து, இறுதி நிரூபணத்தைத் தொகுக்க உதவினர்.

தொடர்ச்சியான பகுத்தறிவின் ஏழு தொகுதிகள் இருந்ததாக ஆய்வகம் விவரிக்கிறது. செயல்முறையின்போது, மாதிரியின் சிக்கல் வரைபடம் 15 கணுக்களிலிருந்து 389 ஆக விரிவடைந்தது. திரண்ட வெளியீடு ஏறத்தாழ ஆயிரம் பக்கங்களை எட்டியதுடன், டஜன் கணக்கான அணுகுமுறைகளையும் முன்வைத்தது.

சிக்கல் வரைபடம் என்பது சிறிய கணிதப் பணிகளையும் அவற்றின் தொடர்புகளையும் காட்டும் வரைபடம். ஒரு கணு இடைநிலைக் கூற்றைக் குறிக்கலாம்; மற்றொரு கணு அதை நிறுவத் தேவையான முடிவைக் குறிக்கலாம். இந்த அதிகரிப்பு, அமைப்பு சிக்கலை எவ்வளவு விரிவாகப் பிரித்து ஆராய்ந்தது என்பதைக் காட்டுகிறது.

முடிக்கப்பட்ட கணிதத்துக்கான பொறுப்பை ஜாங்கின் செயற்கை நுண்ணறிவுப் பயன்பாட்டு அறிவிப்பு நேரடியாக விளக்குகிறது: Intern-S2-ன் உள்நாட்டுப் பதிப்பு பல சுற்று உரையாடல்களின் மூலம் கருத்துகளையும் வாதங்களையும் உருவாக்க உதவியது; கணிதம் அனைத்தையும் அவர் தனிப்பட்ட முறையில் சரிபார்த்தார். தொடர்ச்சியான கலந்துரையாடல்களுக்காகச் சூவுக்கும் தனது ஆய்வுக் கட்டுரையில் நன்றி தெரிவித்துள்ளார்.

துணை மென்பொருள் வழங்கிய பங்களிப்பு

நீண்ட பகுத்தறிவுத் தொடர்களையும் மீண்டும் மீண்டும் வழங்கப்படும் மனிதப் பின்னூட்டத்தையும் நிர்வகிக்கும் நோக்கில், ஷாங்காய் செயற்கை நுண்ணறிவு ஆய்வகம் மாதிரியுடன் மென்பொருளையும் இணைத்தது. கடினமான கேள்வியைச் சிறிய பணிகளாகப் பிரித்து, பல திசைகளை ஆராய்ந்து, ஆய்வாளர்கள் மதிப்பிடுவதற்கான முடிவுகளைத் திருப்பி வழங்கும் திறன் இந்த அமைப்புக்கு இருந்தது.

பயிற்சி அணுகுமுறை, பரந்த அறிவியல் அறிவையும் ஆய்வு கணிதத்துக்கான உள்ளடக்கத்தையும் இணைத்தது. கணித ஆய்வுக் கட்டுரைகளிலிருந்து பெறப்பட்ட கடினமான சிக்கல்களும், முன்மொழியப்பட்ட தீர்வுகளைச் சரிபார்க்கும் முறைகளும் இதில் அடங்கின. சரிபார்க்கக்கூடிய வெகுமதிகளைப் பயன்படுத்திய வலுவூட்டல் கற்றலையும் ஆய்வகம் விவரிக்கிறது. அதாவது, வெற்றிகரமாகச் சரிபார்க்கக்கூடிய பகுத்தறிவு பயிற்சிக்கான சமிக்ஞையாக அமைந்திருக்கலாம்.

பின்னர், துணை அமைப்பிலிருந்து பெற்ற அனுபவத்தைப் பயன்படுத்தி ஆய்வாளர்கள் மாதிரியையே மேம்படுத்தினர். இடைநிலை முடிவுகளைக் கண்காணிப்பதும், புதிய வாதங்கள் உருவாகும்போது தவறுகளைத் திருத்துவதும் உள்ளிட்ட நீண்ட ஆய்வுச் செயல்முறை முழுவதும் பயனுள்ள முன்னேற்றத்தைத் தக்கவைத்தல் என்பதே நடைமுறை நோக்கமாக இருந்தது.

கணிதப் பகுத்தறிவை மையமாகக் கொண்ட மதிப்பீடுகளான IMO-Proof மற்றும் AdvancedMathBench தொடர்பான முடிவுகளையும் ஆய்வகம் குறிப்பிட்டது. கிஸ் திட்டத்தில், விரிவான தருவிப்புகளின் தொடர், நிபுணர் பின்னூட்டம், நிறைவுற்ற ஆய்வுக் கட்டுரை, அதைத் தொடர்ந்த முறையான சரிபார்ப்பு ஆகியவையே அமைப்பு செயல்பட்ட விதத்துக்கான மிக விரிவான சான்றுகளாகும்.

பீக்கிங் பல்கலைக்கழகம் நிரூபணத்தைச் சரிபார்த்த விதம்

பின் டோங், ருசுவான் லியூ தலைமையிலான பீக்கிங் பல்கலைக்கழகக் குழு, ஜாங்கின் ஆய்வுக் கட்டுரையில் உள்ள நான்கு முக்கியத் தேற்றங்களையும் முறையாக்க SHEAF கட்டமைப்பைப் பயன்படுத்தியது. வாதங்கள் சார்ந்திருக்கும் கிஸின் முடிவுகளும் இந்தப் பணியில் அடங்கின.

முறையாக்கம் என்பது கணித வரையறைகள், அனுமானங்கள், பகுத்தறிவு ஆகியவற்றைக் கணினியால் சரிபார்க்கக்கூடிய மொழிக்கு மாற்றுவதாகும். வழக்கமான ஆய்வுக் கட்டுரையில், பயிற்சிபெற்ற வாசகர் பரிச்சயமான படிகளைத் தாமாகவே நிரப்பிக் கொள்ளலாம். Lean-இல், அந்தப் படிகள் துல்லியமான கூற்றுகளாகவும் அனுமதிக்கப்பட்ட தருக்கச் செயல்பாடுகளாகவும் வெளிப்படுத்தப்பட வேண்டும்.

ஜியேடோங் ஜியாங் மற்றும் பின் வூ ஆகிய குழு உறுப்பினர்கள், இந்தப் பணிக்கு சுமார் ஐந்து நாட்கள் ஆனதாகவும், ஒரே நேரத்தில் 100 வரை செயற்கை நுண்ணறிவு முகவர்கள் இயங்கியதாகவும் தெரிவித்தனர். இதன் மூலம் சுமார் 550,000 வரிகள் கொண்ட Lean குறியீடு உருவானது. முறையான கூற்றுகள், ஆய்வுக் கட்டுரையின் முக்கியத் தேற்றங்களின் கணிதப் பொருளுடன் பொருந்துகின்றனவா என்பதையும் நிபுணர்கள் சரிபார்த்தனர்.

வரையறைகள், முன்மொழிவுகள், சார்புநிலைகள் ஆகியவற்றின் திசைகாட்டிய வரைபடமாக SHEAF பணியை ஒழுங்கமைத்தது. இதனால் வெவ்வேறு முகவர்கள் தொடர்புடைய பகுதிகளில் பணிபுரிய முடிந்தது; எந்தக் கூற்றுகளுக்கு நிரூபணங்கள் உள்ளன, எவை இன்னும் பணியில் உள்ளன என்பதையும் குழு கண்காணிக்க முடிந்தது.

இறுதி வாதங்களை மட்டும் மொழிமாற்றம் செய்வது முறையாக்கத்துக்குப் போதவில்லை. இயக்கவியலில் உள்ள சில துணை முடிவுகள், ஏற்கெனவே இருந்த முறையான கணித நூலகங்களில் இல்லை. அந்த அடிப்படைக் கட்டமைப்பை குழு வழங்க வேண்டியிருந்தது அல்லது ஏற்கெனவே கிடைத்த முடிவுகளைப் பயன்படுத்தும் வழிகளைக் கண்டறிய வேண்டியிருந்தது; பின்னர் அவற்றை இணைத்து முழுமையான தொடரை உருவாக்கியது.

ஆய்வுக் கட்டுரை arXiv முன்வெளியீடாகக் கிடைக்கிறது; முறையாக்கக் குறியீடு GitHub-இல் வெளியிடப்பட்டுள்ளது. இதழ் வெளியீடு குறித்தோ சக ஆய்வாளர் மதிப்பாய்வு முடிவு குறித்தோ அறிவிப்பில் எதுவும் குறிப்பிடப்படவில்லை.

இரு கட்டங்களும் ஏன் ஒன்றுக்கொன்று துணை?

Intern-S2 மற்றும் SHEAF வெவ்வேறு நோக்கங்களுக்குப் பயன்பட்டன. கணிதக் கருத்துகளையும் வாதங்களையும் தேடுவதற்கு முதலாவது உதவியது. Lean சரிபார்க்கக்கூடிய முறையான நிரூபணங்களை உருவாக்க இரண்டாவது உதவியது. ஆய்வின் போது கணிதவியலாளர்கள் வழிகாட்டினர்; கிடைத்த கணிதத்தைச் சரிபார்த்து, முறையான கூற்றுகள் நோக்கமிட்ட தேற்றங்களைப் பிரதிபலிக்கின்றனவா என்பதையும் மதிப்பிட்டனர்.

பணியின் அளவே இந்தப் பிரிவைத் தெளிவாக்குகிறது. ஆய்வுக் கட்டுரையாக உருவான சுமார் ஆயிரம் பக்க ஆய்வு வெளியீட்டுக்கு, ஆராய்ச்சியின் போது கிடைத்த தருவிப்புகள் ஆதாரமளித்தன; பின்னர் நடந்த சரிபார்ப்புச் செயல்முறையில் சுமார் 550,000 வரிகள் கொண்ட முறையான குறியீடு உருவானது. ஒவ்வொரு கட்டமும் வேறுபட்ட பணிக்கேற்ற வேறுபட்ட வடிவில் பணியை மாற்றியது.

எதிர்கால ஆய்வாளர்களுக்கு, பொதுவெளிக் கட்டுரை கணித வாதத்தை முன்வைக்கிறது; பொதுவெளிக் குறியீடு முறையான நிரூபணக் கட்டமைப்பைப் பதிவு செய்கிறது. முறையாக்கத்தின்போது சேர்க்கப்பட்ட துணை வரையறைகளும் முடிவுகளும், இதே துறையில் பிற்கால ஆய்வுகளுக்குத் தொடக்கப் புள்ளிகளாகவும் அமையலாம்.

அடுத்த கட்டம்: மீண்டும் பயன்படுத்தக்கூடிய சரிபார்ப்புக் கூறு

Intern Duanyan அறிவியல் கண்டுபிடிப்புத் தளத்துக்காக, இந்தப் பணிமுறையை கணிதச் சரிபார்ப்புக் கூறாகத் தொகுக்க ஷாங்காய் செயற்கை நுண்ணறிவு ஆய்வகம் திட்டமிட்டுள்ளது. மாதிரி வழியிலான ஆய்வு, நிபுணர் பின்னூட்டம், முறையான சரிபார்ப்பு ஆகியவற்றின் இணைப்பை அடுத்தடுத்த திட்டங்கள் மீண்டும் பயன்படுத்த உதவுவதே நோக்கம்.

இந்தத் திட்டத்தின் மூலம் உருவாக்கப்பட்ட பகுத்தறிவுத் திறன்களை, தொடர்புடைய கணிதக் கட்டமைப்புகளைக் கொண்ட பிற துறைகளிலும் பயன்படுத்த ஆய்வகம் திட்டமிட்டுள்ளது. ஆய்வுப் பிரச்சினையைத் தீர்த்து, பயனுள்ள முறைகளை மீண்டும் பயன்படுத்தக்கூடிய மென்பொருளாக மாற்றி, மற்றொரு ஆய்வில் அவற்றைப் பயன்படுத்துவது என்பதே முன்மொழியப்பட்ட சுழற்சி.

சூவைப் பொறுத்தவரை, கிரேட் பே பல்கலைக்கழகம், ஷாங்காய் செயற்கை நுண்ணறிவு ஆய்வகம், KTH, பீக்கிங் பல்கலைக்கழகம் ஆகியவற்றின் கூட்டுப்பணி நீண்டகால ஆய்வு ஆர்வத்தை மேலும் விரிவாக்குகிறது. பரந்த கணிதவியல் சமூகத்துக்கு, இது புதிய வகைப்பாட்டு முடிவையும் மனித வழிகாட்டுதலின் கீழ் செயற்கை நுண்ணறிவு ஆய்வில் பங்கேற்றதற்கான விரிவான எடுத்துக்காட்டையும் வழங்குகிறது.

முக்கிய அம்சங்கள்

• புதிய நிரூபணம், சிக்கலெண் பரிமாணம் மூன்றையும் உள்ளடக்கி, கிஸ் அனுமானத்தின் கோடிமானம்-ஒன்று நிலையைத் தீர்க்கிறது.
• ஆய்வுக் கட்டுரையின் ஒரே ஆசிரியர் ஜியேசோங் ஜாங்; கணிதம் அனைத்தையும் தாம் தனிப்பட்ட முறையில் சரிபார்த்ததாக அவர் தெரிவித்துள்ளார்.
• மீண்டும் மீண்டும் நடந்த ஆய்வு மற்றும் பின்னூட்டச் செயல்முறையில் டிஷெங் சூவும் ஜாங்கும் Intern-S2-க்கு வழிகாட்டினர்.
• மாதிரியின் சிக்கல் வரைபடம் 15 கணுக்களிலிருந்து 389 ஆக வளர்ந்தது; தருவிப்புகள் சுமார் ஆயிரம் பக்கங்களை எட்டின.
• நான்கு முக்கியத் தேற்றங்களையும் துணை முடிவுகளையும் Lean-இல் முறையாக்க பீக்கிங் பல்கலைக்கழகத்தின் SHEAF கட்டமைப்பு உதவியது.
• சரிபார்ப்புப் பணி சுமார் ஐந்து நாட்கள் எடுத்ததாகவும், சுமார் 550,000 வரிகள் கொண்ட குறியீட்டை உருவாக்கியதாகவும் தெரிவிக்கப்பட்டது.
• இந்தப் பணிமுறையை மீண்டும் பயன்படுத்தக்கூடிய கணிதச் சரிபார்ப்புக் கூறாக மாற்ற ஆய்வகம் திட்டமிட்டுள்ளது.