Համակարգչային խաղեր

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-ը անկախ և փոքր է։ Եթե այստեղ ինչ-որ բան սխալ է, ապա դրա ապացուցման ամենաարագ միջոցը սերվերի կողմից ընթացիկ բլոկն է։ Համագործակցել.