ඉල්ලීම ප්‍රකාශ කරන්න. කර්නලය එය ඔප්පු කර ඇතිද යන්න තීරණය කරයි.

ආකෘති මණ්ඩලයක් සාහිත්යය, SageMath, PARI/GP සහ SMT විසඳුමක් සමඟ ඔබේ ගැටලුවට පහර, පසුව Lean 4 Mathlib එරෙහිව ප්රතිඵලය නිල වශයෙන්. ලෙනින් කර්නලය සාක්ෂි පිළිගන්නේ හෝ එය කරන්නේ නැහැ, සහ කිසිදු විශ්වාසවන්ත ප්රාසාංගික ප්රමාණයක් වෙනස්. එය අසාර්ථක වන විට ඔබ ඉතිරි නිශ්චිත ඉලක්කය ලබා ගන්න, සාමාන්යයෙන් නිල නොවන තර්කය අතින් හඬා සිටි ස්ථානයේ.

අරමුණ
සිදු කර ඇති අර්ථය ගැන විශේෂයෙන් සඳහන් කරන්න. 'X සත්‍යද යන්න තීරණය කරන්න, එය ඔප්පු කරන්න' 'X ගැන මට කියන්න'.
බාර් එකට යන්න ඕනේ
විනිසුරු වචනානුසාරයෙන් මෙම බාර් පවත්වාගෙන. ත්යාග මට්ටමේ සාක්ෂි ඉල්ලා එය මණ්ඩලය කෙටි වැටෙන විට පැහැදිලිව ඔබට කියන්නම්, ජයග්රහණය ප්රකාශ කිරීමට වඩා.
පැනලය
වැඩි ආසන වැඩි කෝණ, හා වටයකට වැඩි වියදමක් අදහස්.
විනිසුරු
නියමයන් මත නීති සහ සෑම සාක්ෂි කෑල්ලක් නැවත පරීක්ෂා. ඔබේ ශක්තිමත්ම ආකෘතිය වටිනා.
වට
වියදම් සීමා
ඒකට ගැහුවොත් match නවතිනවා, කිසිම දෙයක් නැතිවෙන්නේ නෑ.
දෘශ්‍යතාව
match ආරම්භ කිරීමට ලියාපදිංචි වන්න
නව ගිණුම් ආරම්භක ණය ලබා ගන්න, ඇත්ත match සඳහා ප්‍රමාණවත්.
තේරුම් ගත නොහැකි පරීක්ෂකයෙක්

Mathlib වර්ගය-පරීක්ෂා අවසන් ප්රකාශය සමග Lean 4, සහ sorry, native_decide හෝ නැවුම් axiom මත හේත්තු සාක්ෂියක් ගණන් වඩා ප්රතික්ෂේප කරනු ලැබේ. එය සමග: SageMath, PARI/GP, Z3, CVC5 සහ OEIS, ඒ නිසා ඉදිකිරීම් කිසිවෙකු එය ගැන කිසිවක් ඔප්පු කිරීමට උත්සාහ පෙර ගණනය හා හඳුනාගත හැක.

අසාර්ථක සාක්ෂි හොයාගන්නවා.

නිල වශයෙන් අසාර්ථක වන විට, ඉලක්කය ලෙයින් සමීප කළ නොහැකි එය පහර දීමට හොඳම තැන්පත් කරන ඕනෑම ආසනයට භාර දී ඇත: ඒ ඉලක්කය පමණක්, මුළු ඉතිහාසය නොවේ. ප්රතික්ෂේප සාක්ෂි නිශ්චිතව හිඩැස නම්, වඩාත් නිල නොවන තර්ක කවදාවත් වඩා වැඩි වන.

කිසිම දෙයක් දෙවරක් ඔප්පු කරන්න බෑ.

මණ්ඩලය ස්ථාපිත සෑම lemma එහි සාක්ෂි සමග හවුල් ලේඛන ගමන්, ඒ නිසා එය නැවත ව්යාප්ත හා අසාර්ථක අවසන් කවදාවත් නැවත උත්සාහ කර නැත. දිගු ගැටළු වැඩ අහිමි තිත වසා හා නැවත: ටැබ් වසා හෙට ආපසු එන්න.