Mathematicians · students · physicists · computer scientists

Search. Prove.
Build on it.

Computer-verified mathematics, by just talking. Ask in plain English and get back a proof a machine has actually checked.

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.

Or try it right here

live — no account, no install

Ask me about mathematics — I search 200k+ verified results by meaning. Or press a button below and watch a real Lean verification run.

This box searches and verifies. To prove and submit your own results, sign in below and use your assistant.

Get your key in 30 seconds.

Google Sign in → get your key