docs: fix incorrect CLI commands, flags, and API examples

docs/examples.md

@@ -12,9 +12,10 @@ async def main():
     client = Client(api_key="your-api-key")
     results = await client.search("natural numbers")
 
-    for item in results.items[:5]:
+    for item in results.results[:5]:
         print(f"{item.primary_declaration.lean_name}")
-        print(f"  {item.informal_name}")
+        if item.informal_description:
+            print(f"  {item.informal_description}")
         print()
 
 asyncio.run(main())
@@ -34,8 +35,8 @@ async def main():
         package_filters=["Mathlib", "Batteries"]
     )
 
-    print(f"Found {len(results.items)} results in Mathlib and Batteries")
-    for item in results.items:
+    print(f"Found {len(results.results)} results in Mathlib and Batteries")
+    for item in results.results:
         print(f"- {item.primary_declaration.lean_name}")
 
 asyncio.run(main())
@@ -60,8 +61,8 @@ async def main():
 
     for result in results:
         print(f"\nQuery: {result.query}")
-        print(f"Results: {len(result.items)}")
-        for item in result.items[:3]:
+        print(f"Results: {len(result.results)}")
+        for item in result.results[:3]:
             print(f"  - {item.primary_declaration.lean_name}")
 
 asyncio.run(main())
@@ -78,15 +79,16 @@ async def main():
 
     # Search first
     search_results = await client.search("Nat")
-    if search_results.items:
-        first_result = search_results.items[0]
+    if search_results.results:
+        first_result = search_results.results[0]
 
-        # Get citations
-        citations = await client.get_citations(first_result.id)
+        # Get dependencies (citations)
+        dependencies = await client.get_dependencies(first_result.id)
 
-        print(f"Citations for {first_result.primary_declaration.lean_name}:")
-        for citation in citations.citations:
-            print(f"  - {citation.lean_name}")
+        if dependencies:
+            print(f"Dependencies for {first_result.primary_declaration.lean_name}:")
+            for citation in dependencies.citations:
+                print(f"  - {citation.primary_declaration.lean_name}")
 
 asyncio.run(main())
 ```
@@ -104,8 +106,8 @@ async def main():
     # Search
     results = await service.search("natural numbers")
 
-    print(f"Found {len(results.items)} results")
-    for item in results.items[:5]:
+    print(f"Found {len(results.results)} results")
+    for item in results.results[:5]:
         print(f"- {item.primary_declaration.lean_name}")
 
 asyncio.run(main())
@@ -119,12 +121,12 @@ from lean_explore.api.client import Client
 
 async def main():
     # Connect to local server
-    client = Client(base_url="http://localhost:8000")
+    client = Client(base_url="http://localhost:8001")
 
     # Use as normal
     results = await client.search("natural numbers")
 
-    for item in results.items:
+    for item in results.results:
         print(item.primary_declaration.lean_name)
 
 asyncio.run(main())
@@ -142,7 +144,7 @@ async def main():
 
     try:
         results = await client.search("natural numbers")
-        print(f"Found {len(results.items)} results")
+        print(f"Found {len(results.results)} results")
     except httpx.HTTPStatusError as e:
         print(f"HTTP error: {e.response.status_code}")
         print(f"Response: {e.response.text}")
@@ -168,7 +170,7 @@ async def main():
     )
 
     results = await client.search("natural numbers")
-    print(f"Found {len(results.items)} results")
+    print(f"Found {len(results.results)} results")
 
 asyncio.run(main())
 ```

docs/getting-started/configuration.md

@@ -14,18 +14,16 @@ leanexplore configure api-key YOUR_API_KEY
 
 The API key is stored in your user configuration directory and will be used for all API requests.
 
-### View Current Configuration
+### OpenAI API Key
 
-```bash
-leanexplore configure show
-```
-
-### Reset Configuration
+Set your OpenAI API key for chat functionality:
 
 ```bash
-leanexplore configure reset
+leanexplore configure openai-key YOUR_OPENAI_API_KEY
 ```
 
+The OpenAI API key is stored in your user configuration directory and will be used for chat sessions.
+
 ## Environment Variables
 
 You can also configure Lean Explore using environment variables:
@@ -41,7 +39,7 @@ export LEAN_EXPLORE_API_KEY=your-api-key
 For local servers or custom endpoints:
 
 ```bash
-export LEAN_EXPLORE_BASE_URL=http://localhost:8000
+export LEAN_EXPLORE_BASE_URL=http://localhost:8001
 ```
 
 ## Python Configuration
