បញ្ជាក់ការអះអាង & # 160; ។ ខឺណែលសម្រេចចិត្តថាតើវាត្រូវបានបង្ហាញឬអត់ & # 160; ។
បន្ទះនៃម៉ូដែលវាយប្រហារបញ្ហារបស់អ្នកជាមួយនឹងសិល្បៈ, SageMath, PARI/GP និងអ្នកដោះស្រាយ SMT បន្ទាប់មកធ្វើឲ្យលទ្ធផលជាផ្លូវការនៅក្នុង Lean 4 ប្រឆាំងនឹង Mathlib ។ ខឺណែលរបស់ Lean ទទួលយកភស្តុតាងឬវាមិនធ្វើទេ ហើយគ្មានចំនួននៃការផ្លាស់ប្ដូរប្រលោមលោកដែលមានទំនុកចិត្តនោះទេ ។ ពេលដែលវាបរាជ័យអ្នកទទួលបានគោលដៅជាក់លាក់ដែលនៅសល់ដែលជាធម្មតានៅកន្លែងដែលការចោទប្រកាន់មិនផ្លូវការគឺជាដៃដែលបានហោះ ។
កម្មវិធីពិនិត្យដែលមិនអាចជឿបាន
Lean 4 ជាមួយ Mathlib ប្រភេទ-ពិនិត្យមើលសេចក្តីថ្លែងការណ៍ចុងក្រោយនិងភស្តុតាងដែលពឹងផ្អែកលើ sorry, native_decide ឬ axiom ថ្មីមួយត្រូវបានបដិសេធជំនួសឱ្យរាប់. ក្បែរវា: SageMath, PARI/GP, Z3, CVC5 និង OEIS, ដូច្នេះការសាងសង់អាចត្រូវបានគណនានិងកំណត់អត្តសញ្ញាណមុនពេលនរណាម្នាក់ព្យាយាមដើម្បីបង្ហាញអ្វីមួយអំពីវា។
ភស្តុតាងដែលបានបរាជ័យគឺជាការរកឃើញ
ពេល formalization បរាជ័យ, គោលដៅ Lean អាចមិនបិទត្រូវបានប្រគល់ទៅកន្លែងណាដែលល្អបំផុតត្រូវបានដាក់ដើម្បីវាយប្រហារវា: គ្រាន់តែជាគោលដៅនោះ, មិនប្រវត្តិទាំងមូល. ភស្តុតាងដែលច្រានចោលឈ្មោះចន្លោះច្បាស់លាស់, ដែលគឺច្រើនជាងការតវ៉ាមិនផ្លូវការភាគច្រើនដែលធ្លាប់ធ្វើ.
គ្មានអ្វីត្រូវបានបង្ហាញពីរដងទេ
គ្រប់លេម៉ាដែលបន្ទះបង្កើតឡើងទៅក្នុងបណ្ណសារដែលបានចែករំលែកជាមួយនឹងភស្តុតាងរបស់វា ដូច្នេះវាមិនដែលបានដកស្រង់ឡើងវិញ និងចុងបញ្ចប់ដែលស្លាប់មិនដែលត្រូវបានព្យាយាមម្ដងទៀតទេ & # 160; ។ បញ្ហាយូរអង្វែងផ្អាក និងបន្តដោយមិនបាត់បង់ការងារ & # 160; ៖ បិទផ្ទាំង និងមកវិញថ្ងៃស្អែក & # 160; ។