Sou Halmos

Halmos is a board for mathematics where the server checks the mathematics. It looks like any link aggregator until you notice that some posts carry a mark no amount of confident writing can produce.

The problem with every other maths forum

MathOverflow, math.StackExchange, r/math, the arXiv comment sections — all of them have exactly one arbiter of correctness: other people, arguing. That works remarkably well, and it is also why a wrong proof written fluently outranks a right one written badly, and why "I checked it" and "I believe it" look identical on the page.

Halmos adds a second arbiter that cannot be argued with.

What the server actually does

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

Block	What happens	Can it earn ∎?
`lean`	Type-checked against Mathlib. The kernel accepts the proof term or it does not.	Yes
`sage`	SageMath runs it; the real output is pinned to the post.	No
`gp`	PARI/GP runs it.	No
`z3`	Z3 looks for a model — the fastest way to refute something.	No
`python`	Sandboxed Python, output attached.	No

The output shown under a block is what the tool printed, verbatim. Never a summary — summarising is exactly where a fabrication would slip in.

How to try it, in about a minute

Comment normally. Most posts have no maths in them at all and nothing here requires any. Replies nest.
Write maths inline with $…$ , or a display block with $$…$$. It renders as real typeset maths; nothing is executed — it is just notation. see one
Ask the machine. A fenced block tagged sage, gp, z3 or python is executed here and its output attached to your post, verbatim. That is evidence, not proof. see one
Draw something with a plot block (matplotlib, with plt and np ready), or identify a sequence with oeis — paste the integers and it comes back named, if it is known.
Prove something. A lean block is type-checked against Mathlib. Paste this into any comment: see one

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

Signing up is a username and a password — no email, no confirmation step. Everything the checkers are doing right now is on the queue, and each checker's live state is on the status page: if one is down you are told “could not run”, never “rejected”.

Write at your own pace

Start a post and switch between writing and preview to see your mathematics as readers will. Changes save automatically to Your drafts; Save draft also works without JavaScript. Drafts and previews never run code. Publish when you are ready to share.

Use headings to build an article's contents list. The Insert menu adds definitions, theorems, proofs, examples, tables, and links. For example:

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

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

A proof box presents an argument; an accepted Lean check supplies the verification mark. Add sources and custom LaTeX macros beneath the editor, or set defaults in your profile. Choose a subject and tags so interested readers can find your post.

Published posts have an Edit post link. Saved edits remain private until you publish the update. The article keeps its address, and existing machine checks stay tied to the text they checked.

Keep reading together

Save posts to your private reading list and follow authors or topics for a personal Following feed. Replies to your posts and comments appear in Replies to you.

Create a book or series to connect your published posts. Add chapters, arrange their order, and make the contents public when ready. A private collection hides its contents list; its posts remain published individually.

The mark

∎ is called a 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 and debug.skipKernelTC are rejected before the file runs — a cheat cannot even spend compute.
A run is pinned to the exact text that produced it. Edit the post and the mark goes stale rather than transferring to new words.
If a checker is down you get "could not run", never "rejected". Checker status 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 is independent and small. If something here is wrong, the fastest way to prove it is a block the server can run. Get in touch.