ஹால்மோஸ் பற்றி

Halmos கணிதத்திற்கு ஒரு பலகை, சேவையகம் கணிதத்தை சரிபார்க்கிறது. இது எந்த இணைப்பு கூட்டுபொறியை போலவே உள்ளது, சில பதிவுகள் ஒரு குறியைக் கொண்டுள்ளன, எந்த அளவு நம்பிக்கையுடன் எழுத முடியும் என்பதை நீங்கள் கவனிக்காத வரை.

மற்ற எல்லா கணிதப் பரிமாற்றங்களிலும் உள்ள பிரச்சனை

MathOverflow, math.StackExchange, r/math, arXiv கருத்துப் பிரிவுகள். அவை அனைத்தும் சரியானதை ஒரு தீர்ப்பாளர்: மற்றவர்கள், விவாதம். அது குறிப்பிடத்தக்க வகையில் நன்றாக வேலை செய்கிறது, மேலும் இது ஏன் தவறான நிரூபணத்தை எழுதுவது சரியானதை எழுதுவதை விட குறைவாக உள்ளது, ஏன் "நான் அதை சரிபார்த்தேன்" மற்றும் "நான் அதை நம்பினேன்" பக்கத்தில் ஒரே மாதிரியாக தோன்றுகிறது.

Halmos ஒரு இரண்டாவது ஆர்பிட்டர் சேர்க்கிறது, அது தர்க்கம் செய்ய இயலாது.

சேவையகம் உண்மையில் என்ன செய்கிறது

எந்த பதிவு அல்லது கருத்துக்கும் ஒரு சுவர் அடைவை இடவும், அது இங்கே இயங்கும், சமர்ப்பிக்கும்போது:

ஒரு தொகுதியின் கீழ் காட்டப்படும் வெளியீடு கருவி அச்சிட்டதை, முழுமையாக காட்டுகிறது. எப்போதும் சுருக்கம்: சுருக்கம் என்பது ஒரு தயாரிப்பு நுழையக்கூடிய இடத்தில் உள்ளது.

எப்படி முயற்சி, ஒரு நிமிடத்தில்

1. வழக்கமான குறிப்பு. பெரும்பாலான பதிவுகள் அவற்றில் எந்த கணிதமும் இல்லை மற்றும் இங்கே எதுவுமே தேவையில்லை. பதில்கள் நுழைவாயில்.
2. கணிதத்தை உள்ளமை உடன் $…$, அல்லது காட்சிப் பகுதி $$…$$. இது உண்மையான எழுத்துரு கணிதத்தை காட்டுகிறது; எதுவுமே செயல்படுத்தப்படவில்லை. இது குறிப்புரை மட்டுமே. ஒருவரைப் பார்
3. இயந்திரம் கேட்க. ஒரு கட்டப்பட்ட குறுக்குவழி sage, gp, z3 அல்லது python இந்த ஆவணங்கள் இங்கே செயல்படுத்தப்படுகிறது மற்றும் அதன் வெளியீடு உங்கள் பதிவு இணைக்கப்பட்டுள்ளது, வார்த்தைக்கு வார்த்தை. ஒருவரைப் பார்
4. ஏதாவது வரை ஒரு plot தொகுதி (matplotlib, with plt மற்றும் np தயாராக உள்ளது), அல்லது வரிசை அடையாளம் oeis: முழு எண்களை ஒட்டவும், அது தெரியும் என்றால், பெயர் பெற்றது.
5. ஏதாவது நிரூபிக்க. A-M_BAR_ஆங்கில மொழி lean மாத்லிப்- க்கு எதிராக வகை- சரிபார்க்கப்பட்ட தட்டு. இதை எந்த குறிப்பிலும் ஒட்டு: ஒருவரைப் பார்

```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```

பதிவு செய்வது பயனர் பெயர் மற்றும் கடவுச்சொல்லை மட்டுமே பெறுகிறது: மின்னஞ்சல் இல்லை, உறுதிப்படுத்தல் இல்லை. சரிபார்ப்பாளர்கள் செய்யும் அனைத்தும் இப்போது மின்னஞ்சல் மூலம் தான். வரிசை, மற்றும் ஒவ்வொரு சோதனையாளரின் உயிர் நிலை நிலைப் பக்கம்: ஒன்று கீழே இருந்தால் நீங்கள் "இயங்க முடியவில்லை" என்று கூறப்படும், "மறுக்கப்பட்டது" இல்லை.

உங்கள் வேகத்தில் எழுதவும்

ஒரு கட்டுரையை துவக்கு உங்கள் கணிதத்தை பார்க்க, எழுதுதல் மற்றும் முன்பார்வை இடையே மாற்றவும். மாற்றங்கள் தானாகவே சேமிக்கப்படும் உங்கள் வரைவுகள்; ஜாவாஸ்கிரிப்ட் இல்லாமல் வரைவுகளை சேமிக்கவும். வரைவுகள் மற்றும் முன்தோற்றங்கள் எப்போதும் குறியீட்டை இயக்காது. பகிர தயாராக இருக்கும் போது வெளியிடவும்.

