#!/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()