@@ -104,30 +102,30 @@ service = Service(
 
 ```bash
 # Use remote API backend
-leanexplore http start --backend api --api-key YOUR_API_KEY
+leanexplore http serve --backend api --api-key YOUR_API_KEY
 
 # Use local backend
-leanexplore http start --backend local
+leanexplore http serve --backend local
 ```
 
 ### Port and Host
 
 ```bash
 # Custom port
-leanexplore http start --backend local --port 8080
+leanexplore http serve --backend local --port 8080
 
 # Custom host
-leanexplore http start --backend local --host 0.0.0.0
+leanexplore http serve --backend local --host 0.0.0.0
 ```
 
 ## MCP Server Configuration
 
 ```bash
 # API backend
-leanexplore mcp start --backend api --api-key YOUR_API_KEY
+leanexplore mcp serve --backend api --api-key YOUR_API_KEY
 
 # Local backend
-leanexplore mcp start --backend local
+leanexplore mcp serve --backend local
 ```
 
 ## Configuration Files

docs/getting-started/quickstart.md

@@ -25,7 +25,7 @@ leanexplore configure api-key YOUR_API_KEY
 Filter results to specific packages:
 
 ```bash
-leanexplore search "monoid" --pkg Mathlib --pkg Batteries
+leanexplore search "monoid" --package Mathlib --package Batteries
 ```
 
 ## Using Python API
@@ -44,8 +44,10 @@ async def main():
     results = await client.search("natural numbers")
 
     # Print results
-    for item in results.items[:5]:  # Top 5 results
-        print(f"{item.primary_declaration.lean_name}: {item.informal_name}")
+    for item in results.results[:5]:  # Top 5 results
+        lean_name = item.primary_declaration.lean_name
+        informal = item.informal_description or "No description"
+        print(f"{lean_name}: {informal}")
 
 asyncio.run(main())
 ```
@@ -65,7 +67,7 @@ async def main():
 
     for result in results:
         print(f"Query: {result.query}")
-        print(f"Found {len(result.items)} results\n")
+        print(f"Found {len(result.results)} results\n")
 
 asyncio.run(main())
 ```
@@ -79,21 +81,21 @@ asyncio.run(main())
 leanexplore data fetch
 
 # Start the server
-leanexplore http start --backend local
+leanexplore http serve --backend local
 ```
 
-The server will be available at `http://localhost:8000`.
+The server will be available at `http://localhost:8001`.
 
 ### Query the Local Server
 
 ```bash
-curl "http://localhost:8000/api/v1/search?q=natural+numbers"
+curl "http://localhost:8001/api/v1/search?q=natural+numbers"
 ```
 
 Or use the Python client with a custom base URL:
 
 ```python
-client = Client(base_url="http://localhost:8000")
+client = Client(base_url="http://localhost:8001")
 results = await client.search("natural numbers")
 ```
 
@@ -102,7 +104,7 @@ results = await client.search("natural numbers")
 The MCP (Model Context Protocol) server allows AI agents to interact with Lean Explore:
 
 ```bash
-leanexplore mcp start --backend api --api-key YOUR_API_KEY
+leanexplore mcp serve --backend api --api-key YOUR_API_KEY
 ```
 
 ## Next Steps

docs/index.md

@@ -51,7 +51,7 @@ leanexplore search "natural numbers"
 leanexplore configure api-key YOUR_API_KEY
 
 # Start local HTTP server
-leanexplore http start --backend local
+leanexplore http serve --backend local
 ```
 
 ### Python API
@@ -67,10 +67,10 @@ results = await client.search("natural numbers")
 
 ```bash
 # Start server
-leanexplore http start --backend local
+leanexplore http serve --backend local
 
 # Query via HTTP
-curl "http://localhost:8000/api/v1/search?q=natural+numbers"
+curl "http://localhost:8001/api/v1/search?q=natural+numbers"
 ```
 
 ## Documentation Structure

docs/user-guide/api-client.md

@@ -13,7 +13,7 @@ from lean_explore.api.client import Client
 client = Client(api_key="your-api-key")
 
 # With custom base URL (for local servers)
-client = Client(base_url="http://localhost:8000")
+client = Client(base_url="http://localhost:8001")
 
 # Both API key and custom URL
 client = Client(
@@ -31,8 +31,8 @@ async def main():
     client = Client(api_key="your-api-key")
     results = await client.search("natural numbers")
 
-    print(f"Found {len(results.items)} results")
-    for item in results.items:
+    print(f"Found {len(results.results)} results")
+    for item in results.results:
         print(f"- {item.primary_declaration.lean_name}")
 
 asyncio.run(main())
@@ -49,7 +49,7 @@ async def main():
 
     for result in results:
         print(f"Query: {result.query}")
-        print(f"Results: {len(result.items)}\n")
+        print(f"Results: {len(result.results)}\n")
 
 asyncio.run(main())
 ```
@@ -68,7 +68,7 @@ async def main():
         package_filters=["Mathlib", "Batteries"]
     )
 
-    for item in results.items:
+    for item in results.results:
         print(f"{item.primary_declaration.lean_name}")
 
 asyncio.run(main())
@@ -82,14 +82,16 @@ async def main():
 
     # Search first
     search_results = await client.search("natural numbers")
-    first_result = search_results.items[0]
-
-    # Get citations for a result
-    citations = await client.get_citations(first_result.id)
-
-    print(f"Citations for {first_result.primary_declaration.lean_name}:")
-    for citation in citations.citations:
-        print(f"- {citation.lean_name}")
+    if search_results.results:
+        first_result = search_results.results[0]
+
+        # Get dependencies (citations) for a result
+        dependencies = await client.get_dependencies(first_result.id)
+
+        if dependencies:
+            print(f"Dependencies for {first_result.primary_declaration.lean_name}:")
+            for citation in dependencies.citations:
+                print(f"- {citation.primary_declaration.lean_name}")
 
 asyncio.run(main())
 ```
@@ -123,38 +125,34 @@ results: APISearchResponse = await client.search("query")
 
 # Access properties
 results.query  # The search query
-results.items  # List of APISearchResultItem
+results.results  # List of APISearchResultItem
 ```
 
 ### APISearchResultItem
 
 ```python
-item = results.items[0]
+item = results.results[0]
 
 # Primary declaration
 item.primary_declaration.lean_name
-item.primary_declaration.decl_type
 
 # Informal description
-item.informal_name
 item.informal_description
 
 # Statement group ID
 item.id
 
-# Score
-item.score
 ```
 
 ### APICitationsResponse
 
 ```python
-citations = await client.get_citations(item_id)
+dependencies = await client.get_dependencies(item_id)
 
-# List of citations
-for citation in citations.citations:
-    print(citation.lean_name)
-    print(citation.decl_type)
+# List of dependencies (citations)
+if dependencies:
+    for citation in dependencies.citations:
+        print(citation.primary_declaration.lean_name)
 ```
 
 ## Configuration