சுமார் Theorem.chat
Theorem.chat ஒரு கணிதக் கோரிக்கையை எடுத்து அதை தீர்க்க முயற்சிக்கிறது. நீங்கள் கோரிக்கையை குறிப்பிடுகிறீர்கள், மற்றும் அது சந்திக்க வேண்டிய தரம். AI மாதிரிகளின் ஒரு குழு - நீங்கள் விரும்பும் அளவு, நீங்கள் விரும்பும் விற்பனையாளர்களிடமிருந்து - அதைத் தாக்குகிறது, மேலும் ஒரு மாதிரி தீர்ப்பு. பின்னர் Lean 4 க்கு எதிராக Mathlib ல் தர்க்கம் முறைப்படுத்தப்படுகிறது, மற்றும் லீன் கெர்னல் அது நிரூபிக்கப்பட்டதா என்று முடிவு செய்கிறது. அந்த கடைசி படிதான் தயாரிப்பு.
ஏன் ஒரு உட்கரு, மற்றொரு மாதிரி இல்லை
ஒரு மாதிரியை ஒரு கடினமான கேள்வியை கேட்கவும் அது சரியா அல்லது தவறா என்று ஒரு தெளிவான பதில் கிடைக்கும். பல கேள்விகளை கேட்கவும் அவர்கள் பெரும்பாலும் ஒப்புக் கொள்வார்கள், இது உறுதிப்படுத்தல் போல உணர்கிறது மற்றும் இல்லை: மாதிரிகள் பயிற்சி தரவை பகிர்ந்து கொள்ளும் மற்றும் பார்வை இல்லாத இடங்களை பகிர்ந்து கொள்ளும். இரண்டாவது மாதிரி முதல் ஒன்றை சரிபார்ப்பது அதே மாதிரியான தீர்ப்பு, இது சுற்றி பேச முடியும். லீன் கெர்னல் செய்ய முடியாது. அது ஒருவேளை அக்ஸியோம்ஸ் மற்றும் Mathlib ல் இருந்து கூற்றுகளை பெறுகிறது, அல்லது இல்லை, நம்பிக்கை முடிவுக்கு எந்த விளைவையும் ஏற்படுத்தாது.
வழக்கமான முறையில் நிரூபிக்கப்படாத நிரூபணங்கள் சரிபார்க்கப்பட்டு நிராகரிக்கப்படும். sorry ல் ஒரு துளை விட்டுவிடும் நிரூபணங்கள், native_decide க்கு அழைப்பு விடுக்கும் ஒன்று, உட்கரு நம்பகத்தன்மையில் கணக்கீடு செய்யும், அல்லது ஒரு புதிய அக்ஸியோமத்தை அமைதியாக அறிமுகப்படுத்தும் ஒன்று, கண்டறியப்பட்டு வெற்றியாக கணக்கிடப்படுவதை விட நிராகரிக்கப்படும்.
பலகத்தின் உண்மையான செயல்கள்
விவாதம் என்பது குறைந்த செலவு பகுதி. இந்த பலகம் இலக்கியத்துடன் வேலை செய்கிறது - arXiv, OpenAlex, Crossref - எனவே ஒரு அறியப்பட்ட முடிவு நன்றாக மீண்டும் பெறுவதை விட குறிப்பிடப்படுகிறது. இது SageMath மற்றும் PARI/GP கணக்கிட, Z3 மற்றும் CVC5 SMT தீர்க்க, OEIS தேடுவதற்கான தொடர் கண்டறிய, மற்றும் ஒரு மணல் பெட்டி பைத்தான் சூழல் வலைப்பின்னல் அணுகல் இல்லாமல். ஒரு யூகத்தை பத்து ஆயிரம் வழக்குகளுக்கு எதிராக சோதிக்கிறது யாரும் ஒரு சுற்று அதை நிரூபிக்க முயற்சிக்கும் முன், மற்றும் ஒரு எதிர் உதாரணம் விவாதத்தை உடனடியாக முடிக்கிறது.
ஆதாரம், திறமை அல்ல
ஒரு match தர்க்கத்தின் தரத்தில் மதிப்பிடப்படுவதில்லை. இந்தக் கோரிக்கை ஏற்றுக்கொள்ளும் தரநிலைகளில் பிரிக்கப்படுகிறது, மற்றும் ஒரு தரநிலை மூன்றாம் தரப்பால் பின்னால் ஏதாவது மீண்டும் சரிபார்க்க முடியும் போது மட்டுமே தீர்மானிக்கப்படுகிறது: தொடர்புடைய பகுதியைக் குறிப்பிடும் மூலத்தை, அல்லது அதன் உண்மையான வெளியீட்டைக் கொண்ட உண்மையில் செயல்படுத்தப்பட்ட குறியீட்டை. தீர்ப்பு வழங்குவதற்கு முன்பு தீர்ப்பு வழங்குபவர் அந்த ஆதாரத்தை மீண்டும் சரிபார்க்கிறார், மற்றும் ஒரு தரநிலை திறந்திருக்கும் போது match முடிந்தது என்று அறிவிக்க முடியாது.
நீங்கள் பட்டை அமைக்க
தரம் என்பது உங்களுடைய தேர்வு, மற்றும் தீர்ப்பாளரின் வார்த்தைகளில் உள்ளது. ஒரு கவனமான நிபுணர் ஏற்றுக்கொள்ளும் எதைப் பற்றி கேட்கவும் நீங்கள் அதைப் பெறுவீர்கள். ஒவ்வொரு கணிப்பும் கூறப்பட்டுள்ள ஒரு முழுமையான விளைவு சார்ந்த தர்க்கத்தைக் கேட்கவும் நீங்கள் அதற்கு எதிராக தீர்ப்பு வழங்கப்படுவீர்கள். ஒரு பரிசு சமர்ப்பிப்பு எதிர்கொள்ளும் வரிகளைக் கேட்கவும், நேர்மையான முடிவு பொதுவாக ஒரு சரியான கணக்கு, தொகுப்பு குறைந்த இடத்தில் உள்ளது - இது ஒரு நம்பிக்கையான கோரிக்கையை விட அதிக மதிப்புள்ளது, நீங்கள் எவ்வாறு இருந்தாலும் உங்களை நீங்கள் சரிபார்க்க வேண்டும்.
இது பற்றி தெளிவாக இருக்க: இது திறந்த பிரச்சனைகளை தீர்க்கும் இயந்திரம் அல்ல. இது ஒரு தர்க்கத்தை தீர்க்கப்படாத போது தீர்க்கப்படாததாக அனுமதிக்க மறுக்கும் இயந்திரம், மற்றும் அது உங்களுக்கு தவறான படி எது என்பதை தெளிவாக கூறுகிறது.
ஒரு தோல்வியடைந்த முறைமைப்படுத்தல் பயன்படும் வெளியீடு
Lean நிரூபணத்தை மூடவில்லை என்றால், நீங்கள் சரியான இலக்கை பெறுவீர்கள். செயல்முறையில் அது எப்போதும் கை- அசைத்த இடமாக இருக்கும் - ஒவ்வொருவரும் புராண பதிப்பைப் படித்த பிறகும் கையசைத்திருப்பார்கள். அந்த இலக்கு அதனைத் தாக்க சிறந்த இடத்தில் இருக்கும் இடத்திற்கு கொடுக்கப்படுகிறது, ஏற்கனவே முயற்சி செய்யப்பட்டவற்றுடன், வேறு எதுவுமில்லை. மாதிரிகள் அடைபட்டால், தங்களை முழு விலையில் மீண்டும் கூறுகின்றன; ஒரு குறிப்பிட்ட கேள்வியை விட ஒரு குறிப்பிட்ட கேள்வியை விட ஒரு பகுதி டாக்கன்களை அடைத்து விடுகிறது.
நீண்ட வேலை உயிர்வாழ்கிறது
ஒவ்வொரு லேமாவும் இந்த குழுவால் நிறுவப்பட்டது அதன் நிரூபணத்துடன் பகிரப்பட்ட லேட்ஜர் க்குள் செல்கிறது, எனவே முடிவுகள் ஒருமுறை எழுதப்படுகின்றன, அவை மீண்டும் பெறப்படுவதில்லை, மற்றும் இறுக்கமான முடிவுகள் பதிவு செய்யப்படுகின்றன, எனவே யாரும் அவற்றில் திரும்பி செல்ல முடியாது. Matches சேவையக பக்கத்தில் இயங்குகிறது மற்றும் சுத்தமாக நிறுத்தப்படுகிறது - நிதியில், ஒரு வழங்குநர் நிறுத்தத்தில் அல்லது நீங்கள் தத்தலை மூடினால் - மற்றும் நிறுத்தப்பட்ட இடத்தில் மீண்டும் தொடங்குகிறது.
இது எதற்கு அல்ல
தேற்றம் என்பது ஒரு கற்பனையான சொல். இந்த தளம் கணிதவியல், தர்க்கவியல், கணினி அறிவியல், இயற்பியல் மற்றும் பொருளாதாரக் கோட்பாடுகள் ஆகியவற்றுக்காக உருவாக்கப்பட்டது. உயிரியல், மருத்துவம், வேதியியல் அல்லது சமூக அறிவியல் போன்றவற்றில் உள்ள அனுபவ கேள்விகள் தேற்றங்களை உருவாக்குவதில்லை, அவை கண்டுபிடிப்புகளை உருவாக்குகின்றன, எந்த அளவு முறைப்படுத்தல்களும் அவற்றை தீர்மானிக்காது. எங்கள் சகோதரி தளம் referee.chat அதே பீன்- அண்ட்- ரெஃபெரீஸ் செயல்முறையை இயக்குகிறது, லீன் படி இல்லாமல், அதே கேள்விகளுக்கு.