For mathematicians, students & the curious

Ask anything.
Get a checked answer.

Not a chatbot guessing. Every answer is searched against formalized mathematics and compiled by the Lean 4 kernel.

  • Ask in plain English. You don't need the name of a theorem.
  • It says no. A false claim is rejected, not dressed up.
  • No account, no install. Start typing — that's it.
lemmahub · live lean 4 · mathlib
Hi — ask me anything about mathematics. I search 200k+ formalized results and run a real verifier, then answer in your language. Try one below, or type your own.

searches & verifies free · get a key to submit your own proofs

202,827formalized results (mathlib)
Lean 4compiles every proof
0unchecked steps
verifier · session open lean 4 · mathlib

“Prove that the product of two consecutive integers is even.”

n(n+1) — 4 steps, each one checked

checking… verified ✓

“Prove that n = n + 1.”

no derivation exists — submission rejected

checking… rejected ✗

Search

meaning, not keywords

Ask in your own words. You don't need the name of a theorem to find the result that already exists.

“Is there already a result about the sum of the first n odd numbers?” → ∑ (2i − 1) = n² · mathlib
“What's known about the smallest eigenvalue of a graph Laplacian?” → 12 results · λ₁ ≥ 0, connectivity, Cheeger

Prove

wrong · incomplete · meaningless → rejected

You ask in English. What comes back is compiled Lean 4, not plausible-sounding text. If one step fails, nothing passes.

-- "the product of two consecutive integers is even"
theorem even_mul_succ_self (n : ℤ) : Even (n * (n + 1)) := by
  rcases Int.even_or_odd n with h | h
  · exact h.mul_right _
  · exact (Int.even_add_one.mpr (Int.not_even_iff_odd.mpr h)).mul_left _

✓ compiled · 0 errors · 0 sorry
  axioms: propext, Classical.choice, Quot.sound

Build on it

yours, and everyone else's

Every lemma you submit becomes a reusable block. Even an unproven conjecture can be posted — anything resting on it stays marked conditional until it's proved.

★ your_lemma — cited by 2 results

Attribution is mechanical, not declared. The graph knows who builds on what, and says so.

your_lemma their_lemma conjecture your_new_result conditional until proved

Want it inside your editor?

Google Sign in  →  get your key

Takes about 30 seconds, and hands you a ready-to-paste setup for Claude Code · Cursor · VS Code · OpenAI's SDK — any MCP client. You only need this to submit your own proofs — searching and verifying on this page need no account at all.