Halmos — mathematics the server can check

sign in<br>sign up

New here? What this does, and how to try it

It is a link aggregator like any other — except a post or comment<br>can carry code, and the server runs it and pins the real output .<br>Sign-up is a username and a password; no email, no confirmation step.

Comment normally. Most posts have no maths in them at<br>all and nothing here requires any. Replies nest, like HN.

Write maths inline with $…$, or a<br>display block with $$…$$. It renders as real typeset maths.<br>Nothing is executed — it is just notation.<br>see one

Ask the machine. A fenced block tagged<br>sage, gp, z3 or python<br>is executed here and its output is attached to your post, verbatim. That<br>is evidence, not proof.<br>see one

Prove something. A lean block is<br>type-checked against Mathlib. If the kernel accepts it the post gets<br>∎ verified — and that mark<br>cannot be talked into existence: sorry, a fresh<br>axiom and skipped type-checking are rejected before the file<br>even runs.<br>see one

Draw something with a plot block<br>(matplotlib, plt and np ready), or identify a<br>sequence with oeis — paste the integers and it comes<br>back named, if it is known.

Watch it say no. A wrong proof is rejected with the<br>goal Lean still had open, which is the useful part.<br>see one

Paste this into a comment and it will be checked:

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

There is one queue and it is<br>public; every checker's live state is on the<br>status page — if one is down you will be told<br>&ldquo;could not run&rdquo;, never &ldquo;rejected&rdquo;.

A wrong proof, kept up on purpose: \sqrt{4} is irrational

rejected

1 point<br>by nadermx<br>17 hours ago &middot;<br>0 comments

What is the most under-appreciated theorem in your field?

1 point<br>by nadermx<br>17 hours ago &middot;<br>0 comments

Every finite division ring is commutative

∎ verified

1 point<br>by nadermx<br>20 hours ago &middot;<br>0 comments

Why \sum_{n=1}^{\infty} 1/n^2 = \pi^2/6 keeps getting new proofs

1 point<br>by nadermx<br>20 hours ago &middot;<br>4 comments

A one-line check that 2^{67}-1 is composite

ran

1 point<br>by nadermx<br>20 hours ago &middot;<br>0 comments

\sqrt{2} is irrational, and the kernel agrees

∎ verified

1 point<br>by nadermx<br>20 hours ago &middot;<br>0 comments