# Project export: Zeta This document was generated by HackStack to give an AI agent context about a hackathon project. Sections are labeled with their provenance; content marked as truncated was cut to keep this document small. ## Project metadata - Hackathon: TreeHacks 2026 - Tagline: Grammarly for Math - Devpost: https://devpost.com/software/zeta-jwq9te - GitHub: https://github.com/aryans-15/treehacks-2026 - Video: https://www.youtube.com/embed/RJV8a8PWkxQ?enablejsapi=1&hl=en_US&rel=0&start=&version=3&wmode=transparent - Result: winner ([Y Combinator] Build an Iconic YC Company with AI (1st Place: Guaranteed YC interview 2nd Place: Guaranteed YC Office Hours 3rd Place: Guaranteed YC Office Hours)) - Team: 4 GitHub contributor(s) — aryans-15 (48 commits), William Feng (38 commits), galacticism (5 commits), Amir Zeinali (1 commits) ## Devpost submission (written by the team) ### Inspiration As math and computer science majors, we’re often spending hours writing proofs in LaTeX, getting lost in paragraphs of LaTeX more times than we can count. Formal correctness is slow: you only find gaps when a TA grades it, often long after you’ve lost context. Instead, we wanted a Grammarly-like experience for proofs: immediate feedback as you write. Recent advances in neural theorem proving and informal-to-formal translation (Polu & Sutskever, 2020; Lewkowycz et al., 2022) indicate that it's possible to close the loop: highlight the exact step that’s wrong, explain why, and suggest a minimal fix in real time. How it Works Zeta is a Chrome extension for Overleaf that assists users with proof-writing, essentially acting as Grammarly for formal math. As users write, it intelligently chunks the document, translates each segment to Lean using a fine-tuned Herald_Translator model (Zhou et al., 2024), and compiles the result. Compilation errors are captured and passed to an LLM to generate precise, actionable feedback. In Thinking mode, Zeta adds an automated repair loop: Lean errors are iteratively fed back into the LLM until valid Lean code is produced or an iteration limit is reached. Once compilation succeeds, a final synthesis step generates structured feedback for the user based on the full repair trajectory. ### Challenges we ran into Robustness to semantic variation The translator’s performance degraded significantly under minor semantic perturbations in the LaTeX that didn’t affect the underlying proof logic. To address this, we fine-tuned Herald_Translator with LoRA on a dataset of systematically perturbed (accounting for how likely the typo was based on key positions), logically equivalent examples, improving invariance to typos. Lean compilation errors Even when the LaTeX was correct, the generated Lean sometimes contained minor issues (e.g., type errors) that prevented compilation. We introduced a Thinking Mode with an automated repair loop: Lean compiler errors are fed back into the LLM, which iteratively patches the code until it compiles, stabilizes (no further changes), or reaches a preset iteration limit. Axioms vs Theorems in Lean4 In Lean4, a theorem must be backed by a proof term that is fully verified by the kernel, but an axiom can just introduce a statement without proof and is accepted as true by assumption. In our project, translated Lean4 code would sometimes rely on undeclared assumptions. In some cases, introducing an axiom would allow compilation to succeed even when the formal proof was incomplete. As a result, we had to ensure that the translation and repair pipeline avoided introducing axioms as shortcuts to resolve proof failures. Instead, all results needed to compile strictly as theorems with explicit proof terms. ### Accomplishments we're proud of We compared Zeta’s Herald-based pipeline against a ChatGPT-based baseline on a 20-problem benchmark (9 true, 11 false statements). The Herald pipeline achieved perfect correctness across both true and false cases while maintaining comparable latency and slightly lower cost. ChatGPT 4.1 struggled primarily on true proofs, where structural reasoning and proof-state consistency are required, highlighting the advantage of a specialized translation + repair pipeline over a single-pass LLM. Fine-tuning Herald_Translator with LoRA (Hu et al., 2021) improved the accuracy on a perturbed evaluation set from 56% (base model) to 90% (LoRA fine-tuned), demonstrating significantly stronger invariance to semantically equivalent variations. On the systems side, baseline inference latency on Modal was ~15–18 seconds per translation. Integrating vLLM (Kwon et al., 2023) reduced this to ~3 seconds per call across 100+ runs, making real-time Overleaf feedback feasible. ### What we learned We learned that translation from informal mathematics to formal language is highly sensitive to surface variation and implicit assumptions. We also saw how ambiguity in LaTeX conventions and library usage (e.g., implicit definitions, overloaded notation, unstated algebraic structures) creates failure modes during translation. Formal systems perform a lot better when provided with explicit structure, types, and hypotheses, and informal answers often omit those. Bridging that gap is the most difficult part of robust translation and feedback. ### What's next While Zeta performs strongly, several clear avenues remain for improvement. First, the iterative repair model could be strengthened by training of a repair model on Lean error–correction trajectories and optimizing for convergence speed under structured compiler feedback. Second, both translation and repair should be conditioned on a richer representation of the Lean proof state. Instead of relying primarily on raw error messages, incorporating structured goal states and type information would allow the model to reason directly over formal constraints. Finally, we could train a dedicated model to map repair trajectories and compiler outputs into high-quality natural language guidance, using human responses (e.g., whether the feedback resolved confusion or improved the proof) as a post-training signal. References Hu et al. (2021). LoRA: Low-Rank Adaptation of Large Language Models. Kwon et al. (2023). vLLM: Easy, Fast, and Cheap LLM Serving with PagedAttention. Lewkowycz et al. (2022). Solving Quantitative Reasoning Problems with Language Models. Polu & Sutskever (2020). Generative Language Modeling for Automated Theorem Proving. Zhou, X., et al. (2024). Herald: Neural Translation from LaTeX to Lean for Formal Verification. ## README (from the GitHub repository) # Zeta **Grammarly for math.** Zeta checks your mathematical writing (e.g. in Overleaf) and suggests fixes, like a proofreader for LaTeX and formal math. ## How to download / install 1. Open Chrome and go to `chrome://extensions`. 2. Turn on **Developer mode** (top right). 3. Click **Load unpacked**. 4. Choose the folder: `apps/overleaf-extension` inside this repo. After that, open an Overleaf project and use the Zeta panel to run checks and see suggestions. ## Detected evidence (automated analysis) Indexed codebase: 49 recognized source files, 975 KB. - CSS (language) — detected in the code - FastAPI (technology) — detected in the code - HTML (language) — detected in the code - JavaScript (language) — detected in the code - Python (language) — detected in the code - AWS (technology) — claimed on Devpost, not found in the code - PyTorch (technology) — claimed on Devpost, not found in the code ## Codebase structure (from repository index) ### Files (82 of 82) ``` .github/workflows/deploy.yml .gitignore apps/overleaf-extension/background.js apps/overleaf-extension/content_adapters.js apps/overleaf-extension/content_app.js apps/overleaf-extension/content_bootstrap.js apps/overleaf-extension/content_shared.js apps/overleaf-extension/content_ui.js apps/overleaf-extension/content.css apps/overleaf-extension/content.js apps/overleaf-extension/manifest.json apps/overleaf-extension/popup.css apps/overleaf-extension/popup.html apps/overleaf-extension/popup.js apps/overleaf-extension/README.md benchmarks/cases_hard20.json benchmarks/cases_hard5.json benchmarks/cases.json benchmarks/rescore.py benchmarks/results/.gitignore benchmarks/results/benchmark-hard20-gpt53.txt benchmarks/results/benchmark-hard20.txt benchmarks/results/benchmark-hard5.txt benchmarks/results/benchmark-latest.txt benchmarks/run_benchmark.py README.md services/lean-backend/.env.example services/lean-backend/app/__init__.py services/lean-backend/app/highlight_llm.py services/lean-backend/app/highlight_locator.py services/lean-backend/app/lean_compile.py services/lean-backend/app/llm_client.py services/lean-backend/app/main.py services/lean-backend/app/modal_client.py services/lean-backend/app/models.py services/lean-backend/app/settings.py services/lean-backend/app/utils.py services/lean-backend/bin/elan services/lean-backend/bin/lake services/lean-backend/bin/lean services/lean-backend/bin/leanc services/lean-backend/bin/leanchecker services/lean-backend/bin/leanmake services/lean-backend/bin/leanpkg services/lean-backend/docker-compose.yml services/lean-backend/Dockerfile services/lean-backend/env services/lean-backend/pytest.ini services/lean-backend/README.md services/lean-backend/requirements.txt services/lean-backend/scripts/bootstrap_mathlib_project.sh services/lean-backend/settings.toml services/lean-backend/tests/test_api.py services/lean-backend/tests/test_highlight_llm.py services/lean-backend/tests/test_highlights.py services/lean-backend/tests/test_lean_compile.py services/lean-backend/tests/test_llm_client.py services/lean-backend/tests/test_modal_client.py services/perturbations/perturb.py services/perturbations/requirements.txt services/translator-modal/.env.example services/translator-modal/evals/build_error_detection_cases.py services/translator-modal/evals/build_proofnetsharp_cases.py services/translator-modal/evals/cases_proofnetsharp_paragraph_smoke5.json services/translator-modal/evals/cases_proofnetsharp_paragraph.json services/translator-modal/evals/cases_proofnetsharp_proof1.json services/translator-modal/evals/cases.json services/translator-modal/evals/demo_algebra_topology.py services/translator-modal/evals/results/.gitignore services/translator-modal/modal_app.py services/translator-modal/pytest.ini services/translator-modal/query_http.py services/translator-modal/query_modal.py services/translator-modal/README.md services/translator-modal/requirements-dev.txt services/translator-modal/requirements-local.txt services/translator-modal/run_error_detection_benchmark.py services/translator-modal/run_eval_suite.py services/translator-modal/tests/test_build_error_detection_cases.py services/translator-modal/tests/test_error_detection_benchmark.py services/translator-modal/tests/test_eval_suite.py services/translator-modal/tests/test_modal_app_helpers.py ``` ### Dependencies - services/lean-backend/requirements.txt: fastapi@>=0.111,<1.0, httpx@>=0.27,<1.0, pydantic@>=2.7,<3.0, pytest@>=8.0,<9.0, uvicorn[standard]@>=0.30,<1.0 - services/perturbations/requirements.txt: datasets@>=2.14.0 ### Recent commits (newest first) - last push - assistant - Merge branch 'main' of https://github.com/aryans-15/treehacks-2026 - orz - Merge branch 'main' of https://github.com/aryans-15/treehacks-2026 - asdf - Merge branch 'main' of https://github.com/aryans-15/treehacks-2026 - auto complete - fixing positioning - 4.1 mini - more testing - logging - testing json - stash - scuffed - Merge branch 'main' of https://github.com/aryans-15/treehacks-2026 - Merge branch 'main' of https://github.com/aryans-15/treehacks-2026 - asdf - relax the heuristic - fix incompatibility ## Key source files (fetched from GitHub, selected and truncated for size) ### services/perturbations/requirements.txt ``` datasets>=2.14.0 ``` ### services/lean-backend/requirements.txt ``` fastapi>=0.111,<1.0 uvicorn[standard]>=0.30,<1.0 httpx>=0.27,<1.0 pydantic>=2.7,<3.0 pytest>=8.0,<9.0 ``` ### services/lean-backend/docker-compose.yml ```yaml services: lean-backend: build: context: . dockerfile: Dockerfile args: INSTALL_LEAN: ${INSTALL_LEAN:-true} env_file: - .env environment: LEAN_TEMP_DIR: ${LEAN_TEMP_DIR:-/lean-state/tmp} ELAN_HOME: ${ELAN_HOME:-/lean-state/elan} ports: - "8000:8000" volumes: - ${LEAN_STATE_DIR:-./.lean-state}:/lean-state command: uvicorn app.main:app --host 0.0.0.0 --port 8000 ``` ### services/lean-backend/Dockerfile ``` FROM python:3.11-slim ARG INSTALL_LEAN=true ENV PYTHONDONTWRITEBYTECODE=1 \ PYTHONUNBUFFERED=1 \ PIP_NO_CACHE_DIR=1 RUN apt-get update \ && apt-get install -y --no-install-recommends curl ca-certificates bash git \ && rm -rf /var/lib/apt/lists/* WORKDIR /srv/app COPY requirements.txt ./requirements.txt RUN pip install --upgrade pip && pip install -r requirements.txt RUN if [ "$INSTALL_LEAN" = "true" ]; then \ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y; \ /root/.elan/bin/elan default stable; \ ln -sf /root/.elan/bin/elan /usr/local/bin/elan; \ ln -sf /root/.elan/bin/lean /usr/local/bin/lean; \ ln -sf /root/.elan/bin/lake /usr/local/bin/lake; \ lean --version; \ lake --version; \ fi COPY app ./app COPY scripts ./scripts RUN chmod +x ./scripts/*.sh EXPOSE 8000 CMD ["uvicorn", "app.main:app", "--host", "0.0.0.0", "--port", "8000"] ``` ### services/lean-backend/app/main.py ```python from __future__ import annotations import logging import re import time import uuid from typing import Any from fastapi import FastAPI, HTTPException, Request from .highlight_llm import resolve_highlights_with_llm from .highlight_locator import resolve_highlights from .lean_compile import compile_lean from .llm_client import ( explain_issue_chat, interpret_errors, interpret_semantic_sanity, repair_lean_compile_errors, repair_lean_def_check, ) from .modal_client import ModalClientError, complete_autocomplete, generate_lean from .models import ( ChatExplainRequest, ChatExplainResponse, CompleteRequest, CompileResult, DashboardAdvice, Diagnostic, GeneratedLean, HighlightChunk, HighlightResolveRequest, HighlightResolveResponse, HighlightSentence, Interpretation, InterpretationItem, PipelineStage, PipelineTrace, SemanticValidation, SolveRequest, SolveResponse, ) from .settings import get_settings from .utils import configure_logging, request_id_ctx settings = get_settings() configure_logging(settings.log_level) logger = logging.getLogger(__name__) # Console log env-derived settings at startup so you can verify they exist _env_line = ( f"env_check ENABLE_LLM_INTERPRETATION={settings.enable_llm_interpretation} " f"LLM_MODEL={settings.llm_model or '(none)'} LLM_API_KEY_set={bool(settings.llm_api_key)} " f"LLM_ENDPOINT_URL={settings.llm_endpoint_url or '(default)'} " f"MODAL_ENDPOINT_URL={settings.modal_endpoint_url or '(none)'} " f"LAKE_PROJECT_DIR={settings.lake_project_dir or '(none)'}" ) print(_env_line, flush=True) logger.info("%s", _env_line) app = FastAPI(title="Lean Solver Backend", version="0.1.0") _FALSE_DECL_RE = re.compile( r"(?m)^\s*(?:axiom|theorem|lemma)\s+(?P[A-Za-z0-9_'.]+)\s*:\s*False(?:\b|$)" ) _FALSE_STDOUT_RE = re.compile( r"^\s*(?P[A-Za-z0-9_'.]+)(?:\s*\([^)]*\))*\s*:\s*False\s*$" ) _LEAN_CANONICAL_REPLACEMENTS: tuple[tuple[re.Pattern[str], str], ...] = ( (re.compile(r"\\mathbb\s*\{\s*N\s*\}", re.IGNORECASE), "Nat"), (re.compile(r"\\mathbb\s*\{\s*Z\s*\}", re.IGNORECASE), "Int"), (re.compile(r"\\mathbb\s*\{\s*Q\s*\}", re.IGNORECASE), "Rat"), (re.compile(r"\\mathbb\s*\{\s*R\s*\}", re.IGNORECASE), "Real"), ) _LEAN_UNICODE_SET_REPLACEMENTS = { "ℕ": "Nat", "ℤ": "Int", "ℚ": "Rat", "ℝ": "Real", } _CHAT_INLINE_MATH_RE = re.compile(r"[=<>+\-*/^|]|[≤≥≠∈∀∃ℕℤℚℝ]") def _format_chat_math_inline(value: str | None) -> str: text = str(value or "").strip() if not text: return "" if "$" in text or "`" in text: return text # Wrap compact math-like expressions, e.g. |a-b|=|b-a|. if len(text) <= 120 and _CHAT_INLINE_MATH_RE.search(text): return f"${text}$" return text @app.middleware("http") async def add_request_context(request: Request, call_next): request_id = request.headers.get("x-request-id") or str(uuid.uuid4()) token = request_id_ctx.set(request_id) logger.info("request_started method=%s path=%s", request.method, request.url.path) try: response = await call_next(request) response.headers["x-request-id"] = request_id logger.info( "request_completed method=%s path=%s status=%s", request.method, request.url.path, response.status_code, ) return response except Exception: logger.exception("request_failed method=%s path=%s", request.method, request.url.path) raise finally: request_id_ctx.reset(token) @app.get("/healthz") async def healthz() -> dict[str, str]: return {"status": "ok"} def _as_int(value: Any) -> int | None: if isinstance(value, bool): return None if isinstance(value, int): return value if isinstance(value, float) and value.is_integer(): return int(value) if isinstance(value, str): try: return int(value) except ValueError: return None return None def _parse_sentences(raw_sentences: Any) -> list[HighlightSentence]: if not isinstance(raw_sentences, list): return [] parsed: list[HighlightSentence] = [] for raw in raw_sentences: if not isinstance(raw, dict): continue sentence_id = raw.get("sentence_id") or raw.get("sentenceId") parsed.append( HighlightSentence( sentence_id=str(sentence_id) if sentence_id else None, start=_as_int(raw.get("start")), end=_as_int(raw.get("end")), text=str(raw.get("text")) if raw.get("text") is not None else None, ) ) return parsed def _parse_chunks_from_context(context: dict[str, Any], nl_input: str) -> list[HighlightChunk]: raw_chunks = context.get("chunks") chunks: list[HighlightChunk] = [] if isinstance(raw_chunks, list): for idx, raw in enumerate(raw_chunks): if not isinstance(raw, dict): continue chunk_id_raw = raw.get("chunk_id") or raw.get("chunkId") or f"chunk-{idx + 1}" chunk_id = str(chunk_id_raw).strip() or f"chunk-{idx + 1}" text = str(raw.get("text")) if raw.get("text") is not None else "" start = _as_int(raw.get("start")) if start is None: start = 0 end = _as_int(raw.get("end")) if end is None: end = start + len(text) parent_id_raw = raw.get("parent_id") or raw.get("parentId") parent_id = str(parent_id_raw) if parent_id_raw is not None else None chunks.append( HighlightChunk( chunk_id=chunk_id, text=text, start=start, end=end, parent_id=parent_id, sentences=_parse_sentences(raw.get("sentences")), [truncated — 35182 more characters] ``` ### benchmarks/rescore.py ```python #!/usr/bin/env python3 """Re-score existing benchmark JSON results with updated pipeline verdict logic. New rule: a well-typed axiom that Lean accepts (is_valid_lean=True, status=ok) counts as CORRECT, even if it's an unproven axiom. Only count as incorrect when compilation fails, status is needs_revision, or statement collapses to False. """ import json import sys from pathlib import Path def pipeline_says_correct(result: dict) -> bool | None: if "error" in result: return None valid = result.get("is_valid_lean") status = str(result.get("status", "")).lower() stmt_type = str(result.get("statement_type", "")).strip() if stmt_type == "False": return False if valid is False: return False if status not in ("ok", ""): return False return True def rescore(path: Path) -> None: data = json.loads(path.read_text()) results = data.get("results", []) gpt_correct, gpt_total = 0, 0 pipe_correct, pipe_total = 0, 0 gpt_costs, pipe_costs = [], [] gpt_lats, pipe_lats = [], [] for row in results: expected = row.get("expected_correct") gpt = row.get("gpt_baseline") if gpt and "error" not in gpt and gpt.get("is_correct") is not None: gpt_total += 1 if gpt["is_correct"] == expected: gpt_correct += 1 if gpt.get("cost_usd") is not None: gpt_costs.append(gpt["cost_usd"]) if gpt.get("latency_ms") is not None: gpt_lats.append(gpt["latency_ms"]) pipe = row.get("pipeline") if pipe and "error" not in pipe: verdict = pipeline_says_correct(pipe) if verdict is not None: pipe_total += 1 if verdict == expected: pipe_correct += 1 if pipe.get("cost_usd") is not None: pipe_costs.append(pipe["cost_usd"]) if pipe.get("latency_ms") is not None: pipe_lats.append(pipe["latency_ms"]) # Update summaries in-place if "gpt_summary" in data: data["gpt_summary"]["correct"] = gpt_correct data["gpt_summary"]["total"] = gpt_total data["gpt_summary"]["accuracy"] = gpt_correct / gpt_total if gpt_total else None if "pipeline_summary" in data: data["pipeline_summary"]["correct"] = pipe_correct data["pipeline_summary"]["total"] = pipe_total data["pipeline_summary"]["accuracy"] = pipe_correct / pipe_total if pipe_total else None path.write_text(json.dumps(data, ensure_ascii=False, indent=2)) print(f"{path.name}: GPT {gpt_correct}/{gpt_total} Pipeline {pipe_correct}/{pipe_total}") if __name__ == "__main__": results_dir = Path(__file__).resolve().parent / "results" files = sorted(results_dir.glob("benchmark-*.json")) for f in files: rescore(f) ``` ### apps/overleaf-extension/content.js ```javascript (() => { "use strict"; // Deprecated file. // Source of truth is now split across: // - content_shared.js // - content_adapters.js // - content_ui.js // - content_app.js // - content_bootstrap.js })(); ``` ### apps/overleaf-extension/content_bootstrap.js ```javascript (() => { "use strict"; if (window.__zetaFrontendV4) { return; } if (!location.hostname.endsWith("overleaf.com")) { return; } const zeta = window.__zetaContent; if (!zeta?.ZetaApp) { console.error("zeta bootstrap failed: ZetaApp module missing."); return; } window.__zetaFrontendV4 = true; const app = new zeta.ZetaApp(); app.init(); window.__zetaApp = app; window.__zetaDebug = { getChunkTree: () => app.chunkTree, getLeafChunks: () => (app.chunkTree ? app.chunkTree.leafChunks : []), getActiveChunkId: () => app.activeChunkId, getActiveChunk: () => { if (!app.chunkTree || !app.activeChunkId) { return null; } return app.chunkTree.chunkById.get(app.activeChunkId) || null; }, }; window.__zetaDestroy = () => { app.destroy(); delete window.__zetaDebug; delete window.__zetaApp; delete window.__zetaFrontendV4; }; })(); ``` ### .github/workflows/deploy.yml ```yaml name: Deploy to EC2 on: push: branches: [ "main" ] jobs: deploy: runs-on: ubuntu-latest steps: - name: Deploy over SSH uses: appleboy/ssh-action@v1.0.3 with: host: ${{ secrets.EC2_HOST }} username: ${{ secrets.EC2_USER }} key: ${{ secrets.EC2_SSH_KEY }} script: | set -e cd /home/ubuntu/treehacks-2026/services/lean-backend git fetch --all git reset --hard origin/main docker compose pull lean-backend || true docker compose up -d --build lean-backend # Wait for the API to accept connections before declaring success. HEALTH_URL="http://127.0.0.1:8000/healthz" ATTEMPTS=30 SLEEP_SECS=2 i=1 until curl -fsS "$HEALTH_URL" >/dev/null; do if [ "$i" -ge "$ATTEMPTS" ]; then echo "Health check failed after $ATTEMPTS attempts." docker compose ps docker compose logs --tail=200 lean-backend || true exit 1 fi echo "Waiting for service health ($i/$ATTEMPTS)..." i=$((i + 1)) sleep "$SLEEP_SECS" done docker image prune -f ``` ### benchmarks/run_benchmark.py ```python #!/usr/bin/env python3 """ Benchmark: GPT baseline vs Herald pipeline (NL → Lean → compile → feedback) For each test case (mix of correct, incorrect, and tricky math statements): 1. GPT baseline – single LLM call asking GPT to judge the statement 2. Pipeline – Herald /v1/analyze (translate → Lean compile → feedback) Tracks accuracy, latency, and estimated cost per query. Usage: python benchmarks/run_benchmark.py --openai-api-key sk-... OPENAI_API_KEY=sk-... python benchmarks/run_benchmark.py --model gpt-4.1 """ from __future__ import annotations import argparse import json import os import sys import time from datetime import datetime, timezone from pathlib import Path from typing import Any import requests # ── paths ────────────────────────────────────────────────────────────────── SCRIPT_DIR = Path(__file__).resolve().parent CASES_PATH = SCRIPT_DIR / "cases.json" RESULTS_DIR = SCRIPT_DIR / "results" # ── pricing ($ per 1M tokens for GPT, $ per GPU-hour for Modal) ────────── GPT_PRICING: dict[str, dict[str, float]] = { # model -> {input: $/1M tokens, output: $/1M tokens} "gpt-5.3": {"input": 3.00, "output": 12.00}, "gpt-4.1": {"input": 2.00, "output": 8.00}, "gpt-4.1-mini": {"input": 0.40, "output": 1.60}, "gpt-4.1-nano": {"input": 0.10, "output": 0.40}, "gpt-4o": {"input": 2.50, "output": 10.00}, "gpt-4o-mini": {"input": 0.15, "output": 0.60}, "gpt-3.5-turbo": {"input": 0.50, "output": 1.50}, } # Fallback pricing if model not in dict GPT_PRICING_DEFAULT = {"input": 2.00, "output": 8.00} # Modal L4 GPU ≈ $0.76/hr. Pipeline request time is a mix of GPU inference # + Lean compilation (CPU) + network. We use full request latency as a rough # upper-bound proxy for GPU-seconds. MODAL_GPU_HOURLY_RATE = 0.76 # $/hr def _gpt_cost(model: str, usage: dict[str, Any] | None) -> float | None: """Compute GPT cost in dollars from token usage.""" if not usage: return None pricing = GPT_PRICING.get(model, GPT_PRICING_DEFAULT) prompt = usage.get("prompt_tokens", 0) completion = usage.get("completion_tokens", 0) return (prompt * pricing["input"] + completion * pricing["output"]) / 1_000_000 def _pipeline_cost(latency_ms: float | None) -> float | None: """Estimate pipeline cost from request latency (rough upper bound).""" if latency_ms is None: return None return (latency_ms / 1000) * (MODAL_GPU_HOURLY_RATE / 3600) # ── GPT prompt ───────────────────────────────────────────────────────────── GPT_SYSTEM_PROMPT = """\ You are an expert mathematician and formal proof checker. Decide whether the given LaTeX mathematical statement is a PROVEN TRUE theorem, a FALSE statement, or an UNPROVEN conjecture. Rules: - Judge mathematical TRUTH, not LaTeX formatting. - A statement is "correct" ONLY if it is a proven mathematical theorem. - Famous unproven conjectures (Goldbach, Collatz, Riemann, etc.) must be marked is_correct: false with a note that they are unproven. - For universally quantified claims, one counterexample suffices to refute. - "Positive" means strictly > 0 unless stated otherwise. - Natural numbers include 0 unless the statement says otherwise. - Pay close attention to boundary conditions (≥ 5 vs ≥ 1, etc.). - Series "converges to X" means the partial sums have limit X in the standard (not Cesàro / Abel / regularized) sense. Respond with ONLY valid JSON (no markdown fences): { "is_correct": true | false, "confidence": "high" | "medium" | "low", "reasoning": "step-by-step reasoning (2-4 sentences)", "issues": [ {"description": "...", "severity": "error" | "warning" | "info"} ], "feedback": "1-2 sentence overall assessment", "counterexample": "a concrete counterexample if false, else null", "suggested_fix": "a corrected statement if wrong, else null" }""" GPT_USER_TEMPLATE = """\ Analyze this mathematical statement for correctness. Statement (LaTeX): {text} {context_line} Is this a proven mathematical theorem? Identify every issue.""" # ── helpers ──────────────────────────────────────────────────────────────── def load_cases(path: Path) -> list[dict[str, Any]]: data = json.loads(path.read_text(encoding="utf-8")) if not isinstance(data, list): raise ValueError(f"Expected JSON array in {path}") return data def call_gpt( text: str, context: str | None, *, api_key: str, model: str, timeout: int = 90, ) -> dict[str, Any]: """Single GPT call to analyse a LaTeX math statement.""" context_line = f"Context: {context}" if context else "" user_msg = GPT_USER_TEMPLATE.format(text=text, context_line=context_line) payload: dict[str, Any] = { "model": model, "messages": [ {"role": "system", "content": GPT_SYSTEM_PROMPT}, {"role": "user", "content": user_msg}, ], "temperature": 0.0, "response_format": {"type": "json_object"}, } started = time.time() try: resp = requests.post( "https://api.openai.com/v1/chat/completions", headers={ "Content-Type": "application/json", "Authorization": f"Bearer {api_key}", }, json=payload, timeout=timeout, ) latency_ms = (time.time() - started) * 1000 if resp.status_code != 200: return {"error": f"HTTP {resp.status_code}: {resp.text[:500]}", "latency_ms": latency_ms} data = resp.json() content = data["choices"][0]["message"]["content"] try: parsed = json.loads(content) except json.JSONDecodeError: parsed = {"raw_content": content, "is_correct": None} parsed["latency_ms"] = latency_ms parsed["model"] = model parsed["usage"] = data.get("usage") parsed["cost_usd"] = _gpt_cost(model, data.get("usage")) return parsed except Exception as exc [truncated — 15283 more characters] ``` [35 more indexed source files omitted to keep this export small. The full file list is in the Codebase structure section above.]