Upload app.py with huggingface_hub

app.py

@@ -5,6 +5,7 @@ AI-assisted research tool for machine-verified theorems.
 """
 
 import json
+import os
 import numpy as np
 import gradio as gr
 from sklearn.feature_extraction.text import TfidfVectorizer
@@ -12,6 +13,14 @@ from sklearn.metrics.pairwise import cosine_similarity
 import matplotlib.pyplot as plt
 import matplotlib
 matplotlib.use('Agg')
+from huggingface_hub import InferenceClient
+
+# HuggingFace Inference API setup
+HF_TOKEN = os.environ.get("HF_TOKEN", None)  # Set as Space secret
+client = InferenceClient(
+    model="mistralai/Mistral-7B-Instruct-v0.3",
+    token=HF_TOKEN
+)
 
 # Load knowledge base
 with open('theorems_kb.json', 'r') as f:
@@ -52,8 +61,8 @@ def find_relevant_theorems(hypothesis, top_k=5):
     
     return results
 
-def generate_proof_scaffold(hypothesis, relevant_theorems):
-    """Generate Lean 4 proof scaffold from hypothesis and relevant theorems."""
+def generate_template_scaffold(hypothesis, relevant_theorems):
+    """Generate basic Lean 4 proof scaffold template (fallback)."""
     
     scaffold = f"""-- Hypothesis: {hypothesis}
 -- Upstream dependencies:
@@ -77,8 +86,63 @@ theorem my_hypothesis : <replace_with_formal_statement> := by
     
     return scaffold
 
+def generate_llm_hypothesis(user_hypothesis: str, relevant_theorems: list) -> str:
+    """Generate LLM-powered hypothesis analysis and Lean 4 draft."""
+    
+    theorem_context = "\n".join([
+        f"- {item['theorem']['name']} ({item['theorem']['module']}): {item['theorem']['statement'][:200]}"
+        for item in relevant_theorems[:5]
+    ])
+    
+    prompt = f"""You are a Lean 4 theorem proving assistant for the Eigenverse mathematical framework.
+
+The Eigenverse framework is built around the critical eigenvalue μ = exp(i·3π/4) at the 135° phase, with coherence function C(r) = 2r/(1+r²). It has 688 machine-verified theorems across physics, chemistry, and cosmology.
+
+User hypothesis: {user_hypothesis}
+
+Relevant existing theorems found:
+{theorem_context}
+
+Your task:
+1. Analyze how the hypothesis relates to these theorems
+2. Identify what mathematical structures are needed
+3. Draft a Lean 4 theorem statement and proof skeleton
+
+Output format:
+## Analysis
+<2-3 sentences connecting hypothesis to existing theorems>
+
+## Lean 4 Draft
+```lean4
+-- Hypothesis: {user_hypothesis}
+-- Dependencies: list the relevant theorems
+
+theorem hypothesis_name : <formal_statement> := by
+  -- Step 1: <what to do>
+  have h1 := relevant_theorem_1
+  -- Step 2: <what to do>  
+  sorry -- replace with proof
+```
+
+## Next Steps
+<what needs to be proven to complete this>"""
+
+    try:
+        response = client.text_generation(
+            prompt,
+            max_new_tokens=600,
+            temperature=0.3,
+            do_sample=True,
+        )
+        return response
+    except Exception as e:
+        # Fallback to template if LLM fails
+        fallback = f"⚠️ LLM generation failed ({str(e)}). Showing template scaffold.\n\n"
+        fallback += generate_template_scaffold(user_hypothesis, relevant_theorems)
+        return fallback
+
 def hypothesis_prover_tab(hypothesis):
-    """Tab 1: Hypothesis Prover."""
+    """Tab 1: Hypothesis Prover - now with LLM-powered analysis."""
     if not hypothesis.strip():
         return "Please enter a hypothesis.", ""
     
@@ -88,23 +152,23 @@ def hypothesis_prover_tab(hypothesis):
         return "No relevant theorems found. Try different keywords.", ""
     
     # Format relevant theorems
-    output = f"## Relevant Theorems (Top {len(relevant)})\n\n"
+    theorems_output = f"## Relevant Theorems (Top {len(relevant)})\n\n"
     
     for i, item in enumerate(relevant, 1):
         thm = item['theorem']
         score = item['score']
-        output += f"### {i}. {thm['name']} (relevance: {score:.3f})\n"
-        output += f"**Module:** {thm['module']}\n\n"
-        output += f"**Kind:** {thm['kind']}\n\n"
+        theorems_output += f"### {i}. {thm['name']} (relevance: {score:.3f})\n"
+        theorems_output += f"**Module:** {thm['module']}\n\n"
+        theorems_output += f"**Kind:** {thm['kind']}\n\n"
         if thm['docstring']:
-            output += f"**Description:** {thm['docstring']}\n\n"
-        output += f"```lean\n{thm['statement']}\n```\n\n"
-        output += "---\n\n"
+            theorems_output += f"**Description:** {thm['docstring']}\n\n"
+        theorems_output += f"```lean\n{thm['statement']}\n```\n\n"
+        theorems_output += "---\n\n"
     
-    # Generate scaffold
-    scaffold = generate_proof_scaffold(hypothesis, relevant)
+    # Generate LLM-powered hypothesis analysis
+    llm_output = generate_llm_hypothesis(hypothesis, relevant)
     
-    return output, scaffold
+    return theorems_output, llm_output
 
 def search_theorems(module_filter, search_query):
     """Tab 2: Theorem Explorer."""
@@ -269,7 +333,8 @@ with gr.Blocks(theme=gr.themes.Soft(), title="Eigenverse Theorem Prover") as app
         
         # Tab 1: Hypothesis Prover
         with gr.Tab("🔍 Hypothesis Prover"):
-            gr.Markdown("### Describe your hypothesis and get relevant theorems + proof scaffold")
+            gr.Markdown("### Describe your hypothesis and get relevant theorems + LLM-powered proof draft")
+            gr.Markdown("*Powered by Mistral-7B via HuggingFace Inference API. Set `HF_TOKEN` as a Space secret for better rate limits.*")
             
             hypothesis_input = gr.Textbox(
                 label="Hypothesis",
@@ -277,13 +342,13 @@ with gr.Blocks(theme=gr.themes.Soft(), title="Eigenverse Theorem Prover") as app
                 lines=3
             )
             
-            prove_button = gr.Button("Find Theorems & Generate Scaffold", variant="primary")
+            prove_button = gr.Button("Find Theorems & Generate Proof Draft", variant="primary")
             
             with gr.Row():
                 with gr.Column():
                     relevant_output = gr.Markdown(label="Relevant Theorems")
                 with gr.Column():
-                    scaffold_output = gr.Code(label="Lean Proof Scaffold", language="lean")
+                    scaffold_output = gr.Markdown(label="LLM Proof Draft")
             
             prove_button.click(
                 hypothesis_prover_tab,