கட்டுரையின் உள்ளடக்க பட்டியலை உருவாக்க தலைப்புகளை பயன்படுத்தவும். உள்ளீடு பட்டி வரையறைகள், தத்துவங்கள், நிரூபணங்கள், உதாரணங்கள், அட்டவணைகள் மற்றும் இணைப்புகளை சேர்க்கும். உதாரணமாக:

:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::

:::proof
Explain your argument here.
:::

ஒரு நிரூபண பெட்டி ஒரு தர்க்கத்தைக் காட்டுகிறது; ஒரு ஏற்றுக்கொள்ளப்பட்ட லியன் சோதனை உறுதிப்படுத்தல் குறியை வழங்குகிறது. மூலங்களை சேர்க்கவும் மற்றும் தனிப்பயன் LaTeX மாக்ரோஸ் தொகுப்பான் கீழே, அல்லது முன்னிருப்புகளை அமைக்கவும் உங்கள் பண்பு. ஒரு பொருளை தேர்ந்தெடு மற்றும் குறிகளை, அதனால் ஆர்வமுள்ள வாசகர்கள் உங்கள் பதிவை கண்டுபிடிக்க முடியும்.

வெளியிடப்பட்ட கட்டுரைகளுக்கு கட்டுரையை திருத்து இணைப்பு உள்ளது. நீங்கள் புதுப்பித்தலை வெளியிடும் வரை சேமிக்கப்பட்ட திருத்தங்கள் தனியாகவே இருக்கும். கட்டுரை அதன் முகவரியை வைத்திருக்கும், மற்றும் ஏற்கனவே உள்ள இயந்திர சோதனைகள் அவர்கள் சோதிக்கப்பட்ட உரையுடன் இணைக்கப்பட்டு இருக்கும்.

ஒரே நேரத்தில் வாசிக்கவும்

உங்கள் தனிப்பட்ட வாசிப்பு பட்டியலில் கட்டுரைகளை சேமிக்கவும் மற்றும் தனிப்பட்ட எழுத்தாளர்கள் அல்லது பொருள்களை பின்பற்றவும் பின்பற்றுதல் உங்கள் பதிவுகளுக்கும் கருத்துகளுக்கும் பதிலளிப்பதற்கு உங்களுக்கு பதிலளிக்கிறது.

புத்தகத்தை அல்லது தொடரை உருவாக்கு உங்கள் வெளியிடப்பட்ட கட்டுரைகளை இணைக்க. அத்தியாயங்களை சேர்க்கவும், அவற்றின் முறையை அமைக்கவும், தயாரான போது உள்ளடக்கங்களை பொதுவாக செய்யவும். தனிப்பட்ட தொகுப்பு அதன் உள்ளடக்க பட்டியலை மறைக்கவும்; அதன் கட்டுரைகள் தனியாக வெளியிடப்பட்டவையாகவே இருக்கும்.

குறி

∎ ஒரு என்று அழைக்கப்படுகிறது halmos, பாவ்ல் Halmos க்குப் பிறகு, யார் நிரூபிப்பு முடிவு குறியை அறிமுகப்படுத்தினார். இது இந்த தளத்தில் அதிகாரத்தைக் கொண்ட ஒரே விஷயம், எனவே இது கவனமாக பெறுவது கடினம்:

• லீன் மட்டுமே இதை அமைக்க முடியும். சாஜ் அச்சு True இது ஒரு சான்று, ஒரு சான்று அல்ல.
• sorry, native_decide, ஒரு புது axiom, unsafe மற்றும் debug.skipKernelTC நிராகரிக்கப்பட்டது முன் கோப்பு இயங்குகிறது, எனவே ஒரு சதி கணக்கீடு செலவு கூட செய்ய முடியாது.
• ஒரு ஓட்டம் உரை உருவாக்கியதை பொருத்து பொருத்தப்படும். கட்டுரையை திருத்தும் போது புதிய வார்த்தைகளை மாற்றுவதை விட குறியை மாற்றிவிடும்.
• ஒரு சோதனை நீங்கள் பெற வேண்டும் கீழே என்றால் "இயக்க முடியவில்லை", எப்போதும் "மறுக்கப்பட்ட". நிலையை சரிபார் அந்த காரணத்திற்காக பொதுவாக உள்ளது.

பொதுவுடைமை

உறுதிப்படுத்துதல் மலிவானது; கண்டுபிடிப்பு அல்ல. பொதுவுடைமை இது இந்த பரிந்துரைக்கு திறந்த பிரச்சனைகளை திறந்து விடுகிறது. யாரும் இதில் பங்களிக்கலாம், யாரும் முடிவுகளை சொந்தமாகக் கொண்டிருக்க முடியாது, மற்றும் ஒவ்வொரு இயக்கமும் பொதுவாக உள்ளது, எங்கும் கிடைக்காதவைகள், பொதுவாக தகவல்களைக் கொண்டவைகள் உள்ளிட்டவை.

யார் இயக்குகிறது

Halmos தனித்துவமானது மற்றும் சிறியதாக உள்ளது. இங்கே ஏதாவது தவறு இருந்தால், அதை நிரூபிக்க வேகமான வழி சேவையகம் இயக்கக்கூடிய ஒரு தடுப்பு. தொடர்பு கொள்.