Upload folder using huggingface_hub

README.md

@@ -1,12 +1,6 @@
 ---
-title: Aristotle Prover
-emoji: 🐠
-colorFrom: purple
-colorTo: pink
-sdk: gradio
-sdk_version: 6.6.0
+title: Aristotle_Theorem_Prover
 app_file: app.py
-pinned: false
+sdk: gradio
+sdk_version: 6.5.1
 ---
-
-Check out the configuration reference at https://huggingface.co/docs/hub/spaces-config-reference

app.py

@@ -0,0 +1,275 @@
+#!/usr/bin/env python3
+"""
+Gradio UI for Aristotle theorem prover (informal mode).
+
+Provides a simple interface for non-programmers to submit
+mathematical problems and receive Lean 4 proofs.
+
+Launch:
+    python aristotle_ui.py
+"""
+
+import asyncio
+import tempfile
+import time
+from pathlib import Path
+
+import gradio as gr
+
+from aristotlelib import api_request
+from aristotlelib.project import Project, ProjectInputType, ProjectStatus
+
+POLL_INTERVAL = 15  # seconds between status checks
+MAX_POLL_TIME = 1800  # 30 minutes max wait
+
+
+# ---------------------------------------------------------------------------
+# Core logic
+# ---------------------------------------------------------------------------
+
+def _set_key(api_key: str) -> bool:
+    key = api_key.strip()
+    if not key:
+        return False
+    api_request.set_api_key(key)
+    return True
+
+
+def _run_async(coro):
+    """Run an async coroutine from synchronous Gradio callback."""
+    loop = asyncio.new_event_loop()
+    try:
+        return loop.run_until_complete(coro)
+    finally:
+        loop.close()
+
+
+def submit_problem(api_key: str, problem_text: str):
+    """Generator: submit a problem and poll until done."""
+    if not _set_key(api_key):
+        yield "Enter your Aristotle API key above.", "", ""
+        return
+    problem_text = problem_text.strip()
+    if not problem_text:
+        yield "Enter a problem or proof statement.", "", ""
+        return
+
+    logs = []
+
+    def log(msg):
+        logs.append(msg)
+        return "\n".join(logs)
+
+    # Submit
+    yield log("Submitting to Aristotle (informal mode)..."), "", ""
+
+    try:
+        project_id = _run_async(
+            Project.prove_from_file(
+                input_content=problem_text,
+                project_input_type=ProjectInputType.INFORMAL,
+                wait_for_completion=False,
+                auto_add_imports=False,
+                validate_lean_project=False,
+            )
+        )
+    except Exception as e:
+        yield log(f"Submission error: {e}"), "", ""
+        return
+
+    yield log(f"Submitted! Project ID: {project_id}"), "", project_id
+
+    # Poll for completion
+    elapsed = 0
+    while elapsed < MAX_POLL_TIME:
+        time.sleep(POLL_INTERVAL)
+        elapsed += POLL_INTERVAL
+
+        try:
+            project = _run_async(Project.from_id(project_id))
+        except Exception as e:
+            yield log(f"[{elapsed}s] Poll error: {e} (will retry)"), "", project_id
+            continue
+
+        status = project.status
+        pct = project.percent_complete
+        pct_str = f" ({pct}%)" if pct is not None else ""
+        yield log(f"[{elapsed}s] {status.value}{pct_str}"), "", project_id
+
+        if status == ProjectStatus.COMPLETE:
+            try:
+                with tempfile.TemporaryDirectory() as td:
+                    out = Path(td) / "solution.lean"
+                    _run_async(project.get_solution(output_path=out))
+                    solution = out.read_text()
+                yield log("Proof retrieved!"), solution, project_id
+            except Exception as e:
+                yield log(f"Error downloading solution: {e}"), "", project_id
+            return
+
+        if status == ProjectStatus.FAILED:
+            yield log("Project FAILED. Aristotle could not find a proof."), "", project_id
+            return
+
+    yield log(f"Timed out after {MAX_POLL_TIME // 60} minutes. Use 'Check Project' with the ID above to check later."), "", project_id
+
+
+def check_project(api_key: str, project_id: str):
+    """Check status of a previously submitted project."""
+    if not _set_key(api_key):
+        return "Enter your API key.", ""
+    project_id = project_id.strip()
+    if not project_id:
+        return "Enter a project ID.", ""
+
+    try:
+        project = _run_async(Project.from_id(project_id))
+    except Exception as e:
+        return f"Error: {e}", ""
+
+    info = f"Project: {project_id}\nStatus: {project.status.value}"
+    if project.percent_complete is not None:
+        info += f"\nProgress: {project.percent_complete}%"
+    if project.file_name:
+        info += f"\nFile: {project.file_name}"
+
+    solution = ""
+    if project.status == ProjectStatus.COMPLETE:
+        try:
+            with tempfile.TemporaryDirectory() as td:
+                out = Path(td) / "solution.lean"
+                _run_async(project.get_solution(output_path=out))
+                solution = out.read_text()
+            info += "\n\nSolution downloaded successfully."
+        except Exception as e:
+            info += f"\n\nError downloading solution: {e}"
+
+    return info, solution
+
+
+def list_recent(api_key: str):
+    """List recent projects for this API key."""
+    if not _set_key(api_key):
+        return "Enter your API key."
+
+    try:
+        projects, _ = _run_async(Project.list_projects(limit=15))
+    except Exception as e:
+        return f"Error: {e}"
+
+    if not projects:
+        return "No projects found."
+
+    lines = []
+    for p in projects:
+        pct = f" ({p.percent_complete}%)" if p.percent_complete is not None else ""
+        desc = f" — {p.description[:60]}" if p.description else ""
+        lines.append(f"{p.project_id[:12]}...  {p.status.value:14s}{pct}{desc}")
+    return "\n".join(lines)
+
+
+# ---------------------------------------------------------------------------
+# Build UI
+# ---------------------------------------------------------------------------
+
+EXAMPLES = [
+    ["Prove that the square root of 2 is irrational."],
+    ["Prove that for all natural numbers n, the sum 1 + 2 + ... + n equals n*(n+1)/2."],
+    ["Show that every continuous function on a closed bounded interval [a,b] is uniformly continuous."],
+    ["Prove that if p is prime and p divides a*b, then p divides a or p divides b."],
+]
+
+
+def build_app() -> gr.Blocks:
+    with gr.Blocks(title="Aristotle Prover", theme=gr.themes.Soft()) as app:
+        gr.Markdown(
+            "# Aristotle Theorem Prover\n"
+            "Submit a mathematical problem or proof in plain English. "
+            "[Aristotle](https://harmonic.fun/) will formalize it in Lean 4 and attempt a proof.\n\n"
+            "You need an Aristotle API key — get one at [harmonic.fun](https://harmonic.fun/)."
+        )
+
+        api_key = gr.Textbox(
+            label="Aristotle API Key",
+            type="password",
+            placeholder="sk-...",
+        )
+
+        with gr.Tab("Prove"):
+            problem_input = gr.Textbox(
+                label="Problem statement",
+                lines=10,
+                placeholder=(
+                    "State a theorem, lemma, or problem in plain English or LaTeX.\n\n"
+                    "Examples:\n"
+                    "- Prove that sqrt(2) is irrational.\n"
+                    "- Show that every bounded monotone sequence converges.\n"
+                    "- Prove: if G is a finite group of order p^n (p prime), then G has a nontrivial center."
+                ),
+            )
+
+            gr.Examples(
+                examples=EXAMPLES,
+                inputs=[problem_input],
+                label="Example problems",
+            )
+
+            submit_btn = gr.Button("Submit to Aristotle", variant="primary")
+
+            with gr.Row():
+                with gr.Column():
+                    progress_log = gr.Textbox(
+                        label="Progress",
+                        lines=12,
+                        interactive=False,
+                    )
+                with gr.Column():
+                    result_output = gr.Code(
+                        label="Lean 4 Proof",
+                        language=None,
+                        lines=20,
+                    )
+
+            project_id_state = gr.Textbox(visible=False)
+
+            submit_btn.click(
+                fn=submit_problem,
+                inputs=[api_key, problem_input],
+                outputs=[progress_log, result_output, project_id_state],
+            )
+
+        with gr.Tab("Check Project"):
+            gr.Markdown(
+                "Check on a previously submitted project by its ID, "
+                "or list your recent projects."
+            )
+
+            with gr.Row():
+                check_id = gr.Textbox(
+                    label="Project ID",
+                    placeholder="paste project ID here",
+                    scale=3,
+                )
+                check_btn = gr.Button("Check", variant="primary", scale=1)
+                list_btn = gr.Button("List Recent", scale=1)
+
+            check_status = gr.Textbox(label="Status", lines=6, interactive=False)
+            check_solution = gr.Code(label="Lean 4 Proof", language=None, lines=20)
+
+            check_btn.click(
+                fn=check_project,
+                inputs=[api_key, check_id],
+                outputs=[check_status, check_solution],
+            )
+            list_btn.click(
+                fn=list_recent,
+                inputs=[api_key],
+                outputs=[check_status],
+            )
+
+    return app
+
+
+if __name__ == "__main__":
+    app = build_app()
+    app.launch()

requirements.txt

@@ -0,0 +1,2 @@
+aristotlelib
+gradio