ແຈ້ງການການອ້າງເອົາສິດ. ຄີລ ຕັດສິນໃຈວ່າຈະພິສູດມັນຫຼືບໍ່.
ແບບຢ່າງຂອງກຸ່ມຜູ້ໃຊ້ທີ່ໄດ້ໂຈມຕີບັນຫາຂອງທ່ານດ້ວຍປຶ້ມທີ່ມີຊື່ສຽງ, SageMath, PARI/GP ແລະຜູ້ແກ້ໄຂບັນຫາ SMT, ຫຼັງຈາກນັ້ນໄດ້ຮັບຜົນທີ່ເປັນທາງການໃນ Lean 4 ຕ້ານກັບ Mathlib. ເຄືອຂ່າຍຂອງ Lean ຈະຮັບເອົາການພິສູດ ຫຼືບໍ່ກໍບໍ່ໄດ້, ແລະບໍ່ມີຈໍານວນຂອງການປ່ຽນແປງທີ່ເຊື່ອຖືໄດ້. ເມື່ອມັນລົ້ມເຫຼວທ່ານຈະໄດ້ຮັບເປົ້າໝາຍທີ່ຖືກຕ້ອງທີ່ຍັງເຫຼືອ, ເຊິ່ງເປັນປົກກະຕິບ່ອນທີ່ການໂຕ້ວາທີແບບບໍ່ເປັນທາງການແມ່ນການໂຍນມືໄປມາ.
ຕົວກວດສອບທີ່ບໍ່ສາມາດດຶງດູດໄດ້
Lean 4 ກັບ Mathlib ປະເພດ-ກວດສອບຄໍາເວົ້າສຸດທ້າຍ, ແລະຫຼັກຖານທີ່ອີງໃສ່ sorry, native_decide ຫຼື axiom ໃຫມ່ແມ່ນປະຕິເສດແທນທີ່ຈະເປັນຈໍານວນ. ຂ້າງຄຽງມັນ: SageMath, PARI/GP, Z3, CVC5 ແລະ OEIS, ດັ່ງນັ້ນການກໍ່ສ້າງສາມາດໄດ້ຮັບການຄິດໄລ່ແລະລະບຸກ່ອນທີ່ຜູ້ໃດຜູ້ຫນຶ່ງພະຍາຍາມເພື່ອພິສູດສິ່ງໃດກ່ຽວກັບມັນ.
ພິສູດທີ່ລົ້ມເຫລວແມ່ນການຄົ້ນພົບ
ໃນເວລາທີ່ formalization ລົ້ມເຫລວ, ເປົ້າໝາຍ Lean ບໍ່ສາມາດປິດໄດ້ແມ່ນມອບໃຫ້ບ່ອນນັ່ງໃດກໍ່ຕາມແມ່ນດີທີ່ສຸດທີ່ຈະວາງໄວ້ເພື່ອໂຈມຕີມັນ: ພຽງແຕ່ວ່າເປົ້າຫມາຍ, ບໍ່ແມ່ນປະຫວັດສາດທັງຫມ. ຫຼັກຖານທີ່ປະຕິເສດຊື່ຂອງຄວາມແຕກແຍກຢ່າງຖືກຕ້ອງ, ເຊິ່ງແມ່ນຫຼາຍກ່ວາຫຼາຍທີ່ສຸດບໍ່ເປັນທາງການຄໍາເຫັນບໍ່ເຄີຍເຮັດ.
ບໍ່ມີຫຍັງຖືກພິສູດສອງຄັ້ງ
ທຸກໆຂໍ້ມູນທີ່ແຜງສ້າງຂຶ້ນຈະໄປຢູ່ໃນບັນທຶກທີ່ແບ່ງປັນຮ່ວມກັບການພິສູດຂອງມັນ, ສະນັ້ນມັນບໍ່ໄດ້ຖືກນຳມາໃຊ້ຄືນໃໝ່ ແລະ ຈຸດຈົບທີ່ບໍ່ໄດ້ຖືກທົດລອງຄືນໃໝ່. ບັນຫາທີ່ຍາວນານຢຸດເຊົາ ແລະ ສືບຕໍ່ໂດຍບໍ່ສູນເສຍວຽກ: ປິດແທັບ ແລະ ກັບມາອີກໃນມື້ອື່ນ.