Tentang Halmos

Halmos adalah papan untuk matematik di mana pelayan menyemak matematik. Ia kelihatan seperti agregator pautan mana-mana sehingga anda menyedari bahawa beberapa post mempunyai tanda tiada jumlah penulisan yang yakin boleh menghasilkan.

Masalah dengan setiap forum matematik lain

MathOverflow, math.StackExchange, r/math, bahagian komen arXiv. Semuanya mempunyai satu penilai kebenaran: orang lain, berhujah. Ia berfungsi dengan baik, dan juga sebab bukti salah yang ditulis dengan lancar melebihi bukti yang betul yang ditulis dengan buruk, dan sebab "saya periksa" dan "saya percaya" kelihatan sama pada halaman.

Halmos menambahkan arbiter kedua yang tidak boleh dipertikaikan.

Apa yang pelayan sebenarnya lakukan

Letak blok pagar dalam sebarang posting atau komen dan ia akan berjalan di sini, pada penyerahan:

Blok	Apa yang berlaku	Bolehkah ia memperoleh ∎?
`lean`	Diuji jenis dengan Mathlib. Kernel menerima istilah bukti atau ia tidak.	Ya
`sage`	SageMath menjalankannya; output sebenar dipin pada post.	Tidak
`gp`	PARI/GP yang menjalankannya.	Tidak
`z3`	Z3 mencari model: cara terpantas untuk tolak sesuatu.	Tidak
`python`	Python sandboxed, output dilampirkan.	Tidak

Output yang dipaparkan di bawah blok adalah apa yang alat cetak, secara bertulis. Tidak pernah ringkasan: ringkasan adalah tepat di mana pembuatan akan terselit.

Bagaimana untuk mencuba ia, dalam masa sebentar

Komen seperti biasa. Kebanyakan post tidak mempunyai matematik dalam mereka sama sekali dan tiada apa-apa di sini memerlukan apa-apa.
Tulis matematik dalam baris dengan $…$ , atau blok paparan dengan $$…$$. Ianya dihasilkan sebagai matematik set aksara sebenar; tiada apa yang dilaksanakan. Ia hanya nota. lihat satu
Tanya mesin. Blok tertutup yang ditanda sage, gp, z3 atau python Ia dilaksanakan di sini dan outputnya disambungkan ke post anda, secara bertulis. lihat satu
Lukis sesuatu dengan plot blok (matplotlib, dengan plt dan np sedia), atau mengenal pasti rentetan dengan oeis: tampal integer dan ia akan kembali dengan nama, jika ia diketahui.
Buktikan sesuatu. A-M_BAR_Arab lean blok telah diuji jenisnya terhadap Mathlib. Tampal ini ke dalam sebarang komen: lihat satu

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

Mendaftar adalah nama pengguna dan kata laluan: tiada emel, tiada langkah pengesahan. Semua yang periksa lakukan sekarang adalah pada baris gilir, dan setiap periksa keadaan hidup adalah pada status page: jika satu di bawah anda diberitahu "tidak boleh berjalan", tidak pernah "ditolak".

Tulis pada kelajuan anda sendiri

Mulakan artikel dan beralih antara menulis dan pralihat untuk melihat matematik anda seperti yang akan dilihat oleh pembaca. Perubahan disimpan secara automatik ke Draf anda; Simpan draf juga berfungsi tanpa JavaScript. Draf dan pralihat tidak pernah menjalankan kod. Terbitkan bila anda bersedia untuk berkongsi.

Gunakan tajuk untuk membina senarai kandungan artikel. Menu Selit menambah definisi, teorema, bukti, contoh, jadual dan pautan. Sebagai contoh:

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

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

Kotak bukti memperlihatkan hujah; semakan Lean yang diterima memberikan tanda pengesahan. Tambah sumber dan makro LaTeX tersendiri di bawah editor, atau tetapkan piawai dalam profil andaPilih subjek dan tag supaya pembaca yang berminat boleh mencari artikel anda.

Artikel yang diterbitkan mempunyai pautan Edit artikel. Edit yang disimpan tetap peribadi sehingga anda menerbitkan kemaskini. Artikel menyimpan alamatnya, dan semakan mesin sedia ada tetap terikat kepada teks yang mereka semak.

Teruskan membaca bersama-sama.

Simpan artikel ke senarai bacaan peribadi anda dan ikut penulis atau topik untuk peribadi Mengikut suapan. Balasan kepada posting dan komen anda muncul dalam Balas kepada anda.

Cipta buku atau siri untuk menyambungkan artikel yang diterbitkan. Tambah bab, susun atur urutannya, dan buat kandungannya awam bila sedia. Koleksi peribadi menyembunyikan senarai kandungannya; artikelnya tetap diterbitkan secara individu.

Tanda

∎ dipanggil halmos, selepas Paul Halmos, yang memperkenalkan simbol akhir- bukti. Ia satu- satunya perkara di laman ini yang membawa kuasa, jadi ia sengaja sukar untuk mendapatkan:

Hanya Lean boleh tetapkannya. True Ini bukti, bukan bukti.
sorry, native_decide, segar axiom, unsafe dan debug.skipKernelTC ditolak sebelum fail berjalan, jadi penipuan tidak boleh menghabiskan komputasi.
Jalankan dipinjamkan kepada teks yang tepat yang menghasilkannya. Edit artikel dan tanda akan menjadi usang berbanding dipindahkan ke perkataan baru.
Jika seorang periksa adalah di bawah anda mendapat "tidak dapat dilaksanakan", tidak pernah "ditolak". Status Pemeriksa adalah awam untuk sebab itu.

The Commons

Pengesahan murah, penemuan tidak. The Commons adalah kolam komputasi berkongsi yang memotong masalah terbuka yang telah diluluskan oleh papan ini. Sesiapa sahaja boleh menyumbang kepadanya, tiada siapa yang mempunyai hasil, dan setiap pelaksanaan ia adalah dana awam, termasuk yang tidak mendapat tempat, yang biasanya yang bermaklumat.

Siapa yang mengendalikannya?

Halmos adalah bebas dan kecil. Jika sesuatu di sini salah, cara terpantas untuk membuktikan ia adalah blok pelayan boleh berjalan. Dapatkan dalam hubungan.