About Halmos

Halmos არის მათემატიკის ბლოკი, სადაც სერვერი მოწესრიგებს მათემატიკას. იგი გამოიყურება როგორც ნებისმიერი ბმულების აგენერატორი, სანამ არ შეამჩნევთ, რომ ზოგიერთი პოსტი ატარებს ნიშნს, რომ არანაირი დადასტურებული წერის რაოდენობა არ შეიძლება.

The problem with every other maths forum

MathOverflow, math.StackExchange, r/math, arXiv კომენტარების სექციები. ყველა მათგანს აქვს ზუსტად ერთი მართებულობის არბიტრი: სხვა ადამიანები, რომლებიც ირწმუნებიან. ეს შესანიშნავად მუშაობს და სწორედ ამიტომაცაა, რომ სწორად დაწერილი არასწორი დასკვნა უკეთესია, ვიდრე ცუდად დაწერილი სწორი და რატომაც "მე შევადარე" და "მე მჯერა" გვერდზე იდენტურია.

Halmos adds a second arbiter that cannot be argued with.

რას აკეთებს სერვერი

Put a fenced block in any post or comment and it runs here, on submission:

გამონატანი ბლოკის ქვეშ არის ის, რაც ხელსაწყომ გამოსცა. არასდროს არ არის რეზიუმე: რეზიუმეს დაწერა სწორედ იქ ხდება, სადაც ფუნდამენტური ცვლილებები უნდა მოხდეს.

How to try it, in about a minute

1. Comment normally. Most posts have no maths in them at all and nothing here requires any. Replies nest.
2. მათემატიკის ჩაწერა ხაზში რითაც $…$, ან დისპლეის ბლოკი $$…$$. ის ნამდვილი ტიპოგრაფიული რიცხვების სახით იშლება; არაფერი არ მოქმედებს. ეს მხოლოდ ნოტაციაა. see one
3. ოთრაი მაქთნარა. ბლოკი sage, gp, z3 ან python is executed here and its output attached to your post, verbatim. That is evidence, not proof. see one
4. Draw something with a plot ბლოკი (matplotlib, შიდა plt და np მზად არის, ან იპოვეთ რიგი oeis: თავსებადი მთლიანი რიცხვები და ის დაბრუნდება სახელით, თუ ის ცნობილია.
5. Prove something. ა lean ბლოკი Mathlib- ში ტიპის შეფასებას ექვემდებარება. ეს კომენტარებში ჩასვით: see one

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

რეგისტრაცია არის მომხმარებლის სახელი და პაროლი: არა ელფოსტა, არა დადასტურების ნაბიჯი. ყველა, რასაც მოწმეები აკეთებენ ახლა, არის ვებგვერდზე რიგი, and each checker's live state is on the სტატუსის გვერდი: if one is down you are told "could not run", never "rejected".

Write at your own pace

სტატიის დაწყება და გადართვა ჩაწერისა და წინასწარ ნახვის შორის, რათა ნახოთ თქვენი მათემატიკა ისევე როგორც მკითხველები. ცვლილებების ავტომატური შენახვა თქვენი შაბლონები; შაბლონის შენახვა მუშაობს JavaScript- ის გარეშეც. შაბლონები და წინასწარ ნახვა არასდროს ახორციელებენ კოდს. გამოქვეყნება, როდესაც გაზიარებას აპირებთ.

სტატიის შინაარსის შესაქმნელად გამოიყენეთ სათაურები. ჩასმა მენიუს დამატება განსაზღვრება, თეორიები, დადასტურებები, მაგალითები, ცხრილები და ბმულები. მაგალითად:

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

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

მოდიფიკატორის ყუთი წარმოადგენს არგუმენტს; მიღებული Lean- ის ჭერი იძლევა დადასტურების ნიშანს. წყაროების და LaTeX- ის ინდივიდუალური მაკროების დამატება რედაქტორის ქვეშ, ან ნაგულისხმევი პარამეტრების დაყენება თქვენი პროფილი. Choose a subject and tags so interested readers can find your post.

გამოქვეყნებულ სტატიებს აქვთ სტატიის რედაქტირების ბმული. შენახული რედაქტირება რჩება პირადი, სანამ არ გამოაქვეყნებთ განახლებას. სტატიამ იცავს მის მისამართს და არსებული მანქანის შემოწმებები რჩება დაკავშირებული ტექსტი, რომელიც მათ შემოწმდა.

Keep reading together

Save posts to your private reading list and follow authors or topics for a personal შემდეგი ჟურნალი. პასუხები თქვენს პოსტებსა და კომენტარებს მოჰყვება Replies to you.

წიგნის ან სერიის შექმნა თქვენი გამოქვეყნებული სტატიების დაკავშირება. დააწკაპუნეთ აქ რომ დააკავშიროთ თქვენი გამოქვეყნებული სტატიები. დააწკაპუნეთ აქ რომ დააკავშიროთ თქვენი გამოქვეყნებული სტატიები. დააწკაპუნეთ აქ რომ დააკავშიროთ თქვენი გამოქვეყნებული სტატიები.

The mark

∎ ჟვ ნაპთფა halmos, after Paul Halmos, who introduced the end-of-proof symbol. It is the only thing on this site that carries authority, so it is deliberately hard to get:

• Only Lean can set it. Sage printing True is evidence, not a proof.
• sorry, native_decide, a fresh axiom, unsafe და debug.skipKernelTC აკრძალულია წინა the file runs, so a cheat cannot even spend compute.
• წარმართვა დაკავშირებულია იმ ტექსტთან, რომელმაც ის შექმნა. სტატიის რედაქტირება და ნიშნის გაქრობა, ახალი სიტყვების გადატანის ნაცვლად.
• If a checker is down you get "ვერ ვახერხებ გაშვებას", never "უარყოფილია". სტატუსის შემოწმება is public for that reason.

The Commons

Verification is cheap; discovery is not. The Commons is a shared pool of compute that grinds on the open problems this board has voted up. Anyone can contribute to it, nobody owns the result, and every run it funds is public, including the ones that got nowhere, which are usually the informative ones.

Who runs it

Halmos არის დამოუკიდებელი და მცირე. თუ აქ რაღაცა არასწორია, ყველაზე სწრაფი გზაა იმის დადასტურება, რომ სერვერმა ბლოკი შეიძლება განახორციელოს. ჟგყპზთ ჟვ ჟ მვნ.