Халмосов туралы

Halmos - бұл математикалық сервері бар математикалық форум. Ол сілтемелер жинақтаушысы сияқты көрінеді, бірақ кейбір мақалаларда "өзіңізге сенімділікпен жазуға болмайды" деген белгісі бар.

Математика форумының барлық басқа форумдарындағы проблема

MathOverflow, math. StackExchange, r/ math, arXiv пікірлер бөлімдері. Олардың барлығының дұрыстығын тек бір ғана адам анықтайды: басқа адамдар, пікірлесу. Бұл өте жақсы жұмыс істейді, және осы себепті дұрыс емес дәлелдеу дұрыс емес дәлелдеуден жоғары орын алады, және "Мен тексердім" мен "Мен оған сендім" дегендер бетте бірдей көрінеді.

Halmos - екінші арбитрді қосады, олмен таласуға болмайды.

Сервердің шынайы істегені

Барлық мақала не пікірлерге қоршау блокты қойып, жіберген кезде ол мұнда орындалады:

Блоктың астында көрсетілген шығыс құралдың шығарған нәтижесі. Ешқашан тұжырымдама: тұжырымдама деген - бұл түпнұсқаның түпнұсқасы.

Оны қалай сынап көруге болады, шамамен бір минутта

1. Түсініктеме қалыпты. Мақалалардың көпшілігінде математикалық есеп жоқ, және мұнда да математикалық есеп қажет емес. Жауаптары бір- біріне еніп кетеді.
2. Математикалық амалдарды жолға жазу келесімен $…$, немесе келесімен көрсетілетін блок $$…$$. Бұл шын математикалық таңбалау жүйесіндегідей көрсетіледі, ештеңе орындалмайды. Бұл тек жазу ғана. бір
3. Машинадан сұра. Тегтелмеген қоршалған блок sage, gp, z3 немесе python Бұл команда орындалып, оның шығысы мақалаңызға тіркеліп, сөзбе- сөз жазылады. Бұл дәлел емес, дәлелдеу. бір
4. Нені болса да салу келесімен plot блок (matplotlib, онымен plt және np дайын), немесе келесі арқылы тізбекті анықтау oeis: бүтін сандарды қойып, егер белгілі болса, атауымен қайтарады.
5. Бірдеңе дәлелдеу. А- М 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, дәлелдеудің соңы белгісін енгізген Paul Halmos дегеннің құрметіне. Бұл сайтта тек қана бұл белгі ғана авторитеттік, сондықтан оны табу қиын:

• Оны тек Lean орната алады. Sage басып шығару True бұл дәлел емес, дәлелдеу.
• sorry, native_decide, жаңа axiom, unsafe және debug.skipKernelTC қабылданбады алдында файл орындалады, сондықтан жымқыру есептеу уақытын да жұмсамайды.
• Жүргізу нәтижесінде шыққан мәтінге арналады. Мақаланы өзгерткенде, жаңа сөздерге ауыстырылмай, белгілеу ескірген болып қалады.
• Егер шашка төмен болса, сіз "орындалмады", ешқашан "қабылданбады". Күй- жайын тексеру осы себепті ашық.

Қоғамдық

Тексеру арзан, ал ашу арзан емес. Қоғамдық бұл осы кеңестің шешімін күтіп тұрған ашық мәселелерді шешетін ортақ есептеу қоры. Оған кез келген адам үлес қоса алады, нәтижеге ешкім иелік етпейді, және әрбір орындау қаржысы ашық, тіпті ештеңе шешілмеген, әдетте ақпараттық, орындаулар да.

Оны кім орындайды

Halmos деген бөлек және кішірек. Егер мұнда бірдеңе дұрыс емес болса, оны дәлелдеудің ең жылдам жолы - сервер орындайтын блок. Қосылым.