អំពី Halmos
Halmos គឺ ក្រុមប្រឹក្សា សម្រាប់ គណិតវិទ្យា ដែល ម៉ាស៊ីន បម្រើ ពិនិត្យ គណិតវិទ្យា. វា មើល ឃើញ ថា ជា សមាសភាគ តំណ ណាមួយ រហូត ដល់ អ្នក សង្កេត ឃើញ ថា ប្រកាស ខ្លះ ដឹក ស្លាក គ្មាន ចំនួន នៃការ សរសេរ ទំនុកចិត្ត អាច ផលិត.
បញ្ហាជាមួយវេទិកាគណិតវិទ្យាផ្សេងទៀតទាំងអស់
MathOverflow, math.StackExchange, r/math, the arXiv comment sections. ពួកវាទាំងអស់មានតែមួយគត់ arbitrator នៃភាពត្រឹមត្រូវ: មនុស្សផ្សេងទៀត, ការតវ៉ា. នោះធ្វើការគួរឱ្យកត់សម្គាល់ល្អ, ហើយវាក៏ជាមូលហេតុដែលភស្តុតាងខុសសរសេរ fluently outranks មួយត្រឹមត្រូវមួយសរសេរអាក្រក់, និងហេតុអ្វី "ខ្ញុំពិនិត្យមើលវា" និង "ខ្ញុំជឿថាវា" មើលទៅដូចគ្នានៅលើទំព័រ.
Halmos បន្ថែមអ្នកកាត់ទោសទីពីរដែលមិនអាចត្រូវបានជជែកជាមួយ ។
អ្វីដែលម៉ាស៊ីនបម្រើពិតជាធ្វើ
ដាក់ប្លុកដែលមានព្រំដែនក្នុងអត្ថបទណាមួយ ឬមតិយោបល់ ហើយវារត់នៅទីនេះ ពេលដាក់ស្នើ ៖
| ប្លុក | អ្វីដែលកើតឡើង | អាចវារកបាន ∎? |
|---|---|---|
lean |
ប្រភេទបានពិនិត្យមើលប្រឆាំងនឹង Mathlib ។ ខឺណែលទទួលយកលក្ខខណ្ឌភស្តុតាង ឬវាមិនទទួលយកទេ ។ | បាទ/ ចាស |
sage | SageMath រត់វា លទ្ធផលពិតប្រាកដត្រូវបានបិទភ្ជាប់ទៅកាន់ប្រកាស ។ | គ្មាន |
gp | PARI/GP ដំណើរការវា។ | គ្មាន |
z3 | Z3 មើលឃើញសម្រាប់ម៉ូដែល: វិធីរហ័សបំផុតដើម្បី ច្រានចោល អ្វីមួយ ។ | គ្មាន |
python | Sandbox Python លទ្ធផលបានភ្ជាប់ ។ | គ្មាន |
លទ្ធផលដែលបង្ហាញនៅក្រោមប្លុកគឺជាអ្វីដែលឧបករណ៍បោះពុម្ពដោយប្រយោគ ។ មិនមែនជាសេចក្ដីសង្ខេប ៖ ការសង្ខេបគឺជាកន្លែងដែលការបង្កើតនឹងលោតចូល ។
របៀបសាកល្បងវាក្នុងរយៈពេលប្រហែលមួយនាទី
- មតិយោបល់ធម្មតា ។ ប្រកាសភាគច្រើនមានគណិតវិទ្យានៅក្នុងពួកគេទាំងអស់និងគ្មានអ្វីនៅទីនេះត្រូវការណាមួយឡើយ.
- សរសេរគណិតវិទ្យាក្នុងបន្ទាត់ ជាមួយ
$…$, ឬប្លុកបង្ហាញជាមួយ$$…$$. វាបង្ហាញជាគណិតវិទ្យាពិតប្រាកដរបស់សំណុំតួអក្សរ គ្មានអ្វីត្រូវបានប្រតិបត្តិទេ ។ វាគឺគ្រាន់តែជាការចង្អុលបង្ហាញ ។ មើលមួយ - សំណួរម៉ាស៊ីន ។ ប្លុកដែលបានដាក់ស្លាកដែលមានរាន
sage,gp,z3ឬpythonអនុវត្តនៅទីនេះនិងលទ្ធផលរបស់វាភ្ជាប់ទៅនឹងប្រកាសរបស់អ្នក, ពាក្យដដែលៗ. នោះជាភស្តុតាង, មិនមែនជាភស្តុតាង. មើលមួយ - គូរអ្វីមួយ ជាមួយនឹង
plotប្លុក (matplotlib, ជាមួយ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 ដែលបានទទួលយកផ្ដល់សញ្ញាបញ្ជាក់ ។ បន្ថែមប្រភព និងម៉ាក្រូ LaTeX ផ្ទាល់ខ្លួននៅក្រោមកម្មវិធីនិពន្ធ ឬកំណត់លំនាំដើមក្នុង ទម្រង់របស់អ្នក. ជ្រើសប្រធានបទ និងស្លាកដូច្នេះអ្នកអានដែលមានចំណាប់អារម្មណ៍អាចរកឃើញប្រកាសរបស់អ្នក.
ប្រកាសដែលបានបោះពុម្ពមានតំណ កែសម្រួលប្រកាស ។ ការកែសម្រួលដែលបានរក្សាទុកនៅតែឯកជនរហូតដល់អ្នកបោះពុម្ពផ្សាយការធ្វើឲ្យទាន់សម័យ ។ អត្ថបទរក្សាអាសយដ្ឋានរបស់វា ហើយការពិនិត្យម៉ាស៊ីនដែលមានស្រាប់នៅតែជាប់នឹងអត្ថបទដែលពួកវាបានពិនិត្យ ។
អានបន្តជាមួយគ្នា
រក្សាទុកអត្ថបទទៅបញ្ជីអានឯកជនរបស់អ្នក និងតាមដានអ្នកនិពន្ធ ឬប្រធានបទសម្រាប់ផ្ទាល់ខ្លួន បន្ទាប់ ឆ្លើយតបទៅនឹងការប្រកាសនិងមតិយោបល់របស់អ្នកលេចឡើងនៅក្នុង ឆ្លើយតបទៅអ្នក.
បង្កើតសៀវភៅ ឬស៊េរី ដើម្បីតភ្ជាប់អត្ថបទដែលបានបោះពុម្ពផ្សាយរបស់អ្នក ។ បន្ថែមជំពូក រៀបចំលំដាប់របស់ពួកគេ និងធ្វើមាតិកាសាធារណៈពេលដែលរួចរាល់ ។ សម្រាំងឯកជនលាក់បញ្ជីមាតិការបស់វា អត្ថបទរបស់វានៅតែបោះពុម្ពផ្សាយដោយឡែក ។
សញ្ញា
∎ ឈ្មោះរបស់វាគឺ halmos, បន្ទាប់ពីលោកប៉ូល Halmos, ដែលបានបង្ហាញនិមិត្តសញ្ញាបញ្ចប់នៃភស្តុតាង. វាគឺជារឿងតែមួយគត់នៅលើតំបន់បណ្ដាញនេះដែលដឹកអាជ្ញាធរ, ដូច្នេះវាជាការពិចារណាពិបាកក្នុងការទទួលបាន:
- មានតែ Lean ប៉ុណ្ណោះអាចកំណត់វាបាន ។ ការបោះពុម្ព Sage
Trueគឺជាភស្តុតាងមិនមែនជាភស្តុតាងទេ ។ sorry,native_decide, ថ្មីaxiom,unsafeនិងdebug.skipKernelTCត្រូវបានបដិសេធ មុន ឯកសាររត់ ដូច្នេះការឆបោកមិនអាចចំណាយពេលគណនាបានឡើយ ។- រត់ត្រូវបានបិទភ្ជាប់ទៅអត្ថបទជាក់លាក់ដែលបានបង្កើតវា ។ កែសម្រួលអត្ថបទ ហើយសញ្ញាសម្គាល់នឹងទៅចាស់ជាងការផ្ទេរទៅពាក្យថ្មី ។
- បើអ្នកពិនិត្យចុះក្រោម អ្នកទទួល "មិនអាចរត់បានទេ", មិនធ្លាប់ទេ "បានបដិសេធ". កម្មវិធីពិនិត្យស្ថានភាព គឺជាសាធារណៈសម្រាប់ហេតុផលនោះ ។
ឯកសាររួម
ការផ្ទៀងផ្ទាត់គឺមានតម្លៃថោក ការរកឃើញគឺមិនមែនទេ ។ ឯកសាររួម ជាការចែករំលែក pool នៃការគណនាដែល grinds លើបញ្ហាបើកចំហនេះក្រុមប្រឹក្សានេះបានបោះឆ្នោតឡើង ។ នរណាម្នាក់អាចចូលរួមក្នុងវា, គ្មាននរណាម្នាក់មានលទ្ធផលផ្ទាល់ខ្លួន, និងរាល់ការរត់វាមូលនិធិគឺសាធារណៈ, រួមទាំងអ្នកដែលបានទទួលកន្លែងណាមួយ, ដែលជាធម្មតាគឺជាអ្នកដែលមានព័ត៌មាន ។
នរណារត់វា
Halmos គឺឯករាជ្យ និងតូច ។ ប្រសិនបើមានអ្វីមួយនៅទីនេះខុស វិធីរហ័សបំផុតដើម្បីបង្ហាញវាគឺជាប្លុកម៉ាស៊ីនបម្រើអាចរត់ ។ ទាក់ទងមកយើង.