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