app.py

from google import genai
from google.genai import types
import gradio as gr

MODEL_ID = "gemini-2.0-flash-thinking-exp"
from google import genai
client = genai.Client(api_key="AIzaSyCmUDbVAOGcRZcOKP4q6mmeZ7Gx1WgE3vE")

def llm_response(text):
  response = client.models.generate_content(
    model=MODEL_ID,
    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 using formal proof assistants such as Lean, Coq, or Isabelle. 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  

iface = gr.Interface(
    fn=theorem_prover, 
    inputs=gr.Textbox(label="Enter Formula (e.g., x > 5 and y < 10)"), 
    outputs=gr.HTML(label="Result"),  # Output as HTML
    title="Theorem proving agent",
    description="Enter a logical formula using Z3 syntax to check its satisfiability."
)

# Launch the app
iface.launch()