ແຈ້ງການ​ການ​ອ້າງ​ເອົາ​ສິດ. ຄີລ ຕັດສິນໃຈວ່າ​ຈະ​ພິສູດ​ມັນ​ຫຼືບໍ່.

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

ເປົ້າໝາຍ
ຕ້ອງ​ລະອຽດ​ກ່ຽວກັບ​ຄວາມ​ໝາຍ​ຂອງ​ການ​ເຮັດ​ແລ້ວ. 'ຕັດສິນໃຈ​ວ່າ X ແມ່ນ​ຈິງ ຫຼື ບໍ່ ແລະ ພິສູດ​ມັນ' ຄື​ກັບ 'ບອກ​ຂ້ອຍ​ກ່ຽວກັບ X'.
ຕົວເລືອກ​ທີ່​ຈະ​ລົບ​ແຖບ​
ຜູ້ຕັດສິນ​ຖື​ແຖບ​ນີ້​ຢ່າງ​ແທ້​ຈິງ. ຖາມ​ເພື່ອ​ພິສູດ​ລະດັບ​ລາງວັນ ແລະ ມັນຈະ​ບອກ​ທ່ານ​ຢ່າງ​ຊັດເຈນ ເມື່ອ​ແຖບ​ລົ້ມ​ລົງ, ແທນ​ທີ່​ຈະ​ປະກາດ​ໄຊຊະນະ.
ພາ​ເລດ
ບ່ອນນັ່ງຫຼາຍຂຶ້ນ ໝາຍຄວາມວ່າ ຈຸດຫຼາຍຂຶ້ນ ແລະ ຄ່າໃຊ້ຈ່າຍຫຼາຍຂຶ້ນຕໍ່ຮອບ.
ຜູ້ຊ່ຽວຊານ
ກົດລະບຽບກ່ຽວກັບມາດຕະຖານແລະກວດສອບຄືນທຸກໆສ່ວນຂອງຫຼັກຖານ. ຄ່າແບບຢ່າງທີ່ເຂັ້ມແຂງທີ່ສຸດຂອງທ່ານ.
ວົງ
ຈໍາກັດ​ການ​ໃຊ້​ຈ່າຍ
ກົດ​ມັນ​ຈະ​ຢຸດ​ການ​ໃຊ້​ງານ​ຂອງ match. ບໍ່ມີ​ຫຍັງ​ສູນ​ເສຍ​ໄປ​ເລີຍ.
​ເບິ່ງ​ເຫັນ
ລົງທະບຽນເພື່ອເລີ່ມຕົ້ນ match
ບັນຊີໃໝ່ ໄດ້ຮັບເງິນກູ້ ເລີ່ມຕົ້ນ, ພຽງພໍສໍາລັບ match ຢ່າງແທ້ຈິງ.
ຕົວກວດສອບ​ທີ່​ບໍ່​ສາມາດ​ດຶງ​ດູດ​ໄດ້

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

ພິສູດ​ທີ່​ລົ້ມເຫລວ​ແມ່ນ​ການ​ຄົ້ນ​ພົບ

ໃນເວລາທີ່ formalization ລົ້ມເຫລວ, ເປົ້າໝາຍ Lean ບໍ່ສາມາດປິດໄດ້ແມ່ນມອບໃຫ້ບ່ອນນັ່ງໃດກໍ່ຕາມແມ່ນດີທີ່ສຸດທີ່ຈະວາງໄວ້ເພື່ອໂຈມຕີມັນ: ພຽງແຕ່ວ່າເປົ້າຫມາຍ, ບໍ່ແມ່ນປະຫວັດສາດທັງຫມ. ຫຼັກຖານທີ່ປະຕິເສດຊື່ຂອງຄວາມແຕກແຍກຢ່າງຖືກຕ້ອງ, ເຊິ່ງແມ່ນຫຼາຍກ່ວາຫຼາຍທີ່ສຸດບໍ່ເປັນທາງການຄໍາເຫັນບໍ່ເຄີຍເຮັດ.

ບໍ່ມີຫຍັງຖືກພິສູດສອງຄັ້ງ

ທຸກໆ​ຂໍ້​ມູນ​ທີ່​ແຜງ​ສ້າງ​ຂຶ້ນ​ຈະ​ໄປ​ຢູ່​ໃນ​ບັນທຶກ​ທີ່​ແບ່ງປັນ​ຮ່ວມ​ກັບ​ການ​ພິສູດ​ຂອງ​ມັນ, ສະນັ້ນ​ມັນ​ບໍ່​ໄດ້​ຖືກ​ນຳ​ມາ​ໃຊ້​ຄືນ​ໃໝ່ ແລະ ຈຸດ​ຈົບ​ທີ່​ບໍ່​ໄດ້​ຖືກ​ທົດລອງ​ຄືນ​ໃໝ່. ບັນຫາ​ທີ່​ຍາວ​ນານ​ຢຸດ​ເຊົາ ແລະ ສືບຕໍ່​ໂດຍ​ບໍ່​ສູນ​ເສຍ​ວຽກ: ປິດ​ແທັບ ແລະ ​ກັບ​ມາ​ອີກ​ໃນ​ມື້​ອື່ນ.