கோரிக்கையை குறிப்பிடவும். அது நிரூபிக்கப்பட்டதா என்பதை உட்கரு முடிவு செய்கிறது.

ஒரு மாதிரிகளின் குழு உங்கள் பிரச்சனைகளை இலக்கியத்துடன் தாக்குகிறது, SageMath, PARI/GP மற்றும் ஒரு SMT தீர்ப்பாளர், பின்னர் Lean 4 ல் Mathlib க்கு எதிராக முடிவுகளை முறைப்படுத்துகிறது. லீன்ஸ் உட்கரு நிரூபணத்தை ஏற்கலாம் அல்லது ஏற்காது, மற்றும் எந்த அளவு நம்பிக்கையான புராணமும் அதை மாற்றாது. அது தோல்வியடைந்தால் நீங்கள் சரியான இலக்கை பெறுவீர்கள், இது வழக்கமாக அநாமதேய தர்க்கம் கை- சைகை செய்த இடத்தில் உள்ளது.

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

Lean 4 Mathlib வகை- சரிபார்க்கிறது கடைசி வாக்கியம், மற்றும் ஒரு நிரூபிப்பு sorry, native_decide அல்லது ஒரு புது axiom மீது ஈடுபட்டது எண்படுத்தப்படுவதை விட நிராகரிக்கப்படுகிறது. அதன் பக்கத்தில்: SageMath, PARI/GP, Z3, CVC5 மற்றும் OEIS, எனவே ஒரு கட்டமைப்பு கணிக்க முடியும் மற்றும் யாராவது அதை பற்றி ஏதாவது நிரூபிக்க முயற்சிக்கும் முன்பு அடையாளம் காணப்படுகிறது.

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

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

ஒன்றும் இருமுறை நிரூபிக்கப்படவில்லை

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