About 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.

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.