ກ່ຽວກັບ Halmos
Halmos ແມ່ນ ຫນ່ວຍງານສໍາລັບຄະນິດສາດບ່ອນທີ່ເຊີບເວີກວດສອບຄະນິດສາດ. ມັນເບິ່ງຄືວ່າເປັນ link aggregator ໃດຫນຶ່ງຈົນກ່ວາທ່ານສັງເກດເຫັນວ່າບາງບົດຄວາມມີຫມາຍບໍ່ຈໍານວນຂອງການຂຽນເຊື່ອຖືສາມາດຜະລິດ.
ບັນຫາກັບເວບໄຊທ໌ຄະນິດສາດອື່ນໆ
MathOverflow, math.StackExchange, r/math, arXiv comment section. ທຸກໆຄົນມີຜູ້ຕັດສິນຄວາມຖືກຕ້ອງຢ່າງດຽວ: ຄົນທີ່ອື່ນ, ຂໍ້ຂັດແຍ່ງ. ນັ້ນເຮັດວຽກໄດ້ດີຫຼາຍ, ແລະມັນກໍ່ເປັນເຫດຜົນທີ່ວ່າເຫດຜົນທີ່ຜິດທີ່ຂຽນ fluently ເກີນໄປທີ່ຖືກຕ້ອງທີ່ຂຽນບໍ່ດີ, ແລະເປັນຫຍັງ "ຂ້ອຍກວດເບິ່ງມັນ" ແລະ "ຂ້ອຍເຊື່ອມັນ" ເບິ່ງຄືກັນໃນຫນ້າ.
Halmos ເພີ່ມຜູ້ຕັດສິນຄົນທີ2ທີ່ບໍ່ສາມາດໂຕ້ຖຽງໄດ້ກັບມັນໄດ້.
ສິ່ງທີ່ເຊີບເວີເຮັດ
ວາງບລັອກທີ່ຖືກປົກປ້ອງໄວ້ໃນບົດຄວາມ ຫຼື ຄຳເຫັນໃດໆ ແລະ ມັນຈະແລ່ນຢູ່ທີ່ນີ້, ເມື່ອສົ່ງຂໍ້ຄວາມ:
| ប្លុក | ສິ່ງທີ່ຈະເກີດຂຶ້ນ | ສາມາດເຮັດໄດ້ບໍ? ∎? |
|---|---|---|
lean |
ກວດສອບປະເພດກັບ Mathlib. ຄໍລ໌ຈະຮັບເອົາຂໍ້ພິສູດ ຫຼື ບໍ່. | ແມ່ນ |
sage | SageMath ແລ່ນມັນ; ຜົນອອກມາທີ່ຈິງແມ່ນຖືກຕິດຢູ່ກັບບົດຄວາມ. | ບໍ່ໄດ້ |
gp | PARI/GP ເປັນຜູ້ຈັດການມັນ. | ບໍ່ໄດ້ |
z3 | Z3 ເບິ່ງແບບແບບ: ວິທີທີ່ໄວທີ່ສຸດເພື່ອ ປະຕິເສດ ບາງສິ່ງບາງຢ່າງ | ບໍ່ໄດ້ |
python | Python ແບບ Sandbox, ຜົນອອກມາຖືກຕິດຕໍ່ໄວ້. | ບໍ່ໄດ້ |
ຜົນອອກມາທີ່ສະແດງຢູ່ພາຍໃຕ້ກ່ອງແມ່ນສິ່ງທີ່ເຄື່ອງມືພິມອອກມາ, ຢ່າງເຕັມທີ່. ບໍ່ເຄີຍເປັນບົດສັງເກດຫຍໍ້: ການສັງເກດຫຍໍ້ແມ່ນບ່ອນທີ່ການສ້າງຕັ້ງຈະຫຼົ້ມລົງມາ.
ວິທີການທົດລອງໃຊ້, ໃນປະມານ 1 ນາທີ
- ຄໍາເຫັນປົກກະຕິ ຫຼາຍທີ່ສຸດ posts ມີຄະນິດສາດໃນພວກເຂົາທັງຫມົດແລະບໍ່ມີຫຍັງຢູ່ທີ່ນີ້ຕ້ອງການໃດໆ. ຕອບຝາ.
- សរសេរຄະນິດສາດໃນແຖບ ດ້ວຍ
$…$, ຫຼື ສະແດງແບັກທີ່ມີ$$…$$. ມັນສະແດງເປັນຕົວເລກຕົວຈິງທີ່ມີຕົວອັກສອນທີ່ຖືກເລືອກໄວ້; ບໍ່ມີຫຍັງຖືກປະຕິບັດເລີຍ. ມັນແມ່ນພຽງແຕ່ຕົວເລກທີ່ຖືກເລືອກໄວ້ເທົ່ານັ້ນ. ເບິ່ງໜຶ່ງ - ຖາມຈັກຈັກ ແທັກກ້ອນທີ່ຖືກປົກດ້ວຍຝາ
sage,gp,z3ឬpythonຕົວເລືອກນີ້ຈະຖືກປະຕິບັດຢູ່ທີ່ນີ້ ແລະ ຜົນອອກມາຈະຖືກຕິດຕໍ່ກັບບົດຄວາມຂອງທ່ານ, ຢ່າງເຕັມທີ່. ນັ້ນແມ່ນຫຼັກຖານ, ບໍ່ແມ່ນການພິສູດ. ເບິ່ງໜຶ່ງ - ແຕ້ມບາງສິ່ງບາງຢ່າງ ດ້ວຍ
plotຕົວເລືອກpltແລະnpແລ້ວແລ້ວມາ, ຫຼືລະບຸລໍາດັບດ້ວຍoeis: ປ້າຍຕົວເລກເຕັມ ແລະມັນກັບຄືນມາຊື່, ຖ້າມັນຮູ້ຈັກ. - ພິສູດບາງສິ່ງບາງຢ່າງ. A-M_BAR_ភាសាបារាំង (បារាំង)
leanຕົວກ່ອງຖືກກວດສອບປະເພດໂດຍໃຊ້ Mathlib. ປ້າຍສິ່ງນີ້ໃສ່ຄໍາເຫັນໃດໆ: ເບິ່ງໜຶ່ງ
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```ການລົງທະບຽນແມ່ນຊື່ຜູ້ໃຊ້ ແລະ ລະຫັດຜ່ານ: ບໍ່ມີອີເມວ, ບໍ່ມີຂັ້ນຕອນການຢືນຢັນ. ທຸກສິ່ງທຸກຢ່າງທີ່ຜູ້ກວດສອບເຮັດຢູ່ໃນປັດຈຸບັນແມ່ນຢູ່ໃນ ជួរ, ແລະ ສະຖານະການຢູ່ຂອງຜູ້ກວດສອບແຕ່ລະຄົນແມ່ນຢູ່ໃນ ໜ້າທີ່ໜ້າທີ່: ຖ້າມີອັນໜຶ່ງລົ້ມລົງ ທ່ານຈະຖືກບອກວ່າ "ບໍ່ສາມາດແລ່ນ" ບໍ່ເຄີຍ "ຖືກປະຕິເສດ"
ພິມຕາມຄວາມໄວຂອງທ່ານ
ເລີ່ມຕົ້ນການໂພດ ແລະປ່ຽນລະຫວ່າງການຂຽນ ແລະການເບິ່ງກ່ອນ ເພື່ອເບິ່ງຄະນິດສາດຂອງທ່ານຄືກັບຜູ້ອ່ານຈະເຮັດໄດ້. ການປ່ຽນແປງຈະຖືກບັນທຶກໄວ້ໂດຍອັດຕະໂນມັດໃນ ຮ່າງຂອງທ່ານ; ບັນທຶກຮ່າງກໍ່ເຮັດວຽກໄດ້ໂດຍບໍ່ຕ້ອງໃຊ້ JavaScript. ຮ່າງແລະເບິ່ງກ່ອນບໍ່ເຄີຍປະມວນຜົນໂປຣແກຣມເລີຍ. ເຜີຍແຜ່ເມື່ອທ່ານພ້ອມທີ່ຈະແບ່ງປັນແລ້ວ.
ໃຊ້ຫົວຂໍ້ເພື່ອສ້າງລາຍຊື່ເນື້ອໃນຂອງບົດຄວາມ. ຕົວເລືອກການເພີ່ມຈະເພີ່ມການອະທິບາຍ, ທິດສະດີ, ພິສູດ, ຕົວຢ່າງ, ຕາຕະລາງ ແລະ ການເຊື່ອມຕໍ່. ຕົວຢ່າງ:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::ຕົວແທນທີ່ໃຊ້ໄດ້ກັບການກວດສອບແບບ Lean ແມ່ນຕົວແທນທີ່ໃຊ້ໄດ້ກັບການກວດສອບແບບ Lean. ເພີ່ມແຫຼ່ງຂໍ້ມູນ ແລະ ມາກໂຣ LaTeX ຕາມໃຈເອງພາຍໃຕ້ຕົວສ້າງ ຫຼື ຕັ້ງຄ່າແບບເດີມໃນ ទម្រង់ປະຫວັດຂອງທ່ານເລືອກຫົວຂໍ້ ແລະ ແທັກ ເພື່ອຜູ້ອ່ານທີ່ສົນໃຈຈະສາມາດຊອກຫາບົດຄວາມຂອງທ່ານໄດ້
ບົດຄວາມທີ່ໄດ້ເຜີຍແຜ່ມີຕ່ອງໂສ້ ແກ້ໄຂບົດຄວາມ. ການປ່ຽນແປງທີ່ໄດ້ບັນທຶກໄວ້ຍັງເປັນສ່ວນຕົວຈົນກວ່າທ່ານຈະໄດ້ເຜີຍແຜ່ການອັບເດດ. ບົດຄວາມຍັງຮັກສາທີ່ຢູ່ຂອງມັນ, ແລະ ການກວດສອບເຄື່ອງທີ່ມີຢູ່ແລ້ວ ຍັງຄົງຕິດກັບຂໍ້ຄວາມທີ່ໄດ້ກວດສອບໄວ້.
ອ່ານຕໍ່ໄປ
ບັນທຶກບົດຄວາມໄປຍັງລາຍຊື່ການອ່ານສ່ວນຕົວຂອງທ່ານ ແລະ ຕິດຕາມຜູ້ຂຽນ ຫຼື ຫົວຂໍ້ສຳລັບສ່ວນຕົວ ຕາມ ຕອບຕໍ່ບົດຄວາມຂອງທ່ານ ແລະ ຄໍາເຫັນຈະປາກົດໃນ ຕອບກັບທ່ານ.
ສ້າງສະບັບປື້ມ ຫຼື ຊຸດ ຕົວເລືອກນີ້ຈະໃຊ້ເພື່ອເຊື່ອມຕໍ່ບົດຄວາມທີ່ໄດ້ພິມອອກມາຂອງທ່ານ. ເພີ່ມບົດ, ຈັດລຳດັບຂອງພວກມັນ ແລະ ເຮັດໃຫ້ເນື້ອໃນເປັນສາທາລະນະ ເມື່ອພ້ອມ. ຊຸດສ່ວນຕົວຈະປົກປິດລາຍຊື່ເນື້ອໃນຂອງມັນ; ບົດຄວາມຂອງມັນຈະຍັງຖືກພິມອອກເປັນສ່ວນຕົວຢູ່.
ຕົວຊີ້ວັດ
∎ ຖືກເອີ້ນວ່າ halmos, ຫຼັງຈາກ Paul Halmos, ຜູ້ທີ່ໄດ້ນໍາສະເຫນີສັນຍາລັກສຸດທ້າຍຂອງຫຼັກຖານ. ມັນແມ່ນສິ່ງດຽວທີ່ຢູ່ໃນເວັບໄຊນີ້ທີ່ນໍາເອົາອໍານາດ, ສະນັ້ນມັນແມ່ນມີຈຸດປະສົງຍາກທີ່ຈະໄດ້ຮັບ:
- ມີແຕ່ Lean ເທົ່ານັ້ນທີ່ສາມາດຕັ້ງມັນໄດ້. Sage printing
Trueນີ້ແມ່ນຫຼັກຖານ, ບໍ່ແມ່ນການພິສູດ. sorry,native_decide, ໃໝ່axiom,unsafeແລະdebug.skipKernelTCຖືກປະຕິເສດ ກ່ອນ ໄຟລ໌ຈະຖືກຂັບເຄື່ອນ, ສະນັ້ນການຫລອກລວງຈະບໍ່ສາມາດໃຊ້ການຄິດໄລ່ໄດ້ເລີຍ.- ການແລ່ນຈະຖືກຕິດຕັ້ງໃສ່ຂໍ້ຄວາມທີ່ໄດ້ສ້າງມັນໄວ້ຢ່າງແທ້ຈິງ. ປ່ຽນແປງບົດຄວາມ ແລະ ຕົວຊີ້ວັດຈະຖືກລົບແທນທີ່ຈະໂອນໄປຫາຄໍາໃໝ່.
- ຖ້າມີຜູ້ນລົງແລ້ວ ທ່ານຈະໄດ້ "ບໍ່ສາມາດປະມວນຜົນໄດ້", ບໍ່ເຄີຍ "ປະຕິເສດ". ກວດສອບສະຖານະ ຖືກເປີດເຜີຍ ສໍາລັບເຫດຜົນນັ້ນ.
Commons ທົ່ວໄປ
ການກວດສອບແມ່ນລາຄາຖືກ; ການຄົ້ນພົບແມ່ນບໍ່. Commons ທົ່ວໄປ ນີ້ແມ່ນການແບ່ງປັນການຄິດໄລ່ທີ່ເຮັດໃຫ້ບັນຫາເປີດທີ່ໄດ້ຮັບການເລືອກຕັ້ງຈາກຄະນະກຳມະການນີ້ເປັນຈິງ. ທຸກໆຄົນສາມາດປະກອບສ່ວນເຂົ້າໃນມັນ, ບໍ່ມີໃຜເປັນເຈົ້າຂອງຜົນທີ່ໄດ້ມາ, ແລະ ທຸກໆການໃຊ້ງານແມ່ນມີທຶນທີ່ເປັນສາທາລະນະ, ລວມທັງພວກທີ່ບໍ່ໄດ້ໄປບ່ອນໃດ, ເຊິ່ງເປັນປົກກະຕິແລ້ວແມ່ນພວກທີ່ໃຫ້ຂໍ້ມູນທີ່ດີ.
ໃຜເປັນຜູ້ຂັບມັນ
Halmos ແມ່ນບໍ່ຂຶ້ນກັບຜູ້ອື່ນ ແລະ ນ້ອຍ. ຖ້າມີສິ່ງໃດຜິດຢູ່ທີ່ນີ້, ວິທີທີ່ໄວທີ່ສຸດເພື່ອພິສູດມັນແມ່ນການບລັອກທີ່ເຊີບເວີສາມາດແລ່ນໄດ້. ຕິດຕໍ່.