diff --git a/LeanBridge/Lookup/Basic.lean b/LeanBridge/Lookup/Basic.lean
new file mode 100644
index 00000000..f3927bc0
--- /dev/null
+++ b/LeanBridge/Lookup/Basic.lean
@@ -0,0 +1,358 @@
+import Mathlib
+
+/-! # `lookup` vocabulary
+
+The shared, table-agnostic pieces: the value types (`Column`, `Cond`, `Cmp`), low-level `Expr`
+matchers, the recogniser combinators for a table's columns and properties, result-row helpers,
+and `TableInfo`.
+
+The concrete tables live in `LeanBridge.Lookup.Tables`; the tactic itself in
+`LeanBridge.Lookup.Lookup`. -/
+
+open Lean Meta
+
+namespace Lookup
+
+/-! ## Literals -/
+
+/-- Extract a natural-number literal from `e`, handling `@OfNat.ofNat _ n _`. -/
+def getNatLit? (e : Expr) : Option Nat :=
+  match_expr e with
+  | OfNat.ofNat _ n _ => n.rawNatLit?
+  | _ => e.rawNatLit?
+
+/-- Extract an integer literal, handling a leading negation `@Neg.neg _ _ n`. -/
+def getIntLit? (e : Expr) : Option Int :=
+  match_expr e with
+  | Neg.neg _ _ a => (getNatLit? a).map fun n => -(n : Int)
+  | _ => (getNatLit? e).map Int.ofNat
+
+/-! ## Comparison operators -/
+
+/-- A comparison operator we know how to send to SQL. -/
+inductive Cmp | eq | ne | le | lt | ge | gt
+  deriving Inhabited, BEq
+
+namespace Cmp
+
+/-- The SQL spelling of the operator. -/
+def toSql : Cmp → String
+  | eq => "=" | ne => "<>" | le => "<=" | lt => "<" | ge => ">=" | gt => ">"
+
+/-- The operator whose truth value is the logical negation of this one. -/
+def negate : Cmp → Cmp
+  | eq => ne | ne => eq | le => gt | lt => ge | ge => lt | gt => le
+
+/-- The operator that holds after swapping the operands (equivalently, after negating both
+sides of an order comparison). -/
+def reverse : Cmp → Cmp
+  | eq => eq | ne => ne | le => ge | lt => gt | ge => le | gt => lt
+
+end Cmp
+
+/-! ## Columns and conditions -/
+
+/-- A scalar quantity: an SQL expression and a display name. `signed?` names the `(sign, abs)`
+columns for a value LMFDB stores as `sign * |·|`. `extraConds` are extra `WHERE` conjuncts the
+quantity implies, e.g. a modular space's level and weight from its `Module.finrank ℂ` type. -/
+structure Column where
+  sql : String
+  display : String
+  signed? : Option (String × String) := none
+  extraConds : Array String := #[]
+
+/-- Prefix `core` with the column's extra `WHERE` conjuncts (the object identity it implies),
+if any. -/
+def Column.withConds (c : Column) (core : String) : String :=
+  if c.extraConds.isEmpty then core
+  else s!"{String.intercalate " AND " c.extraConds.toList} AND {core}"
+
+/-- A translated SQL condition: the boolean SQL, the columns it references (as
+`(displayName, selectExpr)` pairs, for reporting), and the LMFDB table it forces. -/
+structure Cond where
+  sql : String
+  refs : Array (String × String) := #[]
+  table : Option String := none
+
+/-- Build a `Column`. -/
+def col (sql display : String) (signed? : Option (String × String) := none) : Column :=
+  { sql, display, signed? }
+
+/-- A boolean-flag condition `column = 't'` (or `column = 'f'` when negated). -/
+def boolCol (positive : Bool) (column : String) : Cond :=
+  { sql := s!"{column} = {if positive then "'t'" else "'f'"}", refs := #[(column, column)] }
+
+/-! ## Low-level `Expr` matchers -/
+
+/-- Match a comparison `Prop`, returning the operator and the two operands. -/
+def matchCmp (e : Expr) : Option (Cmp × Expr × Expr) :=
+  match_expr e with
+  | Eq _ a b => some (.eq, a, b)
+  | Ne _ a b => some (.ne, a, b)
+  | LE.le _ _ a b => some (.le, a, b)
+  | LT.lt _ _ a b => some (.lt, a, b)
+  | GE.ge _ _ a b => some (.ge, a, b)
+  | GT.gt _ _ a b => some (.gt, a, b)
+  | _ => none
+
+/-- Whether `e` mentions the constant `n` anywhere. -/
+def containsConst (e : Expr) (n : Name) : Bool := (e.find? (·.isConstOf n)).isSome
+
+/-- Read a product of cyclic groups `ZMod n₁ × ⋯ × ZMod n_k` (after stripping any
+`Multiplicative`/`Additive` wrapper) as its list of moduli, in order. A trivial factor (`ZMod 1`,
+`Unit`, `PUnit`) drops out, as LMFDB does, so the trivial group is `#[]`. -/
+partial def cyclicFactors? (e : Expr) : Option (Array Nat) :=
+  match_expr e with
+  | ZMod n => (getNatLit? n).map fun k => if k == 1 then #[] else #[k]
+  | Unit => some #[]
+  | PUnit => some #[]
+  | Multiplicative a => cyclicFactors? a
+  | Additive a => cyclicFactors? a
+  | Prod a b => do return (← cyclicFactors? a) ++ (← cyclicFactors? b)
+  | _ => none
+
+/-- LMFDB encodes the torsion structure as a brace array `{2,4}` and the ideal class group as
+a JSON bracket array `[2, 2]`. -/
+def fmtBraces (f : Array Nat) : String := "{" ++ ",".intercalate (f.toList.map toString) ++ "}"
+def fmtBrackets (f : Array Nat) : String := "[" ++ ", ".intercalate (f.toList.map toString) ++ "]"
+
+/-- The de Bruijn index of a bound variable, if `e` is one. -/
+def bvarIdx? : Expr → Option Nat
+  | .bvar n => some n
+  | _ => none
+
+/-- Recognise the commutativity predicate `∀ a b, a * b = b * a` (an abelian group), up to
+swapping the operands of the two products. -/
+def isAbelianPattern (e : Expr) : Bool :=
+  match e with
+  | .forallE _ _ (.forallE _ _ body _) _ =>
+    match_expr body with
+    | Eq _ lhs rhs =>
+      match_expr lhs with
+      | HMul.hMul _ _ _ _ l1 l2 =>
+        match_expr rhs with
+        | HMul.hMul _ _ _ _ r1 r2 =>
+          (bvarIdx? l1 == bvarIdx? r2) && (bvarIdx? l2 == bvarIdx? r1) &&
+            (bvarIdx? l1).isSome && (bvarIdx? l1 != bvarIdx? l2)
+        | _ => false
+      | _ => false
+    | _ => false
+  | _ => false
+
+/-- Translate an abelian-group-structure claim `lhs ≃ rhs` (with `rhs` a product of cyclics)
+into an invariant-factor column comparison; `positive := false` negates it (`<>`). -/
+def structCond (positive : Bool) (lhs rhs : Expr) (lhsConst : Name)
+    (column display : String) (fmt : Array Nat → String) : Option Cond := do
+  guard (containsConst lhs lhsConst)
+  let factors ← cyclicFactors? rhs
+  return { sql := s!"{column} {if positive then "=" else "<>"} '{fmt factors}'",
+           refs := #[(display, column.replace "::text" "")] }
+
+/-- Recognise an isomorphism `A ≃+ B` or `A ≃* B`, returning the equiv's head constant and the
+two sides. -/
+def matchEquiv (e : Expr) : Option (Name × Expr × Expr) :=
+  match_expr e with
+  | AddEquiv a b _ _ => some (``AddEquiv, a, b)
+  | MulEquiv a b _ _ => some (``MulEquiv, a, b)
+  | _ => none
+
+/-! ## Recogniser combinators
+
+A column recogniser is a function `Expr → Option Column`; a property recogniser is
+`Bool → Expr → Option Cond` (the `Bool` is the wanted polarity). A table lists these functions
+directly; the helpers below build the common shapes, and anything unusual is just a lambda of
+the same type. -/
+
+/-- `headIs c "col" "name"`: matches any application of the constant `c` (e.g.
+`NumberField.classNumber F`) to the column `col`, displayed as `name`. -/
+def headIs (c : Name) (sql display : String) : Expr → Option Column :=
+  fun e => if e.isAppOf c then some (col sql display) else none
+
+/-- `finrankOver R "col" "name"`: matches `Module.finrank R _` (e.g. `R = ℚ` for a number
+field's degree, `R = ℤ` for an elliptic curve's rank). -/
+def finrankOver (R : Name) (sql display : String) : Expr → Option Column :=
+  fun e => match_expr e with
+    | Module.finrank r _ _ _ _ => if r.isConstOf R then some (col sql display) else none
+    | _ => none
+
+/-- `cardMentions c "col" "name"`: matches `Nat.card t` where the type `t` mentions `c`
+(e.g. `Nat.card (AddCommGroup.torsion W.Point)`). -/
+def cardMentions (c : Name) (sql display : String) : Expr → Option Column :=
+  fun e => match_expr e with
+    | Nat.card t => if containsConst t c then some (col sql display) else none
+    | _ => none
+
+/-- `absOf c "col" "name"`: matches `|x|` where `x` is an application of `c`
+(e.g. `|NumberField.discr F|`). -/
+def absOf (c : Name) (sql display : String) : Expr → Option Column :=
+  fun e => match_expr e with
+    | abs _ _ _ x => if x.isAppOf c then some (col sql display) else none
+    | _ => none
+
+/-- `signedValue c "signCol" "absCol" "name"`: matches `c …` whose LMFDB value is split as
+`signCol * absCol` (e.g. the signed discriminant). A comparison then case-splits on the sign to
+stay index-friendly. -/
+def signedValue (c : Name) (signCol absCol display : String) : Expr → Option Column :=
+  fun e => if e.isAppOf c then
+    some (col s!"({signCol} * {absCol})" display (some (signCol, absCol))) else none
+
+/-- `cardIs "col" "name"`: matches `Nat.card G` or `Fintype.card G` to `col`. It ignores what `G`
+is, so it covers additive groups too; a group instance or another property marks this as a
+group's order. -/
+def cardIs (sql display : String) : Expr → Option Column :=
+  fun e => match_expr e with
+    | Nat.card _ => some (col sql display)
+    | Fintype.card _ _ => some (col sql display)
+    | _ => none
+
+/-- From a modular/cusp form *type* `CuspForm Γ k` / `ModularForm Γ k` with `Γ` containing a
+`CongruenceSubgroup.Gamma0 N` subterm, read `(isCuspidal, level N, weight k)`. -/
+def modularSpace? (M : Expr) : Option (Bool × Nat × Int) := do
+  let (isCusp, Γ, k) ← (match_expr M with
+    | CuspForm Γ k => some (true, Γ, k)
+    | ModularForm Γ k => some (false, Γ, k)
+    | _ => none)
+  let kLit ← getIntLit? k
+  let g ← Γ.find? (·.isAppOf ``CongruenceSubgroup.Gamma0)
+  let N ← getNatLit? g.appArg!
+  return (isCusp, N, kLit)
+
+/-- The `WHERE` conjuncts for the `mf_newspaces` row of `S_k(Γ₀(N))`: level, weight, and trivial
+character (`char_orbit_index = 1`, the `Γ₀(N)` nebentypus). -/
+def mfSpaceConds (N : Nat) (k : Int) : Array String :=
+  #[s!"level = {N}", s!"weight = {k}", "char_orbit_index = 1"]
+
+/-- Match `Module.finrank ℂ (CuspForm Γ₀(N) k)` / `(ModularForm Γ₀(N) k)` to the cuspidal or
+total dimension column of `mf_newspaces`, with level, weight and character pinned. -/
+def modularDim : Expr → Option Column := fun e =>
+  match_expr e with
+  | Module.finrank _ M _ _ _ => do
+      let (isCusp, N, k) ← modularSpace? M
+      pure { sql := if isCusp then "cusp_dim" else "mf_dim", display := "dimension",
+             extraConds := mfSpaceConds N k }
+  | _ => none
+
+/-- Match a form *type* `CuspForm Γ₀(N) k` / `ModularForm Γ₀(N) k` (e.g. a hypothesis
+`f : CuspForm Γ₀(N) k`) and pin the space's level, weight and character. Polarity is ignored: a
+type names the object rather than a refutable property. -/
+def modularSpace : Bool → Expr → Option Cond := fun _ e => do
+  let (_, N, k) ← modularSpace? e
+  some { sql := String.intercalate " AND " (mfSpaceConds N k).toList,
+         refs := #[("level", "level"), ("weight", "weight")] }
+
+/-- `flagIs c "col"`: matches any application of `c` (e.g. `IsSimpleGroup G`) to the boolean
+column `col` (`= 't'`, or `= 'f'` when negated). -/
+def flagIs (c : Name) (column : String) : Bool → Expr → Option Cond :=
+  fun pos e => if e.isAppOf c then some (boolCol pos column) else none
+
+/-- `flagCond c posSql negSql refs`: matches `c …` to `posSql` (or `negSql` when negated). Use it
+when a predicate has no boolean column but maps to a condition on existing columns (e.g.
+`NumberField.IsTotallyReal F` ↦ `r2 = 0`). `refs` lists the columns to report. -/
+def flagCond (c : Name) (posSql negSql : String) (refs : Array (String × String)) :
+    Bool → Expr → Option Cond :=
+  fun pos e => if e.isAppOf c then some { sql := if pos then posSql else negSql, refs } else none
+
+/-- Like `flagCond`, but for a *generic* `head` (e.g. `Finite`, `IsPrincipalIdealRing`) that only
+picks this table when its argument mentions `obj`. Matches `head … obj …` (e.g. `Finite W.Point`,
+`obj` the point group) to `posSql`/`negSql`. -/
+def flagCondMentions (head obj : Name) (posSql negSql : String) (refs : Array (String × String)) :
+    Bool → Expr → Option Cond :=
+  fun pos e => if e.isAppOf head && containsConst e obj then
+    some { sql := if pos then posSql else negSql, refs } else none
+
+/-- `isAbelian "col"`: matches the commutativity statement `∀ a b, a * b = b * a` to the
+boolean column `col`. -/
+def isAbelian (column : String) : Bool → Expr → Option Cond :=
+  fun pos e => if isAbelianPattern e then some (boolCol pos column) else none
+
+/-- `isoStructure equiv c "col" "name" bracketed`: matches an isomorphism `lhs ≃ (∏ ZMod nᵢ)`
+via `equiv` (``AddEquiv``/``MulEquiv``) with `lhs` mentioning `c`, and compares the invariant
+factors against `col`. `bracketed` picks the JSON `[…]` form (class group) over `{…}` (torsion). -/
+def isoStructure (equiv c : Name) (column display : String) (bracketed : Bool) :
+    Bool → Expr → Option Cond :=
+  fun pos e => do
+    let (h, a, b) ← matchEquiv e
+    guard (h == equiv)
+    structCond pos a b c column display (if bracketed then fmtBrackets else fmtBraces)
+
+/-! ## Result rows -/
+
+/-- The first returned row of an LMFDB `/sql` response, if any. -/
+def firstRow? (j : Json) : Option Json :=
+  match j.getObjVal? "rows" with
+  | .ok (.arr rs) => rs[0]?
+  | _ => none
+
+/-- Read a (text-cast) field of a row as a string. -/
+def rowStr (row : Json) (key : String) : String :=
+  (row.getObjValAs? String key).toOption.getD "?"
+
+/-- Pretty-print the integer monomial `c * x^e` (its sign is handled by the caller). -/
+def monomial (c : Int) (e : Nat) : String :=
+  if e == 0 then toString c.natAbs
+  else
+    let base := if e == 1 then "x" else s!"x^{e}"
+    if c.natAbs == 1 then base else s!"{c.natAbs}*{base}"
+
+/-- Format an LMFDB `coeffs` array (e.g. `{-1,-1,1}`, lowest degree first) as a polynomial
+in `x`, highest degree first. -/
+def formatPoly (coeffs : String) : String := Id.run do
+  let stripped := (coeffs.replace "{" "").replace "}" ""
+  let cs := (stripped.splitOn ",").filterMap String.toInt?
+  let n := cs.length
+  let mut out := ""
+  for i in [0:n] do
+    let e := n - 1 - i
+    let c := cs[e]!
+    if c == 0 then continue
+    let term := monomial c e
+    if out.isEmpty then
+      out := if c < 0 then s!"-{term}" else term
+    else
+      out := out ++ (if c < 0 then s!" - {term}" else s!" + {term}")
+  return if out.isEmpty then "0" else out
+
+/-- Append `c * mono` (with its sign) to a running sum `acc`, skipping a zero coefficient.
+`mono = ""` is the constant term. -/
+def addTerm (acc : String) (c : Int) (mono : String) : String :=
+  if c == 0 then acc
+  else
+    let mag := if mono.isEmpty then toString c.natAbs
+      else if c.natAbs == 1 then mono else s!"{c.natAbs}*{mono}"
+    acc ++ (if c < 0 then " - " else " + ") ++ mag
+
+/-- Format an LMFDB `ainvs` array `{a₁,a₂,a₃,a₄,a₆}` as the Weierstrass equation
+`y² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆`. -/
+def formatWeierstrass (ainvs : String) : String := Id.run do
+  let stripped := (ainvs.replace "{" "").replace "}" ""
+  let cs := (stripped.splitOn ",").filterMap String.toInt?
+  if cs.length != 5 then return ainvs
+  let (a1, a2, a3, a4, a6) := (cs[0]!, cs[1]!, cs[2]!, cs[3]!, cs[4]!)
+  let lhs := addTerm (addTerm "y^2" a1 "x*y") a3 "y"
+  let rhs := addTerm (addTerm (addTerm "x^3" a2 "x^2") a4 "x") a6 ""
+  return s!"{lhs} = {rhs}"
+
+/-! ## LMFDB tables -/
+
+/-- Everything needed to query one LMFDB table and recognise the Lean expressions that map into
+its columns. The concrete instances live in `LeanBridge.Lookup.Tables`. -/
+structure TableInfo where
+  /-- The SQL table name. -/
+  table : String
+  /-- The column holding the LMFDB label (selected `AS label`). -/
+  labelCol : String
+  /-- Extra SELECT fragments for the descriptive data (e.g. the defining polynomial). -/
+  descSelects : Array String
+  /-- Render the descriptive data of a result row as plain text. -/
+  describe : Json → String
+  /-- Build the LMFDB page URL from a label. -/
+  url : String → String
+  /-- SQL `ORDER BY` clause picking the "smallest"/simplest counterexample. -/
+  orderBy : String
+  /-- Recognisers for scalar quantities of this object (used inside comparisons). Each is an
+  `Expr → Option Column`; build them with `headIs`/`finrankOver`/… or write a lambda. -/
+  scalars : Array (Expr → Option Column) := #[]
+  /-- Recognisers for boolean/structure properties (the `Bool` is the wanted polarity). -/
+  props : Array (Bool → Expr → Option Cond) := #[]
+
+end Lookup
diff --git a/LeanBridge/Lookup/Demo.lean b/LeanBridge/Lookup/Demo.lean
new file mode 100644
index 00000000..f89510d0
--- /dev/null
+++ b/LeanBridge/Lookup/Demo.lean
@@ -0,0 +1,74 @@
+import LeanBridge.Lookup.Lookup
+
+open Lookup
+
+example {F : Type*} [Field F] [NumberField F]
+    (h1 : NumberField.classNumber F = 1) (h2 : Module.finrank ℚ F = 2) (h3 : 2 = 2) :
+    |NumberField.discr F| ≤ 163 := by
+  lookup
+
+example {F : Type*} [Field F] [NumberField F]
+    (h2 : Module.finrank ℚ F = 2) :
+    NumberField.classNumber F = 4 →
+      ClassGroup (NumberField.RingOfIntegers F) ≃* Multiplicative (ZMod 4) := by
+  lookup
+
+example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic]
+    (hW : 4 ≤ Nat.card (AddCommGroup.torsion W.Point)) :
+    Module.finrank ℤ W.Point ≤ 0 := by
+  lookup
+
+example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic]
+    (hW : 2 ≤ Module.finrank ℤ W.Point) :
+    Nat.card (AddCommGroup.torsion W.Point) = 1 := by
+  lookup
+
+example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic]
+    (hW : Nat.card (AddCommGroup.torsion W.Point) = 4) :
+    Nonempty (AddCommGroup.torsion W.Point ≃+ ZMod 4) := by
+  lookup
+
+example {G : Type*} [Group G] [IsSimpleGroup G] : ¬ ∀ a b : G, a * b = b * a := by
+  lookup
+
+example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic]
+    (e : AddCommGroup.torsion W.Point ≃+ ZMod 2 × ZMod 8) :
+    False := by
+  lookup
+
+example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic]
+    (e : AddCommGroup.torsion W.Point ≃+ ZMod 2 × ZMod 10) :
+    False := by
+  lookup
+
+-- modular forms: `M₂(Γ₀(11))` is nonzero (the newspace `11.2.a`), so its dimension is not `≤ 0`
+example : Module.finrank ℂ
+    (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
+      (CongruenceSubgroup.Gamma0 11)) 2) ≤ 0 := by
+  lookup
+
+-- no quadratic field is unramified at every prime: some prime ramifies
+example {F : Type*} [Field F] [NumberField F] (h : Module.finrank ℚ F = 2) :
+    Nat.card {p : PrimeSpectrum (NumberField.RingOfIntegers F) //
+      ¬ Algebra.IsUnramifiedAt ℤ p.asIdeal} = 0 := by
+  lookup
+
+example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic]
+    (hW : 2 ≤ Module.finrank ℤ W.Point) :
+    Nat.card (AddCommGroup.torsion W.Point) ≠ 1 := by
+  lookup
+
+example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic]
+    (hW : 2 ≤ Module.finrank ℤ W.Point) :
+    ¬ Nonempty (AddCommGroup.torsion W.Point ≃+ ZMod 1) := by
+  lookup
+
+example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic]
+    (hW : 2 ≤ Module.finrank ℤ W.Point) :
+    AddCommGroup.torsion W.Point ≃+ ZMod 1 := by
+  lookup
+
+example {W : WeierstrassCurve.Affine ℚ} [W.IsElliptic]
+    (hW : 2 ≤ Module.finrank ℤ W.Point) :
+    AddCommGroup.torsion W.Point ≃+ Unit := by
+  lookup
diff --git a/LeanBridge/Lookup/Lookup.lean b/LeanBridge/Lookup/Lookup.lean
new file mode 100644
index 00000000..98cdc590
--- /dev/null
+++ b/LeanBridge/Lookup/Lookup.lean
@@ -0,0 +1,213 @@
+import LeanBridge.Lookup.Tables
+import ProofWidgets.Component.HtmlDisplay
+
+/-! # The `lookup` tactic
+
+`lookup` reads the local hypotheses and the goal, translates them into a SQL query against LMFDB
+that searches for a *counterexample* (a database object that satisfies every hypothesis but
+violates the goal), and reports it if one is found. It never closes the goal: a hit shows the
+statement is false, and a miss is only evidence, since the database is not exhaustive.
+
+The vocabulary lives in `LeanBridge.Lookup.Basic` and the table registry in
+`LeanBridge.Lookup.Tables`; this file wires them into the query, the report, and the tactic. -/
+
+open Lean Elab Tactic Meta
+
+namespace Lookup
+
+initialize registerTraceClass `lookup
+
+/-! ## Querying LMFDB -/
+
+/-- Build the request body for an LMFDB `/sql` call. -/
+def sqlRequestBody (sql : String) (limit : Nat := 1000) : Json :=
+  .mkObj [("sql", toJson sql), ("limit", toJson limit)]
+
+/-- Run a SQL query against the LMFDB `/sql` endpoint and return the decoded result. -/
+def runSql (sql : String) : MetaM Json := do
+  let sqlUrl := "https://mcp.lmfdb.org/sql"
+  let curlArgs := #[
+    "-sS",
+    "-X", "POST", sqlUrl,
+    "-H", "Content-Type: application/json",
+    "-d", (sqlRequestBody sql).compress
+  ]
+  let out ← IO.Process.output { cmd := "curl", args := curlArgs }
+  if out.exitCode != 0 then
+    throwError s!"curl failed (exit {out.exitCode}): {out.stderr}"
+  let .ok result := Json.parse out.stdout
+    | throwError s!"failed to parse response:\n{out.stdout}"
+  return result
+
+/-! ## Dispatch: translating a `Prop` to a SQL condition -/
+
+/-- Find the scalar column an expression denotes, and its table, across every table's
+recognisers. -/
+def findScalar (e : Expr) : Option (Column × String) :=
+  tables.findSome? fun t => (t.scalars.findSome? (· e)).map (·, t.table)
+
+/-- A column compared against an integer literal. For a signed column (`sign * |·|`), the
+comparison case-splits on the sign to hit the indexed `abs` column instead of the non-indexable
+product. -/
+def colVsLit (c : Column) (table : String) (cmp : Cmp) (k : Int) : Cond :=
+  let core := match c.signed? with
+    | some (signCol, absCol) =>
+        s!"(({signCol} = 1 AND {absCol} {cmp.toSql} {k}) OR \
+            ({signCol} = -1 AND {absCol} {cmp.reverse.toSql} {-k}))"
+    | none => s!"{c.sql} {cmp.toSql} {k}"
+  { sql := c.withConds core, refs := #[(c.display, c.sql)], table := some table }
+
+/-- Translate a comparison `cmp a b` (column vs literal, or column vs column) into a `Cond`. -/
+def toSqlCondCmp (cmp : Cmp) (a b : Expr) : Option Cond :=
+  match findScalar a, findScalar b with
+  | some (ca, ta), some (cb, _) =>
+      some { sql := ca.withConds (cb.withConds s!"{ca.sql} {cmp.toSql} {cb.sql}"),
+             refs := #[(ca.display, ca.sql), (cb.display, cb.sql)], table := some ta }
+  | some (ca, ta), none => (getIntLit? b).map (colVsLit ca ta cmp)
+  | none, some (cb, tb) => (getIntLit? a).map (colVsLit cb tb cmp.reverse)
+  | none, none => none
+
+/-- Combine two conditions with a SQL connective, merging their refs and table. -/
+def combineCond (op : String) (a b : Cond) : Cond :=
+  { sql := s!"(({a.sql}) {op} ({b.sql}))", refs := a.refs ++ b.refs, table := a.table <|> b.table }
+
+/-- Translate a `Prop` into a SQL condition; `pos := false` translates its negation. The negation
+is pushed onto the operator, boolean value, or connective instead of an SQL `NOT (...)`, to keep
+the query index-friendly. `Not` flips polarity, `Nonempty` is transparent, `∧`/`∨` go through by
+De Morgan. -/
+partial def toCond (pos : Bool) (e : Expr) : Option Cond :=
+  match_expr e with
+  | False => some { sql := if pos then "FALSE" else "TRUE" }
+  | True => some { sql := if pos then "TRUE" else "FALSE" }
+  | Not p => toCond (!pos) p
+  | Nonempty p => toCond pos p
+  | And a b => return combineCond (if pos then "AND" else "OR") (← toCond pos a) (← toCond pos b)
+  | Or a b => return combineCond (if pos then "OR" else "AND") (← toCond pos a) (← toCond pos b)
+  | _ =>
+    match matchCmp e with
+    | some (cmp, a, b) => toSqlCondCmp (if pos then cmp else cmp.negate) a b
+    | none => tables.findSome? fun t =>
+        (t.props.findSome? (· pos e)).map fun c => { c with table := some t.table }
+
+/-- Translate a `Prop` into a SQL condition. -/
+def toSqlCond (e : Expr) : Option Cond := toCond true e
+
+/-- Translate the *negation* of a `Prop` into a SQL condition (used for the goal). -/
+def toSqlCondNeg (e : Expr) : Option Cond := toCond false e
+
+/-! ## Assembling the query and report -/
+
+/-- Deduplicate referenced quantities by their SQL expression, preserving order. -/
+def dedupRefs (refs : Array (String × String)) : Array (String × String) := Id.run do
+  let mut seen : Array String := #[]
+  let mut out : Array (String × String) := #[]
+  for (name, expr) in refs do
+    unless seen.contains expr do
+      seen := seen.push expr
+      out := out.push (name, expr)
+  return out
+
+/-- Build the counterexample query: the label, the descriptive data, and the actual values of
+every referenced quantity (cast to text, since the endpoint cannot serialise bignum columns
+directly). -/
+def buildQuery (info : TableInfo) (conds : Array String) (items : Array (String × String)) :
+    String := Id.run do
+  let mut selects : Array String := #[s!"{info.labelCol} AS label"] ++ info.descSelects
+  for i in [0:items.size] do
+    selects := selects.push s!"({items[i]!.2})::text AS c{i}"
+  let whereClause := String.intercalate " AND " conds.toList
+  return s!"SELECT {String.intercalate ", " selects.toList} FROM {info.table} \
+    WHERE {whereClause} ORDER BY {info.orderBy} LIMIT 1"
+
+/-- The "name = value" strings for the referenced quantities of a result row. -/
+def valueStrs (row : Json) (items : Array (String × String)) : Array String := Id.run do
+  let mut out : Array String := #[]
+  for i in [0:items.size] do
+    out := out.push s!"{items[i]!.1} = {rowStr row s!"c{i}"}"
+  return out
+
+open ProofWidgets in
+/-- Render a counterexample row as interactive HTML with a clickable LMFDB link. The infoview
+doesn't linkify a bare or markdown URL in `MessageData`, so we build an actual `<a>` element and
+embed it via `MessageData.ofHtml`. -/
+def reportHtml (info : TableInfo) (row : Json) (items : Array (String × String)) : Html :=
+  let label := rowStr row "label"
+  Html.element "div" #[] #[
+    .text "the statement is false, LMFDB has a counterexample.",
+    .element "br" #[] #[],
+    .text (info.describe row),
+    .element "br" #[] #[],
+    .text (", ".intercalate (valueStrs row items).toList),
+    .element "br" #[] #[],
+    .element "a" #[("href", toJson (info.url label))] #[.text s!"{label} on LMFDB"]
+  ]
+
+/-- A plain-text fallback for the counterexample, shown where HTML cannot render. -/
+def reportAlt (info : TableInfo) (row : Json) (items : Array (String × String)) : String :=
+  s!"the statement is false, LMFDB has a counterexample.\n\
+    {info.describe row}\n\
+    {", ".intercalate (valueStrs row items).toList}\n\
+    {info.url (rowStr row "label")}"
+
+/-! ## The tactic -/
+
+/-- Translate the context hypotheses into SQL conditions. If a hypothesis is a comparison we
+can't translate, warn and drop it: ignoring it silently would weaken any "no counterexample"
+conclusion. -/
+def collectHypotheses : TacticM (Array Cond) := do
+  let mut out : Array Cond := #[]
+  for ldecl in ← getLCtx do
+    if ldecl.isImplementationDetail then continue
+    let ty ← instantiateMVars ldecl.type
+    match toSqlCond ty with
+    | some s => out := out.push s
+    | none =>
+      if (matchCmp ty).isSome then
+        logWarning m!"ignoring hypothesis `{ldecl.userName}` : {ty}\n\
+          (couldn't translate it to a SQL condition, so the search ignores this constraint)."
+  return out
+
+/-- Peel leading non-dependent implications `a₁ → ⋯ → b` into the antecedents `#[a₁, …]`
+(treated as extra hypotheses) and the final consequent `b`. -/
+partial def peelImplications : Expr → Array Expr × Expr
+  | e@(.forallE _ a b _) =>
+      if b.hasLooseBVars then (#[], e)
+      else let (hyps, goal) := peelImplications b; (#[a] ++ hyps, goal)
+  | e => (#[], e)
+
+elab "lookup" : tactic => do
+  let goal ← getMainGoal
+  goal.withContext do
+    -- Treat the antecedents of an implication goal as extra hypotheses; the negated final
+    -- consequent is the condition we hunt for a row to satisfy.
+    let (antecedents, goalType) := peelImplications (← instantiateMVars (← goal.getType))
+    let some goalCond := toSqlCondNeg goalType
+      | throwError "don't know how to translate the goal into a SQL query"
+    let mut conditions ← collectHypotheses
+    for a in antecedents do
+      match toSqlCond a with
+      | some c => conditions := conditions.push c
+      | none =>
+        if (matchCmp a).isSome then
+          logWarning m!"ignoring antecedent `{a}` (couldn't translate it to a SQL condition)."
+    conditions := conditions.push goalCond
+    -- Every condition must point at the same LMFDB table.
+    let info ← match (conditions.filterMap (·.table)).toList.dedup with
+      | [t] => match tableInfo? t with
+        | some info => pure info
+        | none => throwError "no table configuration for `{t}`"
+      | [] => throwError "couldn't determine which LMFDB table the goal is about"
+      | ts => throwError "the goal mixes multiple LMFDB object types {ts}"
+    let conds := conditions.map (·.sql)
+    let items := dedupRefs (conditions.foldl (fun acc s => acc ++ s.refs) #[])
+    let query := buildQuery info conds items
+    trace[lookup] "query:\n{query}"
+    match firstRow? (← runSql query) with
+    | none =>
+      -- No counterexample in the database: report, but do *not* close the goal.
+      logInfo m!"no counterexample found in LMFDB \
+        (the statement is consistent with the database, but this is not a proof)."
+    | some row =>
+      throwError (← MessageData.ofHtml (reportHtml info row items) (reportAlt info row items))
+
+end Lookup
diff --git a/LeanBridge/Lookup/Tables.lean b/LeanBridge/Lookup/Tables.lean
new file mode 100644
index 00000000..2fca2c72
--- /dev/null
+++ b/LeanBridge/Lookup/Tables.lean
@@ -0,0 +1,168 @@
+import LeanBridge.Lookup.Basic
+
+/-! # LMFDB table registry
+
+The object families `lookup` knows about. To add a family, add a `TableInfo` here and list it in
+`tables`. To teach a family a new column or property, add a recogniser to its `scalars`/`props`
+with the combinators from `LeanBridge.Lookup.Basic`. -/
+
+open Lean
+
+namespace Lookup
+
+/-- Number fields. -/
+def nfFields : TableInfo where
+  table := "nf_fields"
+  labelCol := "label"
+  descSelects := #["coeffs::text AS coeffs"]
+  describe row := s!"number field {rowStr row "label"}, with minimal polynomial \
+    {formatPoly (rowStr row "coeffs")}"
+  url label := s!"https://www.lmfdb.org/NumberField/{label}"
+  orderBy := "disc_abs"
+  scalars := #[
+    -- `NumberField.classNumber F`  ↦  class_number
+    headIs ``NumberField.classNumber "class_number" "class number",
+    -- `Module.finrank ℚ F`  ↦  degree
+    finrankOver ``Rat "degree" "degree",
+    -- `|NumberField.discr F|`  ↦  disc_abs
+    absOf ``NumberField.discr "disc_abs" "|discriminant|",
+    -- `NumberField.discr F`  ↦  disc_sign · disc_abs  (signed, sign-split on comparison)
+    signedValue ``NumberField.discr "disc_sign" "disc_abs" "discriminant",
+    -- `NumberField.rootDiscr F`  ↦  rd
+    headIs ``NumberField.rootDiscr "rd" "root discriminant",
+    -- `NumberField.Units.regulator F`  ↦  regulator
+    headIs ``NumberField.Units.regulator "regulator" "regulator",
+    -- `NumberField.Units.torsionOrder F`  ↦  torsion_order (number of roots of unity)
+    headIs ``NumberField.Units.torsionOrder "torsion_order" "number of roots of unity",
+    -- `NumberField.InfinitePlace.nrComplexPlaces F`  ↦  r2
+    headIs ``NumberField.InfinitePlace.nrComplexPlaces "r2" "number of complex places",
+    -- `Nat.card {p // ¬ Algebra.IsUnramifiedAt ℤ p}`  ↦  num_ram: the prime ideals at which
+    -- `F` is not unramified, i.e. the ramified primes.
+    (fun e => match_expr e with
+      | Nat.card t =>
+          if containsConst t ``Algebra.IsUnramifiedAt && containsConst t ``Not then
+            some (col "num_ram" "number of ramified primes")
+          else none
+      | _ => none)]
+  props := #[
+    -- `ClassGroup (𝓞 F) ≃* Multiplicative (∏ ZMod nᵢ)`  ↦  class_group = [n₁, …]
+    isoStructure ``MulEquiv ``ClassGroup "class_group::text" "class group" true,
+    -- additive spelling: `Additive (ClassGroup (𝓞 F)) ≃+ (∏ ZMod nᵢ)`  ↦  class_group = [n₁, …]
+    isoStructure ``AddEquiv ``ClassGroup "class_group::text" "class group" true,
+    -- `NumberField.IsCMField F`  ↦  cm = 't'
+    flagIs ``NumberField.IsCMField "cm",
+    -- `IsGalois ℚ F`  ↦  is_galois = 't'
+    flagIs ``IsGalois "is_galois",
+    -- `IsAbelianGalois ℚ F`  ↦  gal_is_abelian = 't'
+    flagIs ``IsAbelianGalois "gal_is_abelian",
+    -- `NumberField.IsTotallyReal F`  ↦  no real-place column: r2 = 0
+    flagCond ``NumberField.IsTotallyReal "r2 = 0" "r2 <> 0" #[("r2", "r2")],
+    -- `NumberField.IsTotallyComplex F`  ↦  r1 = 0, i.e. degree = 2·r2 (no r1 column)
+    flagCond ``NumberField.IsTotallyComplex "degree = 2 * r2" "degree <> 2 * r2"
+      #[("degree", "degree"), ("r2", "r2")],
+    -- `Algebra.IsQuadraticExtension ℚ F`  ↦  degree = 2
+    flagCond ``Algebra.IsQuadraticExtension "degree = 2" "degree <> 2" #[("degree", "degree")],
+    -- `IsPrincipalIdealRing (𝓞 F)`  ↦  class_number = 1  (trivial class group)
+    flagCondMentions ``IsPrincipalIdealRing ``NumberField.RingOfIntegers
+      "class_number = 1" "class_number <> 1" #[("class_number", "class_number")]]
+
+/-- Elliptic curves over `ℚ`. -/
+def ecCurvedata : TableInfo where
+  table := "ec_curvedata"
+  labelCol := "lmfdb_label"
+  descSelects := #["ainvs::text AS ainvs"]
+  describe row := s!"elliptic curve {rowStr row "label"}: {formatWeierstrass (rowStr row "ainvs")}"
+  -- LMFDB EC labels like `15.a2` live at `.../EllipticCurve/Q/15/a/2`.
+  url label :=
+    match label.splitOn "." with
+    | [conductor, iso] =>
+        s!"https://www.lmfdb.org/EllipticCurve/Q/{conductor}/\
+          {iso.takeWhile Char.isAlpha}/{iso.dropWhile Char.isAlpha}"
+    | _ => s!"https://www.lmfdb.org/EllipticCurve/Q/{label}"
+  orderBy := "conductor"
+  scalars := #[
+    -- `Module.finrank ℤ W.Point`  ↦  rank
+    finrankOver ``Int "rank" "rank",
+    -- `Nat.card (AddCommGroup.torsion W.Point)`  ↦  torsion
+    cardMentions ``AddCommGroup.torsion "torsion" "torsion",
+    -- `WeierstrassCurve.j W`  ↦  jinv  (model-independent, so exact)
+    headIs ``WeierstrassCurve.j "jinv" "j-invariant"]
+  props := #[
+    -- `AddCommGroup.torsion W.Point ≃+ (∏ ZMod nᵢ)`  ↦  torsion_structure = {n₁, …}
+    isoStructure ``AddEquiv ``AddCommGroup.torsion "torsion_structure" "torsion structure" false,
+    -- `Finite W.Point`  ↦  rank = 0  (Mordell-Weil group finite ⟺ rank zero)
+    flagCondMentions ``Finite ``WeierstrassCurve.Affine.Point "rank = 0" "rank <> 0"
+      #[("rank", "rank")],
+    -- `IsAddTorsionFree W.Point`  ↦  torsion = 1
+    flagCondMentions ``IsAddTorsionFree ``WeierstrassCurve.Affine.Point "torsion = 1" "torsion <> 1"
+      #[("torsion", "torsion")]]
+
+/-- Finite groups. -/
+def gpsGroups : TableInfo where
+  table := "gps_groups"
+  labelCol := "label"
+  descSelects := #["tex_name::text AS tex_name"]
+  describe row := s!"group {rowStr row "label"} ({rowStr row "tex_name"})"
+  url label := s!"https://www.lmfdb.org/Groups/Abstract/{label}"
+  -- `order` is a SQL reserved word, so it must be quoted.
+  orderBy := "\"order\""
+  scalars := #[
+    -- `Monoid.exponent G`  ↦  exponent
+    headIs ``Monoid.exponent "exponent" "exponent",
+    -- `Group.nilpotencyClass G`  ↦  nilpotency_class
+    headIs ``Group.nilpotencyClass "nilpotency_class" "nilpotency class",
+    -- `Group.rank G`  ↦  rank (minimal number of generators)
+    headIs ``Group.rank "rank" "rank",
+    -- `Nat.card (Subgroup.center G)`  ↦  center_order
+    cardMentions ``Subgroup.center "center_order" "order of the center",
+    -- `Nat.card (ConjClasses G)`  ↦  number_conjugacy_classes
+    cardMentions ``ConjClasses "number_conjugacy_classes" "number of conjugacy classes",
+    -- `Nat.card (MulAut G)`  ↦  aut_order
+    cardMentions ``MulAut "aut_order" "order of the automorphism group",
+    -- `Nat.card G` / `Fintype.card G`  ↦  order  (generic cardinality; last, so the
+    -- `cardMentions` recognisers above claim the cardinalities of named subobjects first)
+    cardIs "\"order\"" "order"]
+  props := #[
+    -- `IsSimpleGroup G`  ↦  simple = 't'
+    flagIs ``IsSimpleGroup "simple",
+    -- `∀ a b : G, a * b = b * a`  ↦  abelian = 't'
+    isAbelian "abelian",
+    -- a `CommGroup G` / `AddCommGroup G` hypothesis  ↦  abelian = 't'
+    flagIs ``CommGroup "abelian",
+    flagIs ``AddCommGroup "abelian",
+    -- `Group.IsNilpotent G`  ↦  nilpotent = 't'
+    flagIs ``Group.IsNilpotent "nilpotent",
+    -- `Group.IsPerfect G`  ↦  perfect = 't'
+    flagIs ``Group.IsPerfect "perfect",
+    -- `IsCyclic G`  ↦  cyclic = 't'  (generic head, but no other table recognises `IsCyclic`)
+    flagIs ``IsCyclic "cyclic",
+    -- `IsSolvable G`  ↦  solvable = 't'
+    flagIs ``IsSolvable "solvable"]
+
+/-- Spaces of classical modular forms `S_k(Γ₀(N))` / `M_k(Γ₀(N))`. Level and weight come from the
+form type `CuspForm Γ k` / `ModularForm Γ k` (`Γ = Γ₀(N)`) inside a `Module.finrank ℂ …`; see
+`modularDim`. -/
+def mfNewspaces : TableInfo where
+  table := "mf_newspaces"
+  labelCol := "label"
+  descSelects := #["level::text AS level", "weight::text AS weight",
+                   "cusp_dim::text AS cusp_dim", "mf_dim::text AS mf_dim"]
+  describe row := s!"space of level {rowStr row "level"}, weight {rowStr row "weight"} \
+    (cuspidal dimension {rowStr row "cusp_dim"}, total dimension {rowStr row "mf_dim"})"
+  -- LMFDB newspace labels `23.2.a` live at `.../holomorphic/23/2/a`.
+  url label := s!"https://www.lmfdb.org/ModularForm/GL2/Q/holomorphic/{label.replace "." "/"}"
+  orderBy := "level"
+  scalars := #[
+    -- `Module.finrank ℂ (CuspForm Γ₀(N) k)` ↦ cusp_dim,  `(ModularForm …)` ↦ mf_dim
+    modularDim]
+  props := #[
+    -- a `CuspForm Γ₀(N) k` / `ModularForm Γ₀(N) k` type ↦ level = N AND weight = k AND trivial char
+    modularSpace]
+
+/-- All supported object families. To support a new one, add its `TableInfo` here. -/
+def tables : Array TableInfo := #[nfFields, ecCurvedata, gpsGroups, mfNewspaces]
+
+/-- The table configuration for a table name. -/
+def tableInfo? (name : String) : Option TableInfo := tables.find? (·.table == name)
+
+end Lookup