ハルモス
Halmosは数学のフォーラムで、サーバが数学をチェックします。 あらゆるリンク集約者のように見えます。 あるポストが、自信を持って書くことのできないマークを持っていることに気づくまでは。
数学のフォーラムの問題は
MathOverflow、 math.StackExchange、 r/math、 arXiv コメントセクション。 すべての論文には正しい証明の仲裁者が一人だけいます。他の人が論争しています。 これは非常にうまく機能し、流暢に書かれた間違った証明が間違って書かれた正しい証明よりも高いランクを得る理由であり、「私はそれをチェックしました」と「私はそれを信じています」がページ上で同じように見える理由です。
Halmosは 2番目の仲裁者を加えた 議論できない
サーバが実際に行うこと
どのポストやコメントにもフェンスブロックを入れれば、提出時にここで実行されます:
| ブロック | 何が起きるか | それは稼げるか ∎? |
|---|---|---|
lean |
Mathlib との型チェック。カーネルが証明項を受け入れるか否か。 | はい |
sage | 実際の出力はポストにピンされています。 | いや |
gp | パーリ/GPが運営してる | いや |
z3 | Z3 looks for a model: the fastest way to 反論 何か | いや |
python | サンドボックス化された Python で、出力を添付します。 | いや |
ブロックの下に表示される出力はツールが出力したもので、文字通りです。要約はありません。要約は、製造が入り込むところです。
どうやって試すか １分で
- 普通にコメントして ほとんどのポストは数学を全く含んでいません。ここでは何も数学を必要としません。返信は巣を作ります。
- 数学をインラインで書き込む あなたは
$…$あるいは ディスプレイブロックに$$…$$. これは実際のタイプセットの数学としてレンダリングされます。何も実行されません。記号のみです。 見てみろ - マシンに聞いてみろ タグ付けされたフェンスブロック
sage,gp,z3それともpythonここで実行され 出力は あなたのポストに 文字通り付属されます 証拠ではなく証拠です 見てみろ - 何か描いて あなたは あの
plotブロック (matplotlib, with)pltそれにnpあるいは それを表す文字列をoeis整数を貼り付けると、 知られているなら名前付きで返されます。 - 証明して あなたは、私のために、あなたが私のために、あなたが私の
leanブロックは Mathlib とのタイプチェックを受けています。 コメントにこれを貼り付けてください: 見てみろ
```lean
import Mathlib
theorem two_add_two : 2 + 2 = 4 := by norm_num
```登録はユーザ名とパスワードで行います。メールや確認ステップはありません。チェッカーが今行っていることはすべて、 キュー各チェッカーのライブ状態は ステータスページ1つが落ちたら 運転できないと言われます 拒否されません
自分のペースで書く
投稿を開始 読者が見るように 数学を見るために 書き込みとプレビューを切り替えます あなたの草稿草稿を保存するには JavaScript が必要です。草稿とプレビューはコードを実行しません。共有する準備ができたら公開してください。
記事の内容を作成するには、ヘッダを使ってください。 挿入メニューは定義、定理、証明、例、表、リンクを追加します。例:
:::theorem Squares
For every real $x$, we have $x^2 \geq 0$.
:::
:::proof
Explain your argument here.
:::証明ボックスは引数を示し、認められた Lean チェックは検証マークを提供します。エディタの下にソースとカスタム LaTeX マクロを追加します。または、デフォルトを設定します。 あなたのプロフィール関心のある読者がポストを見つけられるように、テーマとタグを選択してください。
発行されたポストには ポストを編集するリンクがあります。保存された編集は更新を発行するまでプライベートになります。記事はアドレスを保持し、既存のマシンチェックはチェックしたテキストに結びついていきます。
読み続けて
個人の読み物リストにポストを保存し、個人的なフォローを行うために作者やトピックをフォローします。 フォロー あなたの投稿やコメントに対する返信は 返信.
本またはシリーズを作成 プライベートコレクションは、 内容リストを隠し、 個々のポストを公開します。
標識
∎ これは 『ア・ラ』と呼ばれます halmos証明の終了記号を導入した Paul Halmos の名前にちなんで 命名されました このサイトで唯一権威を持つものです
- リーンだけが設定できる
True証拠ではなく証拠です sorry,native_decide, あのaxiom,unsafeそれにdebug.skipKernelTC拒否される 前に ファイルは実行される だから チートは コンピュータの時間を使えない- ランは、それを生成したテキストにピンされます。ポストを編集すると、マークは新しい単語に移動する代わりに、古いものになります。
- チェックが下がったら "走れなかった"決して "拒否". チェッカーの状態 それが公開される理由です
コモンズ
検証は安価だが発見はそうではない。 コモンズ 誰でも貢献できる 誰も結果を所有しない すべての運用は公開される 情報を得るためのものも含めて
誰が運営するの？
Halmos is independent and small. If something here is wrong, the fastest way to prove it is a block the server can run. 連絡を取れ.