Update app.py

app.py

@@ -15,147 +15,53 @@ def llm_response(text):
     contents= text)
   return response.text
 
-def theorem_prover(theorem):
-  theorem_llm = llm_response(f'''You are an advanced mathematical reasoning model specializing in formal theorem proving. Your task is to analyze a given theorem, 
-  determine the most appropriate proof strategy, and construct a rigorous proof. If a proof is not  possible, identify gaps, suggest refinements, or provide counterexamples.
-
-  User Prompt:
-Input:
-"Theorem Statement:
-{theorem}
- Task Breakdown:
-1. Understand the Theorem
-Identify the mathematical domain (e.g., Number Theory, Algebra, Topology).
-Recognize any implicit assumptions, definitions, or missing details.
-Determine whether the theorem is constructive, existential, or universally quantified.
-2. Determine the Proof Strategy
-The model will automatically select the best approach based on the theorem's structure:
-
-Proof Strategy Selection Guidelines
-To determine the best proof strategy for a given theorem, follow these principles:
-
-Direct Proof → Use when the statement follows naturally from known axioms or definitions. Example: Proving that if 
-𝑛
-n is even, then 
-𝑛
-2
-n 
-2
-  is even.
-Proof by Contradiction → Assume the negation of the statement and show it leads to a contradiction. This is useful for proving the infinitude of primes.
-Proof by Induction → Apply when proving a property for an infinite sequence or recursively defined structures. Example: Proving the sum formula 
-∑
-𝑖
-=
-1
-𝑛
-𝑖
-=
-𝑛
-(
-𝑛
-+
-1
-)
-2
-∑ 
-i=1
-n
-​
- i= 
-2
-n(n+1)
-​
- .
-Case Analysis → Use when different scenarios must be considered separately. Example: Proving that a quadratic equation has at most two real roots.
-Constructive Proof → Show existence by explicitly constructing an example. Example: Proving that there exists an irrational number 
-𝑥
-x such that 
-𝑥
-𝑥
-x 
-x
-  is rational.
-Non-constructive Proof → Prove existence without constructing an explicit example, often using logic or set theory. Example: Proving that there exists a prime number between 
-𝑛
-n and 
-2
-𝑛
-2n.
-Proof by Exhaustion → Use when a theorem holds for a small, finite set of cases that can be checked individually. Example: Verifying a property for small integers.
-Proof using a Counterexample → Disprove a general claim by providing a specific case where it fails. Example: Showing that not all differentiable functions are continuous.
-The model should analyze the structure of the theorem and automatically select the most suitable proof technique based on these guidelines.
-
-3. Construct the Proof
-Step-by-step logical explanation.
-
-Verification and validation.
-4. Handle Edge Cases
-If proof fails:
-
-Highlight missing assumptions.
-Provide a minimal counterexample (if the statement is false).
-Suggest a reformulation or alternative direction.
-Expected Output:
-✔ Proof Found:
-
-Step-by-step reasoning.
-Proof strategy justification.
-
-❌ Proof Not Possible:
-
-Identified logical gap or missing assumptions.
-Suggested refinement or counterexample.
-Example Usage:
-Input:
-"Every even integer greater than 2 can be expressed as the sum of two prime numbers."
-
-Output:
-✔ Proof Attempt:
-
-Identified Proof Strategy:
-
-This is an existential statement (∃ two primes p1, p2 such that p1 + p2 = n).
-Since direct proof is difficult, contradiction and case analysis are common approaches.
-Computational methods confirm the conjecture for large values of 
-𝑛
-n, but no general proof exists.
-Proof Attempt:
-
-
-theorem goldbach_conjecture (n : ℕ) (h : even n ∧ n > 2) :  
-  ∃ p1 p2, prime p1 ∧ prime p2 ∧ p1 + p2 = n :=  
-begin  
-  -- Step 1: Assume n is an even integer greater than 2  
-  -- Step 2: Search for prime pairs (p1, p2) such that p1 + p2 = n  
-  -- Step 3: If no counterexamples exist up to a given range, assume general case  
-  -- Theorem remains unproven but verified for large n using computational methods  
-end  
-❌ Proof Not Found:
-
-No general proof within standard number theory axioms.
-Computational verification up to 
-10
-18
-10 
-18
-  supports the conjecture.
-Suggest refining the conjecture by imposing additional constraints.
-
-You should intelligently selects the best proof strategy.
-Provides clear justifications for strategy choice.
-
-Output a rigorous proof or meaningful insight even when a full proof is impossible in markdown format.''')
-  return theorem_llm  
+def pvsnp(problem):
+  classification = llm_response(f'''
+
+  You are an expert in computational complexity theory with deep knowledge of both classical complexity classes (P, NP, NP-complete, NP-hard) and modern developments such as parameterized complexity, fine-grained complexity, and recent findings like the Minimum Circuit Size Problem (MCSP). Your task is to analyze a given problem description and classify it into one of the following categories:
+
+- **P**: Problems that can be solved in deterministic polynomial time.
+- **NP**: Problems for which a proposed solution can be verified in deterministic polynomial time.
+- **NP-complete**: Problems that are both in NP and as hard as any problem in NP, via polynomial-time reductions.
+- **NP-hard**: Problems that are at least as hard as NP-complete problems but may not be in NP.
+- **Beyond NP**: Problems that likely belong to more complex classes (e.g., PSPACE, EXPTIME) or are undecidable.
+- **Other**: If the problem fits into an alternative complexity class (e.g., BPP, co-NP) or does not clearly align with the categories above, note that explicitly.
+
+**Problem Description:**
+{problem}
+
+**Guidelines:**
+
+1. **Comprehensive Analysis**:  
+   - Determine whether the problem is primarily a decision problem, an optimization problem, or a function computation.
+   - Identify key input and output characteristics and any explicit constraints.
+
+2. **Complexity Characteristics**:  
+   - Examine if the problem exhibits features common to polynomial-time algorithms (e.g., dynamic programming, greedy strategies) or if it has structural similarities to known NP-complete problems.
+   - Assess whether there is potential for polynomial-time reductions from or to well-studied problems in the literature.
+
+3. **Advanced and Recent Research Considerations**:  
+   - Incorporate insights from the latest research, including the implications of the Minimum Circuit Size Problem (MCSP) for NP-completeness.
+   - Consider parameterized complexity aspects: does the problem admit fixed-parameter tractable (FPT) solutions under certain parameters?
+   - Evaluate any connections to fine-grained complexity results, such as relationships to the Strong Exponential Time Hypothesis (SETH) or other conjectures.
+   - If the problem has probabilistic or average-case aspects, mention how these might affect its classification.
+
+4. **Explanation of Reasoning**:  
+   - Provide a brief, clear explanation for your classification. Justify your decision by referencing specific features of the problem and connecting them to established theory and recent research insights.
+
+**Your Classification and Explanation:**
+
+''')
+  return classification 
 
 iface = gr.Interface(
-    fn=theorem_prover, 
-    inputs=gr.Textbox(label="Enter the theorem you want to prove or disprove"), 
+    fn=pvsnp, 
+    inputs=gr.Textbox(label="What problem would you like to classify as P or NP?"), 
     outputs=gr.Markdown(label="Agent's response"),  # Output as HTML
     title="PolyProb",
-    description="PolyProb is an advanced AI agent that guides users through the intricate maze of computational complexity. This agent scrutinizes problem descriptions with sophisticated LLM prompts and symbolic reasoning. It classifies problems into categories such as P, NP, NP-complete, NP-hard, or beyond (e.g., PSPACE, EXPTIME), while providing clear, concise explanations of its reasoning. As part of AI Quotient’s Millennium Math Challenge, it is the first step towards solving the P vs NP problem",
+    description="PolyProb is an advanced AI agent that guides users through the intricate maze of computational complexity. This agent scrutinizes problem descriptions with sophisticated LLM prompts and symbolic reasoning. It classifies problems into categories such as P, NP, NP-complete, NP-hard, or beyond (e.g., PSPACE, EXPTIME), while providing clear, concise explanations of its reasoning. As part of AI Quotient’s Millennium Math Challenge, it is the first step towards solving the P vs NP problem.",
     theme = gr.themes.Ocean(),
-    examples = ["Every prime number greater than 2 is odd.", "The sum of two rational numbers is always rational.", "The power set of any set has strictly greater cardinality than the set itself."]
+    examples = ["Can you find a path that visits each node exactly once in a given graph?", "How efficiently can two nXn matrices be multiplied?", "Is there a subset of given numbers that sums to a target value?"]
 )
 
 # Launch the app