update to lean_finder_v1_updated endpoint, UI change

.gitignore

@@ -0,0 +1,6 @@
+.env
+__pycache__/
+*.pyc
+.venv/
+venv/
+.DS_Store

README.md

@@ -14,3 +14,8 @@ short_description: Code search for Lean 4
 Check out the configuration reference at https://huggingface.co/docs/hub/spaces-config-reference
 
 arxiv.org/abs/2510.15940
+
+## Acknowledgements
+
+Lean Finder is built on open-source projects like [Jixia](https://github.com/frenzymath/jixia) and [LeanDojo](https://github.com/lean-dojo/leandojo). We were inspired by [LeanSearch](https://leansearch.net/), and we use LeanSearch in our Arena mode to let users compare results. Thanks to the creators of these awesome tools!
+

app.py

@@ -1,1186 +1,1412 @@
-import os, json, datetime, threading, requests, random, re, html
+import os, json, datetime, threading, requests, random, html, time
 from typing import List, Dict, Any
+
 import gradio as gr
 import gspread
 from google.oauth2.service_account import Credentials
 from gspread.exceptions import WorksheetNotFound
-import time
+try:
+    from dotenv import load_dotenv
+    load_dotenv()
+except ImportError:
+    pass  # In deployment the env vars are already set
 
 ENDPOINT_ID_A = os.getenv("ENDPOINT_ID_A")
 ENDPOINT_ID_B = os.getenv("ENDPOINT_ID_B")
-HF_TOKEN    = os.getenv("HF_TOKEN")
+HF_TOKEN = os.getenv("HF_TOKEN", "")
 SERVICE_ACCOUNT_INFO = os.getenv("GCP_SERVICE_ACCOUNT_JSON")
+
 SCOPES = [
     "https://www.googleapis.com/auth/spreadsheets",
     "https://www.googleapis.com/auth/drive",
 ]
 
-credentials = Credentials.from_service_account_info(
-    json.loads(SERVICE_ACCOUNT_INFO), scopes=SCOPES
-)
 if not ENDPOINT_ID_A:
-    raise ValueError("ENDPOINT_ID is not set")
+    raise ValueError("ENDPOINT_ID_A is not set")
 if not ENDPOINT_ID_B:
     raise ValueError("ENDPOINT_ID_B is not set")
+if not SERVICE_ACCOUNT_INFO:
+    raise ValueError("GCP_SERVICE_ACCOUNT_JSON is not set")
+
+credentials = Credentials.from_service_account_info(
+    json.loads(SERVICE_ACCOUNT_INFO), scopes=SCOPES
+)
 
-def _call_retriever_system1(payload: Dict[str, Any]) -> Dict[str, Any]:
+# Mathlib versions supported by the new endpoint
+MATHLIB_VERSIONS = ["v4.19.0", "v4.24.0", "v4.28.0"]
+DEFAULT_VERSION = "v4.19.0"
+
+LEAN_FINDER = "Lean Finder"
+LEAN_SEARCH = "LeanSearch"
+APP_SOURCE = "lean finder web"
+
+
+# Retriever calls
+
+def _call_lean_finder(query: str, k: int, version: str) -> List[Dict[str, Any]]:
     headers = {"Accept": "application/json", "Content-Type": "application/json"}
     if HF_TOKEN:
         headers["Authorization"] = f"Bearer {HF_TOKEN}"
+    payload = {
+        "inputs": query,
+        "top_k": k,
+        "version": version,
+        "source": APP_SOURCE,
+    }
     try:
         r = requests.post(ENDPOINT_ID_A, json=payload, headers=headers, timeout=60)
         r.raise_for_status()
-        return r.json()
-    except requests.exceptions.RequestException as e:
-        raise RuntimeError("Error: failed to contact retriever system 1. Please try again.")
+        return r.json().get("results", []) or []
+    except requests.exceptions.RequestException:
+        raise RuntimeError("Lean Finder service is unreachable.")
 
-def _call_retriever_system2(query: str, k: int) -> List[Dict[str, Any]]:
+
+def _call_lean_search(query: str, k: int) -> List[Dict[str, Any]]:
     payload = {"query": [query], "num_results": str(k)}
     try:
         r = requests.post(ENDPOINT_ID_B, json=payload, timeout=60)
         r.raise_for_status()
         data = r.json()
         return data[0] if isinstance(data, list) and data else []
-    except requests.exceptions.RequestException as e:
-        raise RuntimeError("Error: failed to contact retriever system 2. Please try again.")
+    except requests.exceptions.RequestException:
+        raise RuntimeError("LeanSearch service is unreachable.")
+
+
+# Normalize results from both retrievers into a common schema
+
+def _norm_lean_finder(results: List[Dict[str, Any]]) -> List[Dict[str, Any]]:
+    out = []
+    for r in results:
+        out.append({
+            "formal_name": (r.get("formal_name") or "").strip(),
+            "informal_name": (r.get("informal_name") or "").strip(),
+            "kind": (r.get("kind") or "").strip(),
+            "type": (r.get("type") or "").strip(),
+            "informal_description": (r.get("informal_description") or "").strip(),
+            "path": (r.get("path") or "").strip(),
+            "score": float(r.get("score") or 0.0),
+            "source": LEAN_FINDER,
+        })
+    return out
+
+
+def _norm_lean_search(results: List[Dict[str, Any]]) -> List[Dict[str, Any]]:
+    out = []
+    for e in results:
+        r = e.get("result", {}) or {}
+        formal_name = ".".join(r.get("name") or [])
+        module = r.get("module_name") or []
+        path = "/".join(module) if module else ""
+        type_str = (r.get("type") or r.get("signature") or "").strip()
+        # LeanSearch returns a distance (lower is better, ~cosine). Convert to a
+        # similarity-ish score for display only.
+        try:
+            distance = float(e.get("distance") or 1.0)
+        except (TypeError, ValueError):
+            distance = 1.0
+        score = max(0.0, min(1.0, 1.0 - distance))
+        out.append({
+            "formal_name": formal_name.strip(),
+            "informal_name": (r.get("informal_name") or "").strip(),
+            "kind": (r.get("kind") or "").strip(),
+            "type": type_str,
+            "informal_description": (r.get("informal_description") or "").strip(),
+            "path": path,
+            "score": score,
+            "source": LEAN_SEARCH,
+        })
+    return out
+
+
+# Google Sheets — new sheet names
+
+gc = gspread.authorize(credentials)
+SHEET_LOCK = threading.Lock()
+_spreadsheet = gc.open("arena_votes")
 
-gc         = gspread.authorize(credentials)
-worksheet  = gc.open("arena_votes").sheet1
-vote_worksheet = gc.open("arena_votes").worksheet("individual_votes")
 
-SHEET_LOCK = threading.Lock()
+def _get_or_create_sheet(name: str, header: List[str]):
+    try:
+        ws = _spreadsheet.worksheet(name)
+        # Ensure header exists
+        try:
+            first = ws.row_values(1)
+        except Exception:
+            first = []
+        if not first:
+            ws.append_row(header, value_input_option="RAW")
+        return ws
+    except WorksheetNotFound:
+        ws = _spreadsheet.add_worksheet(title=name, rows=2000, cols=max(12, len(header)))
+        ws.append_row(header, value_input_option="RAW")
+        return ws
+
+
+comparison_ws = _get_or_create_sheet(
+    "leansearch_comparison_updated",
+    ["timestamp", "query", "version", "ui_choice", "winner", "a_source", "b_source", "payload", "type"],
+)
+individual_ws = _get_or_create_sheet(
+    "individual_votes_updated",
+    ["timestamp", "query", "version", "formal_name", "vote_decision", "system", "rank", "payload"],
+)
+
+
+VOTE_UI = ["Retriever A better", "Retriever B better", "Tie", "Both are bad"]
 
-VOTE_UI  = ["Retriever A better", "Retriever B better", "Tie", "Both are bad"]
 
-def _save_vote(choice: str, query: str,
-               ret_a_json: Dict[str, Any], ret_b_json: List[Dict[str, Any]], 
-               sys1_is_a: bool) -> gr.Textbox:
+def _save_vote(choice: str, query: str, version: str,
+               ret_a: List[Dict[str, Any]], ret_b: List[Dict[str, Any]],
+               a_source: str, b_source: str):
     if not choice:
-        return gr.update(value="**Please pick a system.**", visible=True)
+        return gr.update(value="⚠️ Please pick a winner first.", visible=True)
+
     if choice == "Retriever A better":
-        actual_winner = "System1 better" if sys1_is_a else "System2 better"
+        winner = a_source
     elif choice == "Retriever B better":
-        actual_winner = "System2 better" if sys1_is_a else "System1 better"
+        winner = b_source
     else:
-        actual_winner = choice
+        winner = choice  # "Tie" or "Both are bad"
 
     payload = {
-        "retriever_a": ret_a_json,
-        "retriever_b": ret_b_json,
-        "sys1_is_a": sys1_is_a,
+        "retriever_a": ret_a,
+        "retriever_b": ret_b,
+        "a_source": a_source,
+        "b_source": b_source,
     }
     row = [
-        datetime.datetime.utcnow().isoformat(timespec="seconds"),
+        datetime.datetime.now(datetime.timezone.utc).replace(tzinfo=None).isoformat(timespec="seconds"),
         query,
-        actual_winner,
+        version,
+        choice,
+        winner,
+        a_source,
+        b_source,
         json.dumps(payload, ensure_ascii=False),
-        "User Preference"
+        "User Preference",
     ]
     with SHEET_LOCK:
-        worksheet.append_row(row, value_input_option="RAW")
-    return gr.update(value="**Vote recorded — thanks!**", visible=True)
+        comparison_ws.append_row(row, value_input_option="RAW")
+    return gr.update(value="✅ **Vote recorded — thanks!**", visible=True)
+
 
-def _save_individual_vote(formal_statement: str, vote_decision: str, query: str, system: str, rank: int, payload: Dict[str, Any]) -> str:
+def _save_individual_vote(formal_name: str, vote_decision: str, query: str,
+                          system: str, rank: int, version: str,
+                          payload: Dict[str, Any]) -> str:
     row = [
-        datetime.datetime.utcnow().isoformat(timespec="seconds"),
+        datetime.datetime.now(datetime.timezone.utc).replace(tzinfo=None).isoformat(timespec="seconds"),
         query,
-        formal_statement,
+        version,
+        formal_name,
         vote_decision,
         system,
         rank,
-        json.dumps(payload, ensure_ascii=False)
+        json.dumps(payload, ensure_ascii=False),
     ]
     try:
         with SHEET_LOCK:
-            vote_worksheet.append_row(row, value_input_option="RAW")
+            individual_ws.append_row(row, value_input_option="RAW")
         return "Vote recorded!"
     except Exception as e:
-        return f"Error writing to Google Sheets: {str(e)}"
+        return f"Error writing to Google Sheets: {e}"
+
+
+# Rendering
+
+KIND_COLORS = {
+    "theorem":     ("#dbeafe", "#1d4ed8"),
+    "lemma":       ("#dbeafe", "#1d4ed8"),
+    "def":         ("#d1fae5", "#047857"),
+    "definition":  ("#d1fae5", "#047857"),
+    "structure":   ("#ede9fe", "#6d28d9"),
+    "class":       ("#ede9fe", "#6d28d9"),
+    "inductive":   ("#ffedd5", "#c2410c"),
+    "instance":    ("#fce7f3", "#be185d"),
+    "abbrev":      ("#cffafe", "#0e7490"),
+    "opaque":      ("#e5e7eb", "#374151"),
+    "axiom":       ("#fef3c7", "#a16207"),
+}
 
-def _process_informal_statement(text: str) -> str:
-    if not text:
+
+def _kind_chip(kind: str) -> str:
+    label = (kind or "").strip()
+    if not label:
         return ""
-    
-    text = re.sub(r'`([^`]+)`', r'<code>\1</code>', text)
-    return text
-
-def _render_system1_results(res: List[Dict[str, Any]], title: str = "Retriever A", query: str = ""):
-    if not res:
-        return f"<p>No results from {title}.</p>"
-    
-    def make_row(i: int, r: Dict[str, Any]) -> str:
-        formal_text = r['formal_statement']
-        informal_text = r['informal_statement']
-        
-        formal_escaped = html.escape(formal_text)
-        doc_url = r.get('url', '')
-        doc_button = f'<button class="doc-button" onclick="window.open(\'{doc_url}\', \'_blank\')" title="View documentation">Doc</button>' if doc_url else ''
-        
-        formal_cell = (
-            f'<div class="copy-container">'
-            f'<code style="white-space:pre-wrap">{formal_escaped}</code>'
-            f'<div class="button-container">'
-            f'<div class="left-buttons">'
-            f'{doc_button}'
-            f'<button class="copy-button" data-copy-text="{formal_escaped}" onclick="copyToClipboard(this.getAttribute(\'data-copy-text\'), this)">Copy</button>'
-            f'</div>'
-            f'<div class="right-buttons">'
-            f'<button class="vote-button upvote" data-formal="{formal_escaped}" data-query="{html.escape(query)}" data-system="System1" data-rank="{i}" onclick="voteOnResultSafe(this, \'Upvote\')">👍</button>'
-            f'<button class="vote-button downvote" data-formal="{formal_escaped}" data-query="{html.escape(query)}" data-system="System1" data-rank="{i}" onclick="voteOnResultSafe(this, \'Downvote\')">👎</button>'
-            f'</div>'
-            f'</div>'
-            f'</div>'
-        )
-        
-        informal_cell = (
-            f'<div class="copy-container">'
-            f'<span style="white-space:pre-wrap">{_process_informal_statement(informal_text)}</span>'
-            f'<div class="button-container">'
-            f'<button class="copy-button" data-copy-text="{informal_text}" onclick="copyToClipboard(this.getAttribute(\'data-copy-text\'), this)">Copy</button>'
-            f'</div>'
-            f'</div>'
-        )
-        
-        return f"<tr><td>{i}</td><td>{formal_cell}</td><td>{informal_cell}</td></tr>"
-    
-    rows = "\n".join(make_row(i, r) for i, r in enumerate(res, 1))
+    bg, fg = KIND_COLORS.get(label.lower(), ("#e5e7eb", "#374151"))
     return (
-        f"<h3>{title}</h3>"
-        "<table><thead><tr><th>Rank</th>"
-        "<th>Formal statement</th><th>Informal statement</th></tr></thead>"
-        f"<tbody>{rows}</tbody></table>"
+        f'<span class="kind-chip" '
+        f'style="background:{bg};color:{fg};">{html.escape(label)}</span>'
     )
 
-def _render_system2_results(res: List[Dict[str, Any]], title: str = "Retriever B", query: str = ""):
-    if not res:
-        return f"<p>No results from {title}.</p>"
-    
-    def row(i: int, e: Dict[str, Any]) -> str:
-        r   = e.get("result", {})
-        kind, name = r.get("kind","").strip(), ".".join(r.get("name", []))
-        sig = r.get("signature") or ""
-        val = (r.get("value") or "").lstrip()
-        formal_text = f"{kind} {name}{sig} {val}".strip()
-        informal_text = r.get('informal_description','')
-        
-        formal_escaped = html.escape(formal_text)
-        full_name = ".".join(r.get("name", []))
-        doc_url = f"https://leanprover-community.github.io/mathlib4_docs/find/?pattern={full_name}#doc" if full_name else ""
-        doc_button = f'<button class="doc-button" onclick="window.open(\'{doc_url}\', \'_blank\')" title="View documentation">Doc</button>' if doc_url else ''
-        formal_cell = (
-            f'<div class="copy-container">'
-            f'<code style="white-space:pre-wrap">{formal_escaped}</code>'
-            f'<div class="button-container">'
-            f'<div class="left-buttons">'
-            f'{doc_button}'
-            f'<button class="copy-button" data-copy-text="{formal_escaped}" onclick="copyToClipboard(this.getAttribute(\'data-copy-text\'), this)">Copy</button>'
-            f'</div>'
-            f'<div class="right-buttons">'
-            f'<button class="vote-button upvote" data-formal="{formal_escaped}" data-query="{html.escape(query)}" data-system="System2" data-rank="{i}" onclick="voteOnResultSafe(this, \'Upvote\')">👍</button>'
-            f'<button class="vote-button downvote" data-formal="{formal_escaped}" data-query="{html.escape(query)}" data-system="System2" data-rank="{i}" onclick="voteOnResultSafe(this, \'Downvote\')">👎</button>'
-            f'</div>'
-            f'</div>'
-            f'</div>'
+
+def _result_card(idx: int, r: Dict[str, Any], system_label: str, query: str,
+                 arena_mode: bool, version: str = "") -> str:
+    formal_name = r.get("formal_name", "")
+    informal_name = r.get("informal_name", "")
+    kind = r.get("kind", "")
+    type_str = r.get("type", "")
+    informal_desc = r.get("informal_description", "")
+    path = (r.get("path") or "").strip()
+
+    formal_escaped = html.escape(formal_name)
+    type_escaped = html.escape(type_str)
+    query_escaped = html.escape(query)
+    system_escaped = html.escape(system_label)
+
+    doc_url = (
+        f"https://leanprover-community.github.io/mathlib4_docs/find/"
+        f"?pattern={requests.utils.quote(formal_name)}#doc"
+        if formal_name else ""
+    )
+
+    btns: List[str] = []
+    if doc_url:
+        btns.append(
+            f'<button class="card-btn" '
+            f'onclick="window.open(\'{doc_url}\', \'_blank\')" '
+            f'title="Open in mathlib docs">Doc</button>'
         )
-        
-        informal_cell = (
-            f'<div class="copy-container">'
-            f'<span style="white-space:pre-wrap">{_process_informal_statement(informal_text)}</span>'
-            f'<div class="button-container">'
-            f'<button class="copy-button" data-copy-text="{informal_text}" onclick="copyToClipboard(this.getAttribute(\'data-copy-text\'), this)">Copy</button>'
-            f'</div>'
+    btns.append(
+        f'<button class="card-btn" data-copy-text="{formal_escaped}" '
+        f'onclick="copyToClipboard(this.getAttribute(\'data-copy-text\'), this)" '
+        f'title="Copy name">Copy</button>'
+    )
+
+    vote_cluster = ""
+    if arena_mode:
+        vote_cluster = (
+            f'<div class="vote-cluster">'
+            f'<button class="vote-btn upvote" data-formal="{formal_escaped}" '
+            f'data-query="{query_escaped}" data-system="{system_escaped}" '
+            f'data-rank="{idx}" onclick="voteOnResultSafe(this, \'Upvote\')" '
+            f'title="Useful">👍</button>'
+            f'<button class="vote-btn downvote" data-formal="{formal_escaped}" '
+            f'data-query="{query_escaped}" data-system="{system_escaped}" '
+            f'data-rank="{idx}" onclick="voteOnResultSafe(this, \'Downvote\')" '
+            f'title="Not useful">👎</button>'
             f'</div>'
         )
-        
-        return f"<tr><td>{i}</td><td>{formal_cell}</td><td>{informal_cell}</td></tr>"
-    
-    rows = "\n".join(row(i,e) for i,e in enumerate(res,1))
+
+    informal_name_html = (
+        f'<div class="informal-name"><span class="math-content">'
+        f'{html.escape(informal_name)}</span></div>'
+        if informal_name else ""
+    )
+
+    informal_desc_html = ""
+    if informal_desc:
+        if len(informal_desc) > 320:
+            preview = informal_desc[:320].rstrip() + "…"
+            informal_desc_html = (
+                f'<div class="informal-desc collapsible">'
+                f'<span class="math-content desc-preview">{html.escape(preview)}</span>'
+                f'<span class="math-content desc-full" hidden>{html.escape(informal_desc)}</span>'
+                f'<button class="link-btn read-more" onclick="toggleDesc(this)">Read more</button>'
+                f'</div>'
+            )
+        else:
+            informal_desc_html = (
+                f'<div class="informal-desc">'
+                f'<span class="math-content">{html.escape(informal_desc)}</span>'
+                f'</div>'
+            )
+
+    type_section_html = (
+        f'<pre class="formal-type"><code>{type_escaped}</code></pre>'
+        if type_str else ""
+    )
+    path_html = ""
+    if path:
+        path_dotted = html.escape(path.replace("/", "."))
+        github_url = f"https://github.com/leanprover-community/mathlib4/tree/{version}/{path}.lean" if version else ""
+        if github_url:
+            path_html = f'<div class="module-path">In: <a href="{github_url}" target="_blank" class="module-path-link">{path_dotted}</a></div>'
+        else:
+            path_html = f'<div class="module-path">In: {path_dotted}</div>'
+
+    return (
+        f'<article class="result-card">'
+        f'  <div class="card-header">'
+        f'    <span class="rank-badge">{idx}</span>'
+        f'    {_kind_chip(kind)}'
+        f'    <code class="formal-name">{formal_escaped}</code>'
+        f'    <div class="header-actions">{"".join(btns)}{vote_cluster}</div>'
+        f'  </div>'
+        f'  {informal_name_html}'
+        f'  {informal_desc_html}'
+        f'  {type_section_html}'
+        f'  {path_html}'
+        f'</article>'
+    )
+
+
+def _render_column(results: List[Dict[str, Any]], col_title: str,
+                   system_label: str, query: str, arena_mode: bool,
+                   version: str = "", col_css: str = "") -> str:
+    if not results:
+        body = '<p class="empty">No results.</p>'
+    else:
+        body = "".join(_result_card(i, r, system_label, query, arena_mode, version)
+                       for i, r in enumerate(results, 1))
+    cls = f'results-column {col_css}'.strip()
     return (
-        f"<h3>{title}</h3>"
-        "<table><thead><tr><th>Rank</th>"
-        "<th>Formal statement</th><th>Informal statement</th></tr></thead>"
-        f"<tbody>{rows}</tbody></table>"
+        f'<div class="{cls}">'
+        f'  <div class="col-title">{html.escape(col_title)}</div>'
+        f'  <div class="cards-stack">{body}</div>'
+        f'</div>'
     )
 
+
+def _render_single(results: List[Dict[str, Any]], query: str, version: str = "") -> str:
+    if not results:
+        return '<div class="empty-state">No matching Lean statements found.</div>'
+    cards = "".join(_result_card(i, r, LEAN_FINDER, query, arena_mode=False, version=version)
+                    for i, r in enumerate(results, 1))
+    return f'<div class="results-single"><div class="cards-stack">{cards}</div></div>'
+
+
+def _render_arena(ret_a: List[Dict[str, Any]], ret_b: List[Dict[str, Any]],
+                  a_source: str, b_source: str, query: str, version: str = "") -> str:
+    a_html = _render_column(ret_a, "Retriever A", a_source, query, arena_mode=True, version=version, col_css="column-a")
+    b_html = _render_column(ret_b, "Retriever B", b_source, query, arena_mode=True, version=version, col_css="column-b")
+    return f'<div class="arena-grid">{a_html}{b_html}</div>'
+
+
+# Static content
+
 INSTRUCTIONS_MD = """
-## Supported query types
-
-### 1. Informalized statement  
-Enter an informal translation of a formal Lean statement, and find relevant Lean statements.\n
-**Example:** 
-```
-Let L/K be a field extension and let x, y ∈ L be algebraic elements over K with the same minimal polynomial. Then the K-algebra isomorphism algEquiv between the simple field extensions K(x) and K(y) maps the generator x of K(x) to the generator y of K(y); i.e. algEquiv(x) = y.
-```
-
-### 2. User question  
-Ask any question about Lean statements.\n
-**Example:** 
-```
-I'm working with algebraic elements over a field extension … Does this imply that the minimal polynomials of `x` and `y` are equal?
-```
-
-### 3. Proof State 
-Enter the proof state of a theorem. For better results, enter a proof state followed by how you want to transform the proof state.\n
-**Example:** 
-```
-K : Type u_1\nE : Type u_2\ninst✝ : RCLike K\nz✝ z : K\n⊢ |re z| ≤ ‖z‖\nTransform the goal from proving that the absolute value of the real part of a complex number is less than or equal to its norm, to proving that the square of the real part is less than or equal to the squared norm of the number.
-```
-
-### 4. Statement definition  
-Enter any fragment or the whole statement definition, and find statements that match the entered content. Note that the query syntax doesn't need to be perfect.\n
-**Example:** 
-```
-theorem restrict Ioi: restrict Ioi e = restrict Ici e
-```
+### Lean Finder accepts four kinds of queries
+
+1. **Informalized statement** — A natural-language rendering of a Lean statement.
+   > *Let L/K be a field extension and let x, y ∈ L be algebraic elements over K with the same minimal polynomial. Then the K-algebra isomorphism algEquiv between the simple field extensions K(x) and K(y) maps the generator x of K(x) to the generator y of K(y); i.e. algEquiv(x) = y.*
+
+2. **User question** — Free-form questions about Lean / Mathlib.
+   > *I'm working with algebraic elements over a field extension … Does this imply that the minimal polynomials of `x` and `y` are equal?*
+
+3. **Proof state** — Paste a proof state, optionally followed by what you want to do next.
+   > *K : Type u_1, E : Type u_2, inst✝ : RCLike K, z✝ z : K ⊢ |re z| ≤ ‖z‖. Transform the goal from proving that the absolute value of the real part is ≤ the norm, to proving that the square of the real part is ≤ the squared norm.*
+
+4. **Statement fragment** — A snippet or rough draft of the Lean definition you're looking for.
+   > *theorem restrict Ioi: restrict Ioi e = restrict Ici e*
+
+**Mathlib version** — pick from `v4.19.0`, `v4.24.0`, or `v4.28.0`. Lean Finder
+queries the index matching that version so the formal names it returns actually
+exist in your build.
 """
 
-# Gradio app
+
 CUSTOM_CSS = """
-html,body{margin:0;padding:0;width:100%;}
-.gradio-container,.gradio-container .block{
-    max-width:none!important;width:100%!important;padding:0 0.5rem;
+:root {
+    --bg: #ffffff;
+    --fg: #111827;
+    --muted: #6b7280;
+    --border: #e5e7eb;
+    --card-bg: #ffffff;
+    --card-border: #e5e7eb;
+    --card-hover-border: #c7d2fe;
+    --primary: #4f46e5;
+    --primary-2: #7c3aed;
+    --primary-soft: #eef2ff;
+    --code-bg: #f9fafb;
+    --success: #10b981;
+    --danger: #ef4444;
 }
 
-/* Tables and code blocks */
-table{width:100%;border-collapse:collapse;font-size:0.9rem;}
-th,td{border:1px solid #ddd;padding:6px;vertical-align:top;}
-th{background:#f5f5f5;font-weight:600;}
-code{background:#f8f8f8;border:1px solid #eee;border-radius:4px;padding:2px 4px;color:#333;}
+@media (prefers-color-scheme: dark) {
+    :root {
+        --bg: #0b0b0d;
+        --fg: #e5e7eb;
+        --muted: #9ca3af;
+        --border: #27272a;
+        --card-bg: #141417;
+        --card-border: #27272a;
+        --card-hover-border: #4f46e5;
+        --primary: #818cf8;
+        --primary-2: #a78bfa;
+        --primary-soft: #1e1b4b;
+        --code-bg: #0f0f12;
+        --success: #34d399;
+        --danger: #f87171;
+    }
+}
+.dark {
+    --bg: #0b0b0d;
+    --fg: #e5e7eb;
+    --muted: #9ca3af;
+    --border: #27272a;
+    --card-bg: #141417;
+    --card-border: #27272a;
+    --card-hover-border: #4f46e5;
+    --primary: #818cf8;
+    --primary-2: #a78bfa;
+    --primary-soft: #1e1b4b;
+    --code-bg: #0f0f12;
+    --success: #34d399;
+    --danger: #f87171;
+}
 
-td code{
-    background:#f0f0f0;
-    border:1px solid #ddd;
-    border-radius:3px;
-    padding:1px 3px;
-    font-size:0.9em;
-    font-family:Monaco, Consolas, "Courier New", monospace;
+html, body { margin: 0; padding: 0; width: 100%; }
+.gradio-container, .gradio-container .block {
+    max-width: 1280px !important;
+    margin: 0 auto !important;
+    padding: 0 1rem;
 }
 
-/* Dark mode support */
+/* Hero — 3-column grid keeps the logo+title centered while the badge floats right */
+.lf-hero {
+    display: grid;
+    grid-template-columns: 1fr auto 1fr;
+    align-items: center;
+    gap: 1rem;
+    padding: 1.6rem 1.4rem;
+    margin: 0.5rem 0 1.1rem;
+    background: linear-gradient(135deg, rgba(102,126,234,0.08) 0%, rgba(118,75,162,0.08) 100%);
+    border: 1px solid var(--border);
+    border-radius: 18px;
+}
+.lf-hero-main {
+    grid-column: 2;
+    display: flex;
+    align-items: center;
+    gap: 1.1rem;
+    min-width: 0;
+}
+.lf-hero .lf-logo {
+    width: 76px; height: 76px; flex: 0 0 76px;
+    border-radius: 14px;
+    object-fit: contain;
+    background: white;
+    padding: 8px;
+    box-shadow: 0 2px 10px rgba(0,0,0,0.06);
+}
+.lf-hero-text { display: flex; flex-direction: column; justify-content: center; min-width: 0; }
+.lf-title {
+    margin: 0 !important;
+    padding: 0 !important;
+    font-size: clamp(2rem, 4.5vw, 2.85rem) !important;
+    font-weight: 800 !important;
+    line-height: 1.1 !important;
+    letter-spacing: -0.02em !important;
+    color: #4f46e5; /* fallback for browsers that don't support gradient text */
+    background: linear-gradient(135deg, #4f46e5 0%, #7c3aed 100%);
+    -webkit-background-clip: text;
+    background-clip: text;
+    -webkit-text-fill-color: transparent;
+    display: inline-block;
+}
 @media (prefers-color-scheme: dark) {
-    table{color:#e0e0e0;}
-    th,td{border:1px solid #555;}
-    th{background:#2a2a2a;color:#e0e0e0;}
-    code{background:#2a2a2a;border:1px solid #555;color:#e0e0e0;}
-    
-    td code{
-        background:#333;
-        border:1px solid #555;
-        color:#e0e0e0;
+    .lf-title {
+        color: #a78bfa;
+        background: linear-gradient(135deg, #818cf8 0%, #c4b5fd 100%);
+        -webkit-background-clip: text;
+        background-clip: text;
+        -webkit-text-fill-color: transparent;
     }
 }
-
-/* Arena voting controls */
-#vote_area{
-    margin-top:1.5rem;
-    align-items:center;
-    justify-content:center;
-    gap:1rem;
-    flex-wrap:wrap;
-    border:none!important;
-    box-shadow:none!important;
+.dark .lf-title {
+    color: #a78bfa;
+    background: linear-gradient(135deg, #818cf8 0%, #c4b5fd 100%);
+    -webkit-background-clip: text;
+    background-clip: text;
+    -webkit-text-fill-color: transparent;
+}
+.lf-tagline {
+    margin: 0.35rem 0 0 0;
+    color: var(--muted);
+    font-size: 0.92rem;
+    font-weight: 400;
+    line-height: 1.4;
+}
+.lf-hero-badge {
+    grid-column: 3;
+    justify-self: end;
+    display: inline-flex;
+    align-items: center;
+    gap: 0.4rem;
+    padding: 0.5rem 0.95rem;
+    background: linear-gradient(135deg, #667eea 0%, #764ba2 100%);
+    color: white;
+    text-decoration: none;
+    border-radius: 999px;
+    font-weight: 500;
+    font-size: 0.82rem;
+    box-shadow: 0 2px 8px rgba(102, 126, 234, 0.25);
+    transition: transform .15s ease, box-shadow .15s ease;
+    white-space: nowrap;
+}
+.lf-hero-badge:hover {
+    transform: translateY(-1px);
+    box-shadow: 0 6px 16px rgba(102, 126, 234, 0.35);
+}
+@media (max-width: 760px) {
+    .lf-hero {
+        grid-template-columns: 1fr;
+        text-align: center;
+        gap: 0.75rem;
+    }
+    .lf-hero-main { grid-column: 1; flex-direction: column; }
+    .lf-hero-badge { grid-column: 1; justify-self: center; }
 }
 
-#vote_radio_col{
-    display:flex;
-    flex-direction:column;
-    align-items:center;
-    gap:0.75rem;
+/* Query input */
+#query_input textarea {
+    resize: vertical !important;
+    min-height: 120px !important;
+    max-height: 360px !important;
+    font-size: 0.95rem !important;
+    line-height: 1.5 !important;
+    padding: 12px !important;
+    border-radius: 10px !important;
 }
 
-#vote_radio .gr-radio{display:flex;gap:0.75rem;}
-#vote_radio label{
-    padding:4px 14px;
-    border:1px solid #ccc;
-    border-radius:8px;
-    cursor:pointer;
-    user-select:none;
-    transition:all .15s ease;
+/* Controls row — keep compact, even baseline */
+#controls_row { gap: 0.75rem; align-items: flex-end; margin-top: 0.4rem; }
+#controls_row label { font-size: 0.8rem !important; font-weight: 500 !important; color: var(--muted) !important; }
+#controls_row label.selected, #controls_row label.selected span { color: white !important; }
+#controls_row .gr-form { background: transparent !important; border: none !important; }
+
+/* Search button - the only purple gradient in this region */
+#search_btn { margin: 0.9rem 0 0.6rem; }
+#search_btn button {
+    background: linear-gradient(135deg, var(--primary) 0%, var(--primary-2) 100%) !important;
+    color: white !important;
+    border: none !important;
+    padding: 0.85rem 1.4rem !important;
+    font-weight: 600 !important;
+    font-size: 1rem !important;
+    border-radius: 12px !important;
+    box-shadow: 0 4px 14px rgba(79, 70, 229, 0.28) !important;
+    transition: transform .12s ease, box-shadow .15s ease !important;
+    width: 100% !important;
 }
-#vote_radio input[type="radio"]:checked + label{
-    background:#0066ff;color:#fff;border-color:#0066ff;
+#search_btn button:hover {
+    transform: translateY(-1px) !important;
+    box-shadow: 0 8px 20px rgba(79, 70, 229, 0.38) !important;
 }
 
-#submit_btn button{
-    padding:0.65rem 1.6rem;
-    font-weight:600;font-size:1rem;border-radius:8px;
+#mode_description { color: var(--muted); font-size: 0.85rem; margin: 0.2rem 0 0.4rem; }
+#mode_description p { margin: 0; }
+
+/* Result cards */
+.results-single, .arena-grid { margin-top: 1rem; }
+.arena-grid {
+    display: grid;
+    grid-template-columns: 1fr 1fr;
+    gap: 1rem;
+}
+@media (max-width: 860px) {
+    .arena-grid { grid-template-columns: 1fr; }
 }
 
-#vote_status{margin-top:0.5rem;text-align:center;}   /* works for Markdown */
+.results-column { display: flex; flex-direction: column; min-width: 0; }
 
-#lf_header.gr-column{
-    display:flex !important;
-    flex-direction:row !important;
-    align-items:center !important;
-    justify-content:center !important;
-    gap:1rem !important;
-    width:100% !important;
-    margin:1rem auto !important;
-    padding:0 !important;
+/* Vertical divider between arena columns */
+.results-column.column-b { border-left: 2px solid #6366f1; padding-left: 1rem; }
+@media (prefers-color-scheme: dark) {
+    .results-column.column-b { border-left-color: #818cf8; }
 }
+.dark .results-column.column-b { border-left-color: #818cf8; }
 
-/* Alternative selector in case the above doesn't work */
-div#lf_header{
-    display:flex !important;
-    flex-direction:row !important;
-    align-items:center !important;
-    justify-content:center !important;
-    gap:1rem !important;
-    width:100% !important;
-    margin:1rem auto !important;
-    padding:0 !important;
+/* Subtle, non-gradient column titles */
+.col-title {
+    font-size: 0.78rem;
+    margin: 0 0 0.7rem 0;
+    padding: 0.4rem 0;
+    color: var(--muted);
+    font-weight: 600;
+    text-align: center;
+    letter-spacing: 0.12em;
+    text-transform: uppercase;
+    border-bottom: 1px solid var(--border);
 }
 
-#lf_logo{
-    width:60px !important;
-    height:60px !important;
-    flex:0 0 60px !important;
-    overflow:hidden;
-}
+.cards-stack { display: flex; flex-direction: column; gap: 0.7rem; }
 
-#lf_logo .gr-image-toolbar{
-    display:none !important;
+.result-card {
+    background: var(--card-bg);
+    border: 1px solid var(--card-border);
+    border-radius: 12px;
+    padding: 0.85rem 1rem;
+    transition: border-color .15s ease, box-shadow .15s ease, transform .12s ease;
+    box-shadow: 0 1px 2px rgba(0,0,0,0.04);
+    min-width: 0;
+}
+.result-card:hover {
+    border-color: var(--card-hover-border);
+    box-shadow: 0 4px 14px rgba(79, 70, 229, 0.08);
 }
 
+.card-header {
+    display: flex;
+    align-items: center;
+    gap: 0.55rem;
+    min-width: 0;
+}
 
-/* Fix the HTML container for the title */
-#lf_header .gr-html{
-    width:auto !important;
-    min-width:auto !important;
-    max-width:none !important;
-    flex:0 0 auto !important;
+.rank-badge {
+    display: inline-flex;
+    align-items: center;
+    justify-content: center;
+    width: 1.6rem;
+    height: 1.6rem;
+    border-radius: 50%;
+    background: var(--primary-soft);
+    color: var(--primary);
+    font-weight: 700;
+    font-size: 0.78rem;
+    flex-shrink: 0;
 }
 
-.lf-title{
-    margin:0 !important;
-    padding:0 !important;
-    font-size:1.6rem !important;
-    font-weight:700 !important;
-    white-space:normal !important;
-    color:#333 !important;
-    line-height:1.2 !important;
-    text-align:center !important;
+.kind-chip {
+    font-size: 0.65rem;
+    font-weight: 700;
+    padding: 0.18rem 0.55rem;
+    border-radius: 999px;
+    letter-spacing: 0.04em;
+    text-transform: uppercase;
+    line-height: 1.4;
 }
 
-.gr-accordion-header {
-    font-size: 1.05rem;
+code.formal-name {
+    background: transparent;
+    border: none;
+    color: var(--fg);
     font-weight: 600;
-    cursor: pointer;
-    padding: 0.4rem 0;
+    font-size: 0.92rem;
+    padding: 0;
+    word-break: break-all;
+    flex: 1 1 0;
+    min-width: 0;
+    font-family: 'JetBrains Mono', ui-monospace, Menlo, Monaco, Consolas, 'Courier New', monospace;
 }
 
-/* Progress bar overlay fix for HF Spaces */
-div.gradio-modal[aria-label="progress"]          /* outer overlay on HF */
-{
-    position: fixed !important;      /* pull it out of the normal flow   */
-    top: 50% !important;             /* perfectly centred in the viewport */
-    left: 50% !important;
-    transform: translate(-50%, -50%) !important;
-    z-index: 2000 !important;
-
-    width: clamp(260px, 70vw, 440px) !important;
-    max-height: 140px !important;
-    padding: 20px 24px !important;
-
-    /* optional aesthetic tweaks — remove if you like HF’s defaults */
-    background: var(--block-background-fill, #fff) !important;
-    border: 1px solid #ddd !important;
-    border-radius: 8px !important;
-    box-shadow: 0 4px 12px rgba(0,0,0,.15) !important;
-    pointer-events: none !important;
+.module-path {
+    margin-top: 0.3rem;
+    font-size: 0.75rem;
+    color: var(--muted);
+    font-family: 'JetBrains Mono', ui-monospace, Menlo, Monaco, Consolas, monospace;
+    opacity: 0.75;
+    letter-spacing: 0.01em;
+}
+.module-path-link {
+    color: var(--primary);
+    opacity: 0.55;
+    text-decoration: underline;
+    text-decoration-color: rgba(79, 70, 229, 0.25);
+    text-underline-offset: 2px;
+    transition: opacity .12s ease, text-decoration-color .12s ease;
+}
+.module-path-link:hover {
+    opacity: 0.85;
+    text-decoration-color: var(--primary);
 }
 
-
-/* Copy button styling */
-.copy-container {
-    position: relative;
-    display: block;
-    width: 100%;
-    min-height: 1.5em;
+.header-actions {
+    display: flex;
+    gap: 0.3rem;
+    margin-left: auto;
+    align-items: center;
+    flex-wrap: wrap;
 }
 
-.copy-button {
-    background: rgba(0, 0, 0, 0.1);
-    border: 1px solid #ccc;
-    border-radius: 4px;
-    padding: 4px 8px;
-    font-size: 12px;
+.card-btn {
+    display: inline-flex;
+    align-items: center;
+    justify-content: center;
+    gap: 0.35rem;
+    height: 32px;
+    padding: 0 0.8rem;
+    background: var(--bg);
+    border: 1px solid var(--border);
+    color: var(--muted);
+    border-radius: 7px;
+    font-size: 0.82rem;
+    line-height: 1;
     cursor: pointer;
-    transition: background-color 0.2s ease;
-    color: #666;
-    font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, sans-serif;
-    line-height: 1.2;
+    transition: all .12s ease;
     white-space: nowrap;
-    vertical-align: baseline;
-    box-sizing: border-box;
+    font-family: inherit;
+    font-weight: 500;
+    vertical-align: middle;
 }
-
-.copy-button:hover {
-    background: rgba(0, 0, 0, 0.2);
+.card-btn:hover {
+    border-color: var(--primary);
+    color: var(--primary);
+    background: var(--primary-soft);
 }
 
-.copy-button:active {
-    background: rgba(0, 0, 0, 0.3);
+.vote-cluster {
+    display: inline-flex;
+    align-items: center;
+    gap: 0.25rem;
+    margin-left: 0.4rem;
+    padding-left: 0.55rem;
+    border-left: 1px solid var(--border);
 }
 
-td {
-    position: relative;
+.vote-btn {
+    display: inline-flex;
+    align-items: center;
+    justify-content: center;
+    height: 28px;
+    min-width: 36px;
+    padding: 0 0.4rem;
+    background: var(--bg);
+    border: 1px solid var(--border);
+    color: var(--muted);
+    border-radius: 7px;
+    font-size: 0.95rem;
+    line-height: 1;
+    cursor: pointer;
+    transition: all .12s ease;
+    vertical-align: middle;
 }
-
-/* Query input styling */
-#query_input textarea {
-    resize: vertical !important;
-    min-height: 100px !important;
-    max-height: 400px !important;
-    font-size: 14px !important;
-    line-height: 1.5 !important;
-    padding: 12px !important;
+.vote-btn:hover { transform: translateY(-1px); }
+.vote-btn.upvote:hover   { border-color: var(--success); color: var(--success); background: rgba(16,185,129,0.08); }
+.vote-btn.downvote:hover { border-color: var(--danger);  color: var(--danger);  background: rgba(239,68,68,0.08); }
+.vote-btn.voted.upvote   { background: var(--success); color: white; border-color: var(--success); }
+.vote-btn.voted.downvote { background: var(--danger);  color: white; border-color: var(--danger); }
+
+.informal-name {
+    margin-top: 0.55rem;
+    font-size: 0.92rem;
+    color: var(--fg);
+    font-weight: 500;
+    line-height: 1.45;
 }
 
-#query_input .gr-textbox {
-    min-height: 100px !important;
+.informal-desc {
+    margin-top: 0.4rem;
+    font-size: 0.86rem;
+    line-height: 1.55;
+    color: var(--muted);
 }
 
-/* Alternative selectors for different Gradio versions */
-textarea[data-testid="textbox"] {
-    resize: vertical !important;
-    min-height: 100px !important;
-    max-height: 400px !important;
+/* Dark-mode: ensure informal text is bright enough on dark card backgrounds */
+@media (prefers-color-scheme: dark) {
+    .informal-name { color: #e5e7eb; }
+    .informal-desc { color: #a1a1aa; }
 }
-
-div[data-testid="textbox"] textarea {
-    resize: vertical !important;
-    min-height: 100px !important;
-    max-height: 400px !important;
+.dark .informal-name { color: #e5e7eb; }
+.dark .informal-desc { color: #a1a1aa; }
+.informal-desc.collapsible .desc-full[hidden] { display: none; }
+.link-btn {
+    background: none;
+    border: none;
+    color: var(--primary);
+    cursor: pointer;
+    font-size: 0.78rem;
+    font-weight: 500;
+    padding: 0 0 0 4px;
+    text-decoration: underline;
+    font-family: inherit;
 }
-
-/* Vote buttons styling */
-.vote-button {
+.link-btn:hover { text-decoration: none; }
+
+/* Formal type — always visible, calm look */
+.formal-type {
+    background: var(--code-bg);
+    border: 1px solid var(--border);
+    border-radius: 8px;
+    padding: 0.65rem 0.8rem;
+    margin: 0.7rem 0 0;
+    overflow-x: auto;
+    font-size: 0.78rem;
+    line-height: 1.5;
+}
+.formal-type code {
     background: transparent;
-    border: 1px solid #ddd;
-    border-radius: 4px;
-    padding: 4px 8px;
-    cursor: pointer;
-    font-size: 16px;
-    line-height: 1.2;
-    transition: all 0.2s ease;
-    opacity: 0.6;
-    vertical-align: baseline;
-    box-sizing: border-box;
+    border: none;
+    padding: 0;
+    white-space: pre-wrap;
+    word-break: break-word;
+    color: var(--fg);
+    font-family: 'JetBrains Mono', ui-monospace, Menlo, Monaco, Consolas, monospace;
 }
 
-.vote-button:hover {
-    opacity: 1;
-    transform: scale(1.1);
+.empty {
+    color: var(--muted);
+    text-align: center;
+    padding: 1rem;
+    font-size: 0.9rem;
 }
-
-.vote-button.upvote {
-    color: #28a745;
-    border-color: #28a745;
+.empty-state {
+    text-align: center;
+    padding: 2.5rem 1rem;
+    color: var(--muted);
+    border: 1px dashed var(--border);
+    border-radius: 12px;
+    margin-top: 0.75rem;
 }
 
-.vote-button.downvote {
-    color: #dc3545;
-    border-color: #dc3545;
+/* Vote area — warm accent so it reads as a separate "action" zone */
+#vote_area {
+    margin: 1rem 0 0.3rem !important;
+    padding: 0.95rem 1.1rem !important;
+    border: 1px solid rgba(245, 158, 11, 0.35) !important;
+    border-radius: 14px !important;
+    background: linear-gradient(180deg, rgba(254, 243, 199, 0.55) 0%, rgba(254, 243, 199, 0.12) 100%) !important;
+    box-shadow: 0 1px 2px rgba(0,0,0,0.03);
 }
-
-/* Doc button styling */
-.doc-button {
-    background: rgba(0, 123, 255, 0.1);
-    border: 1px solid #007bff;
-    border-radius: 4px;
-    padding: 4px 8px;
-    font-size: 12px;
+@media (prefers-color-scheme: dark) {
+    #vote_area {
+        background: linear-gradient(180deg, rgba(120, 53, 15, 0.22) 0%, rgba(120, 53, 15, 0.05) 100%) !important;
+        border-color: rgba(245, 158, 11, 0.30) !important;
+    }
+}
+.dark #vote_area {
+    background: linear-gradient(180deg, rgba(120, 53, 15, 0.22) 0%, rgba(120, 53, 15, 0.05) 100%) !important;
+    border-color: rgba(245, 158, 11, 0.30) !important;
+}
+.vote-area-label {
+    font-size: 0.78rem;
+    font-weight: 700;
+    color: #92400e;
+    letter-spacing: 0.08em;
+    text-transform: uppercase;
+    margin-bottom: 0.55rem;
+}
+@media (prefers-color-scheme: dark) {
+    .vote-area-label { color: #fbbf24; }
+}
+.dark .vote-area-label { color: #fbbf24; }
+#vote_radio .gr-radio { display: flex; gap: 0.45rem; flex-wrap: wrap; }
+#vote_radio label {
+    padding: 6px 14px;
+    border: 1px solid var(--border);
+    background: var(--card-bg);
+    border-radius: 8px;
     cursor: pointer;
-    transition: background-color 0.2s ease;
-    color: #007bff;
-    font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, sans-serif;
-    line-height: 1.2;
-    white-space: nowrap;
-    vertical-align: baseline;
-    box-sizing: border-box;
+    user-select: none;
+    transition: all .15s ease;
+    font-size: 0.86rem;
+    color: var(--fg);
 }
-
-.doc-button:hover {
-    background: #007bff;
+@media (prefers-color-scheme: dark) {
+    #vote_radio label { color: #e5e7eb; background: #1c1c20; border-color: #3f3f46; }
+}
+.dark #vote_radio label { color: #e5e7eb; background: #1c1c20; border-color: #3f3f46; }
+#vote_radio input[type="radio"]:checked + label {
+    background: #f59e0b;
     color: white;
+    border-color: #f59e0b;
 }
 
-/* Button container for all buttons */
-.button-container {
-    display: flex;
-    margin-top: 8px;
-    align-items: baseline;
-    justify-content: space-between;
+/* Dark-mode kind chips — boost contrast */
+@media (prefers-color-scheme: dark) {
+    .kind-chip { filter: brightness(1.15) saturate(1.1); }
 }
-
-.left-buttons {
-    display: flex;
-    gap: 8px;
-    align-items: baseline;
+.dark .kind-chip { filter: brightness(1.15) saturate(1.1); }
+#submit_btn button {
+    padding: 0.55rem 1.4rem !important;
+    font-weight: 600 !important;
+    font-size: 0.9rem !important;
+    border-radius: 8px !important;
+    background: #f59e0b !important;
+    color: white !important;
+    border: none !important;
+    margin-top: 0.5rem !important;
+    width: auto !important;
+    align-self: flex-start;
+    box-shadow: 0 2px 8px rgba(245, 158, 11, 0.25) !important;
 }
-
-.right-buttons {
-    display: flex;
-    gap: 8px;
-    align-items: baseline;
+#submit_btn button:hover {
+    background: #d97706 !important;
+    box-shadow: 0 4px 12px rgba(245, 158, 11, 0.35) !important;
 }
+#vote_status { margin-top: 0.5rem; text-align: center; }
+#vote_trigger_input { display: none !important; }
 
-.vote-button.upvote:hover {
-    background: #28a745;
-    color: white;
+/* Misc */
+.gr-accordion-header {
+    font-size: 1.0rem;
+    font-weight: 600;
+    cursor: pointer;
 }
 
-.vote-button.downvote:hover {
-    background: #dc3545;
-    color: white;
+/* Progress overlay center */
+div.gradio-modal[aria-label="progress"] {
+    position: fixed !important;
+    top: 50% !important; left: 50% !important;
+    transform: translate(-50%, -50%) !important;
+    z-index: 2000 !important;
+    width: clamp(260px, 70vw, 440px) !important;
+    max-height: 160px !important;
+    padding: 20px 24px !important;
+    background: var(--card-bg) !important;
+    border: 1px solid var(--border) !important;
+    border-radius: 12px !important;
+    box-shadow: 0 8px 28px rgba(0,0,0,.18) !important;
 }
 
-.vote-button.voted {
+/* Acknowledgements */
+.acknowledgements {
+    margin-top: 2rem;
+    padding: 1rem 0 0.5rem;
+    border-top: 1px solid var(--border);
+    text-align: center;
+}
+.ack-title {
+    font-size: 0.72rem;
+    font-weight: 600;
+    text-transform: uppercase;
+    letter-spacing: 0.1em;
+    color: var(--muted);
+    margin-bottom: 0.35rem;
+}
+.ack-body {
+    font-size: 0.78rem;
+    color: var(--muted);
+    line-height: 1.6;
+}
+.ack-body a {
+    color: var(--primary);
+    text-decoration: none;
+    opacity: 0.75;
+    transition: opacity .12s ease;
+}
+.ack-body a:hover {
     opacity: 1;
-    transform: scale(1.1);
+    text-decoration: underline;
 }
+"""
 
-.vote-button.upvote.voted {
-    background: #28a745;
-    color: white;
-}
 
-.vote-button.downvote.voted {
-    background: #dc3545;
-    color: white;
+HEAD_HTML = """
+<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.16.8/dist/katex.min.css">
+<link href="https://fonts.googleapis.com/css2?family=Inter:wght@400;500;600;700&family=JetBrains+Mono:wght@400;500&display=swap" rel="stylesheet">
+<script src="https://cdn.jsdelivr.net/npm/katex@0.16.8/dist/katex.min.js"></script>
+<style>
+  body, .gradio-container { font-family: 'Inter', -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, sans-serif; }
+</style>
+<script>
+function renderKatex() {
+    if (typeof katex === 'undefined') { setTimeout(renderKatex, 400); return; }
+    document.querySelectorAll('.math-content:not([data-katex-processed])').forEach(function(el) {
+        el.setAttribute('data-katex-processed', 'true');
+        const text = el.textContent;
+        if (!text || (text.indexOf('$') === -1 && text.indexOf('\\\\(') === -1)) return;
+        let html = '';
+        let i = 0;
+        while (i < text.length) {
+            if (text[i] === '$' && text[i+1] === '$') {
+                const end = text.indexOf('$$', i + 2);
+                if (end === -1) { html += text.substring(i); break; }
+                try {
+                    html += katex.renderToString(text.substring(i + 2, end), { throwOnError: false, displayMode: true });
+                } catch (e) { html += '$$' + escapeHtml(text.substring(i + 2, end)) + '$$'; }
+                i = end + 2;
+            } else if (text[i] === '$') {
+                const end = text.indexOf('$', i + 1);
+                if (end === -1) { html += escapeHtml(text.substring(i)); break; }
+                try {
+                    html += katex.renderToString(text.substring(i + 1, end), { throwOnError: false });
+                } catch (e) { html += '$' + escapeHtml(text.substring(i + 1, end)) + '$'; }
+                i = end + 1;
+            } else {
+                html += escapeHtml(text[i]);
+                i++;
+            }
+        }
+        el.innerHTML = html;
+    });
 }
-
-/* Additional dark mode support */
-@media (prefers-color-scheme: dark) {
-    .lf-title{
-        color:#e0e0e0 !important;
-    }
-    
-    #vote_radio label{
-        border:1px solid #555;
-        background:#2a2a2a;
-        color:#e0e0e0;
-    }
-    
-    #vote_radio input[type="radio"]:checked + label{
-        background:#0066ff;
-        color:#fff;
-        border-color:#0066ff;
-    }
-    
-    /* Progress bar dark mode */
-    .gradio-container .progress-bar {
-        background: #2a2a2a !important;
-        border: 1px solid #555 !important;
-    }
-    
-    .gradio-container .progress-bar .progress-text {
-        color: #e0e0e0 !important;
-    }
-    
-    .gradio-container .progress-bar .progress-level {
-        background: #444 !important;
-    }
-    
-    /* Copy button dark mode */
-    .copy-button {
-        background: rgba(255, 255, 255, 0.1);
-        color: #ccc;
-        border-color: #555;
-    }
-    
-    .copy-button:hover {
-        background: rgba(255, 255, 255, 0.2);
-        color: #fff;
-    }
-    
-    .copy-button:active {
-        background: rgba(255, 255, 255, 0.3);
-        color: #fff;
-    }
-    
-    /* Query input dark mode */
-    #query_input textarea {
-        background: #2a2a2a !important;
-        color: #e0e0e0 !important;
-    }
-    
-    #query_input textarea:focus {
-        border-color: #0066ff !important;
-        box-shadow: 0 0 0 2px rgba(0, 102, 255, 0.2) !important;
-    }
-    
-    /* Vote buttons dark mode */
-    .vote-button {
-        border-color: #555 !important;
-        background: #2a2a2a !important;
-    }
-    
-    .vote-button.upvote {
-        color: #4ade80 !important;
-        border-color: #4ade80 !important;
-    }
-    
-    .vote-button.downvote {
-        color: #f87171 !important;
-        border-color: #f87171 !important;
-    }
-    
-    /* Doc button dark mode */
-    .doc-button {
-        background: rgba(96, 165, 250, 0.1) !important;
-        border-color: #60a5fa !important;
-        color: #60a5fa !important;
-    }
-    
-    .doc-button:hover {
-        background: #60a5fa !important;
-        color: #000 !important;
-    }
-    
-    .vote-button.upvote:hover {
-        background: #4ade80 !important;
-        color: #000 !important;
+function escapeHtml(s) { return s.replace(/[&<>"']/g, function(c) { return ({'&':'&amp;','<':'&lt;','>':'&gt;','"':'&quot;',"'":'&#39;'})[c]; }); }
+setInterval(renderKatex, 1200);
+
+function copyToClipboard(text, button) {
+    const ok = (b) => {
+        const t = b.innerHTML; b.innerHTML = '✓ Copied'; b.style.color = '#10b981';
+        setTimeout(() => { b.innerHTML = t; b.style.color = ''; }, 1200);
+    };
+    if (navigator.clipboard && window.isSecureContext) {
+        navigator.clipboard.writeText(text).then(() => ok(button)).catch(() => fb(text, button));
+    } else { fb(text, button); }
+    function fb(t, b) {
+        const ta = document.createElement('textarea');
+        ta.value = t; ta.style.position = 'fixed'; ta.style.left = '-9999px';
+        document.body.appendChild(ta); ta.select();
+        try { document.execCommand('copy'); ok(b); } catch(e) {}
+        document.body.removeChild(ta);
     }
-    
-    .vote-button.downvote:hover {
-        background: #f87171 !important;
-        color: #000 !important;
-    }
-    
-    .vote-button.upvote.voted {
-        background: #4ade80 !important;
-        color: #000 !important;
-    }
-    
-    .vote-button.downvote.voted {
-        background: #f87171 !important;
-        color: #000 !important;
-    }
-    
-    /* Vote feedback styling */
-    #vote_feedback {
-        margin-top: 1rem;
-        text-align: center;
-    }
-    
-    #vote_feedback .markdown {
-        background: #d4edda !important;
-        border: 1px solid #c3e6cb !important;
-        border-radius: 8px !important;
-        padding: 12px 16px !important;
-        color: #155724 !important;
-        font-weight: 500 !important;
-        margin: 0 !important;
-        transition: opacity 0.5s ease !important;
-        opacity: 1 !important;
-    }
-    
-    /* Error styling for vote feedback */
-    #vote_feedback .markdown:has-text("ERROR"),
-    #vote_feedback .markdown[data-error="true"] {
-        background: #f8d7da !important;
-        border-color: #f5c6cb !important;
-        color: #721c24 !important;
+}
+
+function toggleDesc(btn) {
+    const parent = btn.parentElement;
+    const preview = parent.querySelector('.desc-preview');
+    const full = parent.querySelector('.desc-full');
+    const showingFull = !full.hasAttribute('hidden');
+    if (showingFull) {
+        full.setAttribute('hidden', '');
+        preview.removeAttribute('hidden');
+        btn.textContent = 'Read more';
+    } else {
+        full.removeAttribute('hidden');
+        preview.setAttribute('hidden', '');
+        btn.textContent = 'Show less';
     }
-    
-    /* Dark mode for vote feedback */
-    @media (prefers-color-scheme: dark) {
-        #vote_feedback .markdown {
-            background: #1e3a2e !important;
-            border-color: #2d5a3d !important;
-            color: #a7d4b4 !important;
-        }
-        
-        /* Error styling in dark mode */
-        #vote_feedback .markdown:has-text("ERROR"),
-        #vote_feedback .markdown[data-error="true"] {
-            background: #3d1a1a !important;
-            border-color: #5a2d2d !important;
-            color: #ff9999 !important;
+}
+
+function voteOnResultSafe(button, voteDecision) {
+    const formal = button.getAttribute('data-formal');
+    const query  = button.getAttribute('data-query');
+    const system = button.getAttribute('data-system');
+    const rank   = parseInt(button.getAttribute('data-rank'));
+    button.classList.add('voted');
+    const sibling = button.parentElement.querySelector(
+        '.vote-btn.' + (voteDecision === 'Upvote' ? 'downvote' : 'upvote')
+    );
+    if (sibling) { sibling.style.opacity = '0.35'; sibling.style.pointerEvents = 'none'; }
+    const data = JSON.stringify({
+        formal_statement: formal, vote_decision: voteDecision,
+        query: query, system: system, rank: rank
+    });
+    const container = document.querySelector('#vote_trigger_input');
+    if (container) {
+        const input = container.querySelector('textarea') || container.querySelector('input[type="text"]');
+        if (input) {
+            input.value = data;
+            input.dispatchEvent(new Event('input', { bubbles: true }));
+            input.dispatchEvent(new Event('change', { bubbles: true }));
+            setTimeout(function() {
+                const inp = container.querySelector('textarea') || container.querySelector('input[type="text"]');
+                if (inp) { inp.value=''; inp.dispatchEvent(new Event('input',{bubbles:true})); }
+            }, 2500);
         }
     }
 }
-"""
 
-with gr.Blocks(
-    title="Lean Finder Retrieval", 
-    css=CUSTOM_CSS,
-    head="""
-    <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.16.8/dist/katex.min.css">
-    <script src="https://cdn.jsdelivr.net/npm/katex@0.16.8/dist/katex.min.js"></script>
-    <script>
-    function renderKatex() {
-        if (typeof katex === 'undefined') {
-            setTimeout(renderKatex, 500);
-            return;
-        }
-        
-        const spans = document.querySelectorAll('span:not([data-katex-processed])');
-        
-        spans.forEach(function(span) {
-            const text = span.textContent;
-            if (text && text.includes('$')) {
-                span.setAttribute('data-katex-processed', 'true');
-                
-                let mathExpressions = [];
-                
-                // Find inline math $...$
-                let pos = 0;
-                while (pos < text.length) {
-                    const start = text.indexOf('$', pos);
-                    if (start === -1) break;
-                    const end = text.indexOf('$', start + 1);
-                    if (end === -1) break;
-                    
-                    const isDisplayMath = (start > 0 && text[start - 1] === '$') || 
-                                         (end < text.length - 1 && text[end + 1] === '$');
-                    
-                    if (!isDisplayMath) {
-                        mathExpressions.push({
-                            start: start,
-                            end: end + 1,
-                            content: text.substring(start + 1, end),
-                            type: 'inline'
-                        });
-                        pos = end + 1;
-                    } else {
-                        pos = start + 1;
-                    }
-                }
-                
-                // Find display math $$...$$
-                pos = 0;
-                while (pos < text.length) {
-                    const start = text.indexOf('$$', pos);
-                    if (start === -1) break;
-                    const end = text.indexOf('$$', start + 2);
-                    if (end === -1) break;
-                    
-                    mathExpressions.push({
-                        start: start,
-                        end: end + 2,
-                        content: text.substring(start + 2, end),
-                        type: 'display'
-                    });
-                    pos = end + 2;
-                }
-                
-                mathExpressions.sort((a, b) => a.start - b.start);
-                
-                // Remove overlapping expressions
-                let filtered = [];
-                for (let expr of mathExpressions) {
-                    let shouldAdd = true;
-                    for (let j = 0; j < filtered.length; j++) {
-                        const existing = filtered[j];
-                        if (!(expr.end <= existing.start || expr.start >= existing.end)) {
-                            if (expr.type === 'display' && existing.type === 'inline') {
-                                filtered.splice(j, 1);
-                                j--;
-                            } else {
-                                shouldAdd = false;
-                                break;
-                            }
-                        }
-                    }
-                    if (shouldAdd) filtered.push(expr);
-                }
-                
-                if (filtered.length > 0) {
-                    let newContent = document.createDocumentFragment();
-                    let lastPos = 0;
-                    
-                    filtered.forEach(function(expr) {
-                        if (expr.start > lastPos) {
-                            newContent.appendChild(document.createTextNode(text.substring(lastPos, expr.start)));
-                        }
-                        
-                        try {
-                            const mathElement = document.createElement('span');
-                            mathElement.innerHTML = katex.renderToString(expr.content, {
-                                throwOnError: false,
-                                displayMode: expr.type === 'display'
-                            });
-                            newContent.appendChild(mathElement);
-                        } catch (e) {
-                            const fallback = expr.type === 'display' ? '$$' + expr.content + '$$' : '$' + expr.content + '$';
-                            newContent.appendChild(document.createTextNode(fallback));
-                        }
-                        
-                        lastPos = expr.end;
-                    });
-                    
-                    if (lastPos < text.length) {
-                        newContent.appendChild(document.createTextNode(text.substring(lastPos)));
-                    }
-                    
-                    span.innerHTML = '';
-                    span.appendChild(newContent);
+/* --- Auto-scroll to vote area after search results load --- */
+function lf_scrollToVote() {
+    const voteArea = document.querySelector('#vote_area');
+    const resultsEl = document.querySelector('.arena-grid') || document.querySelector('.results-single');
+    const target = voteArea && voteArea.offsetParent !== null ? voteArea : resultsEl;
+    if (target) {
+        setTimeout(function() {
+            target.scrollIntoView({ behavior: 'smooth', block: 'start' });
+        }, 120);
+    }
+}
+// Observe the results HTML container for changes (Gradio replaces innerHTML)
+(function() {
+    const observer = new MutationObserver(function(mutations) {
+        for (const m of mutations) {
+            if (m.type === 'childList' && m.addedNodes.length) {
+                const container = m.target.closest ? m.target : m.target.parentElement;
+                if (container && (container.querySelector('.arena-grid') || container.querySelector('.results-single'))) {
+                    lf_scrollToVote();
+                    break;
                 }
             }
-        });
-    }
-    
-    setTimeout(renderKatex, 1000);
-    setTimeout(renderKatex, 3000);
-    setTimeout(renderKatex, 5000);
-    
-    function copyToClipboard(text, button) {
-        if (navigator.clipboard && window.isSecureContext) {
-            navigator.clipboard.writeText(text).then(function() {
-                showCopySuccess(button);
-            }).catch(function() {
-                fallbackCopy(text, button);
-            });
-        } else {
-            fallbackCopy(text, button);
         }
-    }
-    
-    function fallbackCopy(text, button) {
-        const textArea = document.createElement('textarea');
-        textArea.value = text;
-        textArea.style.position = 'fixed';
-        textArea.style.left = '-9999px';
-        textArea.style.top = '-9999px';
-        document.body.appendChild(textArea);
-        textArea.focus();
-        textArea.select();
-        
-        try {
-            document.execCommand('copy');
-            showCopySuccess(button);
-        } catch (err) {
-            showCopyError(button);
+    });
+    // Start observing once Gradio has mounted
+    function startObserving() {
+        const app = document.querySelector('.gradio-container');
+        if (app) {
+            observer.observe(app, { childList: true, subtree: true });
+        } else {
+            setTimeout(startObserving, 500);
         }
-        
-        document.body.removeChild(textArea);
-    }
-    
-    function showCopySuccess(button) {
-        const originalText = button.innerHTML;
-        button.innerHTML = '✓';
-        button.style.color = '#28a745';
-        setTimeout(function() {
-            button.innerHTML = originalText;
-            button.style.color = '';
-        }, 1000);
-    }
-    
-    function showCopyError(button) {
-        const originalText = button.innerHTML;
-        button.innerHTML = '✗';
-        button.style.color = '#dc3545';
-        setTimeout(function() {
-            button.innerHTML = originalText;
-            button.style.color = '';
-        }, 1000);
     }
-    
-    function voteOnResultSafe(button, voteDecision) {
-        const formalStatement = button.getAttribute('data-formal');
-        const query = button.getAttribute('data-query');
-        const system = button.getAttribute('data-system');
-        const rank = parseInt(button.getAttribute('data-rank'));
-        
-        button.classList.add('voted');
-        
-        const otherButton = button.parentElement.querySelector('.vote-button:not(.' + (voteDecision === 'Upvote' ? 'upvote' : 'downvote') + ')');
-        if (otherButton) {
-            otherButton.style.opacity = '0.3';
-            otherButton.style.pointerEvents = 'none';
-        }
-        
-        const originalText = button.innerHTML;
-        button.innerHTML = voteDecision === 'Upvote' ? '👍✓' : '👎✓';
-        setTimeout(function() {
-            button.innerHTML = originalText;
-        }, 2000);
-        
-        const voteData = JSON.stringify({
-            formal_statement: formalStatement,
-            vote_decision: voteDecision,
-            query: query,
-            system: system,
-            rank: rank
-        });
-        
-        const voteContainer = document.querySelector('#vote_trigger_input');
-        if (voteContainer) {
-            const input = voteContainer.querySelector('textarea') || voteContainer.querySelector('input[type="text"]');
-            if (input) {
-                input.value = voteData;
-                input.dispatchEvent(new Event('input', { bubbles: true, cancelable: true }));
-                input.dispatchEvent(new Event('change', { bubbles: true, cancelable: true }));
-                
-                setTimeout(function() {
-                    const feedbackElement = document.querySelector('#vote_feedback .markdown');
-                    if (feedbackElement) {
-                        if (feedbackElement.textContent.includes('ERROR')) {
-                            feedbackElement.setAttribute('data-error', 'true');
-                        } else {
-                            feedbackElement.removeAttribute('data-error');
-                        }
-                    }
-                }, 100);
-                
-                setTimeout(function() {
-                    const feedbackElement = document.querySelector('#vote_feedback .markdown');
-                    if (feedbackElement && feedbackElement.textContent.trim()) {
-                        feedbackElement.style.opacity = '0';
-                        setTimeout(function() {
-                            const input = voteContainer.querySelector('textarea') || voteContainer.querySelector('input[type="text"]');
-                            if (input) {
-                                input.value = '';
-                                input.dispatchEvent(new Event('input', { bubbles: true }));
-                            }
-                        }, 500);
-                    }
-                }, 4000);
+    startObserving();
+})();
+
+/* --- Enter key to search --- */
+(function() {
+    function attachEnter() {
+        const container = document.querySelector('#query_input');
+        if (!container) { setTimeout(attachEnter, 500); return; }
+        const textarea = container.querySelector('textarea');
+        if (!textarea) { setTimeout(attachEnter, 500); return; }
+        textarea.addEventListener('keydown', function(e) {
+            // Enter (without Shift) triggers search
+            if (e.key === 'Enter' && !e.shiftKey) {
+                e.preventDefault();
+                const btn = document.querySelector('#search_btn button');
+                if (btn) btn.click();
             }
-        }
+        });
     }
-    
-    function voteOnResult(formalStatement, voteDecision, query, system, rank, button) {
-        const tempButton = document.createElement('button');
-        tempButton.setAttribute('data-formal', formalStatement);
-        tempButton.setAttribute('data-query', query);
-        tempButton.setAttribute('data-system', system);
-        tempButton.setAttribute('data-rank', rank);
-        tempButton.className = button.className;
-        tempButton.parentElement = button.parentElement;
-        voteOnResultSafe(tempButton, voteDecision);
+    if (document.readyState === 'loading') {
+        document.addEventListener('DOMContentLoaded', attachEnter);
+    } else {
+        attachEnter();
     }
-    
-        setInterval(function() {
-        if (document.querySelector('table')) {
-            renderKatex();
-        }
-    }, 3000);
-    </script>
-    """
-) as demo:
-    with gr.Column(elem_id="lf_header"):
-        gr.Image(
-            value="lean_finder_logo.png",
-            show_label=False,
-            interactive=False,
-            container=False,
-            show_download_button=False,
-            height=60,
-            elem_id="lf_logo",
-        )
-        gr.HTML('<h1 class="lf-title">Lean Finder: Semantic Search for Mathlib That Understands User Intents</h1>')
+})();
+</script>
+"""
+
 
-    with gr.Accordion("Supported query types(click for details): Informalized statement, User question, Proof state, Statement definition", open=False):
+with gr.Blocks(title="Lean Finder — Semantic Search for Mathlib",
+               css=CUSTOM_CSS, head=HEAD_HTML, theme=gr.themes.Soft(
+                   primary_hue="indigo",
+                   neutral_hue="slate",
+               )) as demo:
+
+    gr.HTML(
+        '<div class="lf-hero">'
+        '  <div class="lf-hero-main">'
+        '    <img class="lf-logo" src="/file=lean_finder_logo.png" alt="Lean Finder logo">'
+        '    <div class="lf-hero-text">'
+        '      <div class="lf-title">Lean Finder</div>'
+        '      <div class="lf-tagline">Semantic Search For Mathlib That Understands User Intents</div>'
+        '    </div>'
+        '  </div>'
+        '  <a class="lf-hero-badge" href="https://arxiv.org/pdf/2510.15940" target="_blank">'
+        '    Paper Link'
+        '  </a>'
+        '</div>'
+    )
+
+    with gr.Accordion("📘 What can I search for? (4 query types + Mathlib versions)", open=False):
         gr.Markdown(INSTRUCTIONS_MD)
 
-    gr.Markdown("Currently using Mathlib v4.16.0")
+    query_box = gr.Textbox(
+        label="Your query",
+        lines=4, max_lines=18,
+        placeholder="Describe the Lean statement you're looking for, ask a question, paste a proof state, or sketch a definition…",
+        elem_id="query_input",
+        show_copy_button=True,
+    )
+
+    with gr.Row(elem_id="controls_row", equal_height=True):
+        version_sel = gr.Dropdown(
+            MATHLIB_VERSIONS,
+            value=DEFAULT_VERSION,
+            label="Mathlib version",
+            scale=1, min_width=140, container=True,
+        )
+        topk_slider = gr.Slider(
+            label="Results",
+            minimum=1, maximum=20, step=1, value=5,
+            scale=2, min_width=180,
+        )
+        mode_sel = gr.Radio(
+            ["Arena", "Normal"], value="Arena", label="Mode",
+            scale=2, min_width=180,
+        )
 
+    run_btn = gr.Button("Search", elem_id="search_btn", variant="primary")
 
+    mode_description = gr.Markdown(
+        "_**Arena mode** — Lean Finder is compared side-by-side with another model. "
+        "The two models are shown as **Retriever A** and **Retriever B** in random order so the comparison stays fair. "
+        "Vote for the better set overall, or 👍/👎 individual results. "
+        "Your votes help us improve Lean Finder — no personally identifiable information is stored._",
+        elem_id="mode_description",
+    )
 
-    with gr.Row():
-        query_box   = gr.Textbox(label="Query", lines=4, max_lines=20,
-                                 placeholder="Type your query here …", 
-                                 elem_id="query_input")
-        topk_slider = gr.Slider(label="Number of results", minimum=1, maximum=50, step=1, value=5)
+    with gr.Row(elem_id="vote_area", visible=False) as vote_row:
         with gr.Column():
-            mode_sel    = gr.Radio(["Arena", "Normal"], value="Arena", label="Mode")
-            mode_description = gr.Markdown("Arena mode: Compare retrieval results from Lean Finder with another retriever and vote.\n By voting, you agree that your responses may be used to help improve Lean Finder. We only collect the voting results; no identifiable information is stored.")
-    
-    run_btn = gr.Button("Retrieve")
-
-    with gr.Row(elem_id="vote_area"):
-        with gr.Column(elem_id="vote_radio_col"):
+            gr.HTML('<div class="vote-area-label">Cast your vote</div>')
             vote_radio = gr.Radio(
                 VOTE_UI,
-                label="Which result is better?",
-                visible=False,
-                elem_id="vote_radio"
+                label="Which set of results did better overall?",
+                elem_id="vote_radio",
             )
             submit_btn = gr.Button(
                 "Submit vote",
-                visible=False,
                 elem_id="submit_btn",
-                variant="primary"
             )
     vote_status = gr.Markdown("", visible=False, elem_id="vote_status")
 
-    results_html = gr.HTML()
-
-    gr.HTML('''
-    <div style="text-align: center; margin: 0.75rem 0;">
-        <a href="https://arxiv.org/abs/2510.15940" target="_blank" style="
-            display: inline-flex;
-            align-items: center;
-            gap: 0.4rem;
-            padding: 0.4rem 0.8rem;
-            background: linear-gradient(135deg, #667eea 0%, #764ba2 100%);
-            color: white;
-            text-decoration: none;
-            border-radius: 20px;
-            font-weight: 500;
-            font-size: 0.85rem;
-            box-shadow: 0 2px 8px rgba(102, 126, 234, 0.25);
-            transition: all 0.3s ease;
-            border: none;
-        " onmouseover="this.style.transform='translateY(-1px)'; this.style.boxShadow='0 4px 12px rgba(102, 126, 234, 0.35)'" 
-            onmouseout="this.style.transform='translateY(0px)'; this.style.boxShadow='0 2px 8px rgba(102, 126, 234, 0.25)'">
-            <span style="font-size: 1rem;">📄</span>
-            Read our paper for details about Lean Finder
-        </a>
-    </div>
-''', elem_id="paper_link")
-    
-    # Hidden component for individual vote triggers
-    vote_trigger = gr.Textbox(visible=False, elem_id="vote_trigger_input")
+    results_html = gr.HTML(
+        '<div class="empty-state">Type a query above and hit <b>Search</b> '
+        'to see Lean statements from Mathlib.</div>'
+    )
+
+    # Hidden vote bridge
+    vote_trigger = gr.Textbox(visible=True, elem_id="vote_trigger_input")
     vote_feedback = gr.Markdown("", visible=True, elem_id="vote_feedback")
 
-    # per-session state
+    gr.HTML(
+        '<div class="acknowledgements">'
+        '  <div class="ack-title">Acknowledgements</div>'
+        '  <div class="ack-body">'
+        '    Lean Finder is built on open-source projects like '
+        '    <a href="https://github.com/frenzymath/jixia" target="_blank">Jixia</a> and '
+        '    <a href="https://github.com/lean-dojo/leandojo" target="_blank">LeanDojo</a>. '
+        '    We were inspired by '
+        '    <a href="https://leansearch.net/" target="_blank">LeanSearch</a>, and we '
+        '    use LeanSearch in our Arena mode to let users compare results. '
+        '    Thanks to the creators of these awesome tools!'
+        '  </div>'
+        '</div>'
+    )
+
+    # Session state
     st_query = gr.State("")
-    st_ret_a_js = gr.State({})
-    st_ret_b_js = gr.State([])
-    st_sys1_is_a = gr.State(True)  # Track which system is A in current session
+    st_version = gr.State(DEFAULT_VERSION)
+    st_ret_a = gr.State([])
+    st_ret_b = gr.State([])
+    st_a_source = gr.State(LEAN_FINDER)
+    st_b_source = gr.State(LEAN_SEARCH)
+
+    def retrieve(query: str, k: int, version: str, mode: str, progress=gr.Progress()):
+        query = (query or "").strip()
+        hide_radio  = gr.update(visible=False, value=None)
+        hide_status = gr.update(visible=False, value="")
+        hide_row    = gr.update(visible=False)
 
-    def retrieve(query: str, k: int, mode: str, progress=gr.Progress()):
-        query = query.strip()
         if not query:
-            hide = gr.update(visible=False, value="")
-            return "<p>Please enter a query.</p>", query, {}, [], hide, hide, hide, True
+            return (
+                '<div class="empty-state">Please enter a query.</div>',
+                "", version, [], [], LEAN_FINDER, LEAN_SEARCH,
+                hide_radio, hide_status, hide_row,
+            )
 
+        # Call Lean Finder, with cold-start retry loop preserved
         try:
-            sys1_json = _call_retriever_system1({"inputs": query, "top_k": k}).get("results", [])
+            lf_raw = _call_lean_finder(query, k, version)
         except RuntimeError:
-            payload = {"inputs": query, "top_k": k}
-            hide = gr.update(visible=False, value="")
-            progress(0, desc="Please wait about 2 minutes. The Lean Finder service is starting up. Results will be displayed automatically once Lean Finder is ready.")
-            
-            start_time = time.time()
-            timeout_duration = 300
-            progress_phase1_duration = 120
-            last_progress_update = 0
-            
-            while time.time() - start_time < timeout_duration:
-                elapsed_time = time.time() - start_time
-                if elapsed_time - last_progress_update >= 10:
-                    if elapsed_time < progress_phase1_duration:
-                        progress(elapsed_time / progress_phase1_duration, desc="Please wait about 2 minutes. The Lean Finder service is starting up. Results will be displayed automatically once Lean Finder is ready.")
-                    else:
-                        progress(1.0, desc="Experiencing a slow start. Please wait a little longer — the content will be displayed once Lean Finder is ready.")
-                    last_progress_update = elapsed_time
-                
-                time.sleep(1)
+            progress(0, desc="Lean Finder is warming up. Results will appear in ~1–2 min.")
+            start = time.time()
+            lf_raw = None
+            timeout_s = 300
+            phase1 = 120
+            while time.time() - start < timeout_s:
+                elapsed = time.time() - start
+                if elapsed < phase1:
+                    progress(elapsed / phase1, desc="Lean Finder is warming up. Results will appear in ~1–2 min.")
+                else:
+                    progress(1.0, desc="Slow cold start — almost ready…")
                 try:
-                    sys1_json = _call_retriever_system1(payload).get("results", [])
+                    lf_raw = _call_lean_finder(query, k, version)
                     break
                 except RuntimeError:
-                    continue
-            else:
-                error_message = "<div style='background-color: #f8d7da; border: 1px solid #f5c6cb; padding: 10px; margin-bottom: 15px; border-radius: 5px; color: #721c24;'><strong>Error:</strong> Lean Finder service is currently unavailable. Please contact the maintainer of this project at mike_lu@sfu.ca</div>"
-                return error_message, query, {}, [], hide, hide, hide, True
+                    time.sleep(2)
+            if lf_raw is None:
+                err = (
+                    '<div class="empty-state" style="color:#b91c1c;border-color:#fecaca;background:#fef2f2;">'
+                    '⚠️ Lean Finder is currently unavailable. Please try again in a moment '
+                    'or contact <a href="mailto:mike_lu@sfu.ca">mike_lu@sfu.ca</a>.'
+                    '</div>'
+                )
+                return err, query, version, [], [], LEAN_FINDER, LEAN_SEARCH, hide_radio, hide_status, hide_row
+
+        lf = _norm_lean_finder(lf_raw)
 
         if mode == "Normal":
-            sys1_html = _render_system1_results(sys1_json, title="Lean Finder", query=query)
-            hide    = gr.update(visible=False, value="")
-            return sys1_html, query, sys1_json, [], hide, hide, hide, True
+            return (
+                _render_single(lf, query, version),
+                query, version, lf, [], LEAN_FINDER, LEAN_SEARCH,
+                hide_radio, hide_status, hide_row,
+            )
 
+        # Arena mode
         try:
-            sys2_json = _call_retriever_system2(query, k)
+            ls_raw = _call_lean_search(query, k)
+            ls = _norm_lean_search(ls_raw)
         except RuntimeError:
-            error_message = "<div style='background-color: #fff3cd; border: 1px solid #ffeaa7; padding: 10px; margin-bottom: 15px; border-radius: 5px; color: #856404;'><strong>Notice:</strong> The other retriever Lean Search is currently unavailable, falling back to Normal mode.</div>"
-            sys1_html = _render_system1_results(sys1_json, title="Lean Finder", query=query)
-            fallback_html = error_message + sys1_html
-            hide = gr.update(visible=False, value="")
-            return fallback_html, query, sys1_json, [], hide, hide, hide, True
-        
-        sys1_is_a = random.choice([True, False])
-        if sys1_is_a:
-            ret_a_json, ret_b_json = sys1_json, sys2_json
-            ret_a_html = _render_system1_results(ret_a_json, title="Retriever A", query=query)
-            ret_b_html = _render_system2_results(ret_b_json, title="Retriever B", query=query)
+            notice = (
+                '<div class="empty-state" style="border-color:#fde68a;background:#fffbeb;color:#92400e;">'
+                '⚠️ LeanSearch is unavailable right now — showing Lean Finder results only.'
+                '</div>'
+            )
+            return (
+                notice + _render_single(lf, query, version),
+                query, version, lf, [], LEAN_FINDER, LEAN_SEARCH,
+                hide_radio, hide_status, hide_row,
+            )
+
+        # Random shuffle of A/B so the user can't tell which is which
+        lf_is_a = random.choice([True, False])
+        if lf_is_a:
+            ret_a, ret_b = lf, ls
+            a_src, b_src = LEAN_FINDER, LEAN_SEARCH
         else:
-            ret_a_json, ret_b_json = sys2_json, sys1_json
-            ret_a_html = _render_system2_results(ret_a_json, title="Retriever A", query=query)
-            ret_b_html = _render_system1_results(ret_b_json, title="Retriever B", query=query)
-
-        page = (
-            "<div style='display:flex; gap:0.5rem;'>"
-            f"<div style='flex:1 1 0;'>{ret_a_html}</div>"
-            f"<div style='flex:1 1 0;'>{ret_b_html}</div>"
-            "</div>"
+            ret_a, ret_b = ls, lf
+            a_src, b_src = LEAN_SEARCH, LEAN_FINDER
+
+        return (
+            _render_arena(ret_a, ret_b, a_src, b_src, query, version),
+            query, version, ret_a, ret_b, a_src, b_src,
+            gr.update(visible=True, value=None),
+            gr.update(visible=False, value=""),
+            gr.update(visible=True),
         )
-        show_radio  = gr.update(visible=True,  value=None)
-        hide_status = gr.update(visible=False, value="")
-        show_btn    = gr.update(visible=True)
-        return page, query, ret_a_json, ret_b_json, show_radio, show_btn, hide_status, sys1_is_a
 
     run_btn.click(
         retrieve,
-        inputs=[query_box, topk_slider, mode_sel],
-        outputs=[results_html, st_query, st_ret_a_js, st_ret_b_js,
-                 vote_radio, submit_btn, vote_status, st_sys1_is_a],
+        inputs=[query_box, topk_slider, version_sel, mode_sel],
+        outputs=[results_html, st_query, st_version, st_ret_a, st_ret_b,
+                 st_a_source, st_b_source,
+                 vote_radio, vote_status, vote_row],
     )
 
-    def _reset_ui_on_mode_change(mode):
+    def _on_mode_change(mode):
         if mode == "Arena":
-            description = "Arena mode: Compare retrieval results from Lean Finder with another retriever and vote."
+            desc = (
+                "_**Arena mode** — Lean Finder vs. another model, shown in random order as Retriever A / B. "
+                "Vote for the better set or 👍/👎 individual results. "
+                "Votes help improve Lean Finder — we do not collect IP addresses or any personally identifiable information._"
+            )
         else:
-            description = "Normal mode: Standard retrieval from Lean Finder."
-        
+            desc = (
+                "_Normal mode — Lean Finder only. Quick results, no voting._"
+            )
         return (
-            "",
+            '<div class="empty-state">Type a query above and hit <b>Search</b> '
+            'to see Lean statements from Mathlib.</div>',
             gr.update(visible=False, value=None),
             gr.update(visible=False),
             gr.update(visible=False, value=""),
-            description,
+            desc,
         )
 
     mode_sel.change(
-        _reset_ui_on_mode_change,
+        _on_mode_change,
         inputs=mode_sel,
-        outputs=[results_html, vote_radio, submit_btn, vote_status, mode_description],
+        outputs=[results_html, vote_radio, vote_row, vote_status, mode_description],
     )
 
     submit_btn.click(
         _save_vote,
-        inputs=[vote_radio, st_query, st_ret_a_js, st_ret_b_js, st_sys1_is_a],
-        outputs=vote_status
+        inputs=[vote_radio, st_query, st_version, st_ret_a, st_ret_b,
+                st_a_source, st_b_source],
+        outputs=vote_status,
     )
-    
-    def handle_individual_vote(vote_data: str, query: str, ret_a_js: Dict[str, Any], ret_b_js: List[Dict[str, Any]], sys1_is_a: bool) -> str:
+
+    def handle_individual_vote(vote_data: str, query: str, version: str,
+                               ret_a: List[Dict[str, Any]], ret_b: List[Dict[str, Any]],
+                               a_source: str, b_source: str) -> str:
         if not vote_data:
             return ""
         try:
             data = json.loads(vote_data)
-            
+            # The on-card "system" attribute holds the real source name (Lean Finder / LeanSearch)
+            # because we already pass it through when rendering arena cards.
+            system = data.get("system", "")
             payload = {
-                "retriever_a": ret_a_js,
-                "retriever_b": ret_b_js,
-                "sys1_is_a": sys1_is_a,
-                "individual_vote": data
+                "retriever_a": ret_a,
+                "retriever_b": ret_b,
+                "a_source": a_source,
+                "b_source": b_source,
+                "individual_vote": data,
             }
-            
             _save_individual_vote(
                 data["formal_statement"],
                 data["vote_decision"],
                 data["query"],
-                data["system"],
+                system,
                 data["rank"],
-                payload
+                version,
+                payload,
             )
-            return f"**{data['vote_decision']} recorded!** (Rank {data['rank']})"
+            return f"✅ **{data['vote_decision']}** recorded for rank {data['rank']}. Thanks!"
         except (json.JSONDecodeError, KeyError) as e:
-            return f"Error saving vote: {str(e)}"
+            return f"Error saving vote: {e}"
         except Exception as e:
-            return f"ERROR: {str(e)}"
-    
+            return f"ERROR: {e}"
+
     vote_trigger.change(
         handle_individual_vote,
-        inputs=[vote_trigger, st_query, st_ret_a_js, st_ret_b_js, st_sys1_is_a],
-        outputs=vote_feedback
+        inputs=[vote_trigger, st_query, st_version, st_ret_a, st_ret_b,
+                st_a_source, st_b_source],
+        outputs=vote_feedback,
     )
 
+
 if __name__ == "__main__":
-    demo.launch()
+    demo.launch(allowed_paths=["lean_finder_logo.png"])

requirements.txt

@@ -1,3 +1,4 @@
 huggingface_hub>=0.26.0,<1
 gspread
-google-auth
+google-auth
+requests