Inspiration

Mathematical proofs and derivations are notoriously difficult to audit. A single misplaced sign or subtle logical gap early in a complex equation can invalidate pages of work. We wanted to build a tool that acts as an intelligent co-pilot for mathematicians, students, and researchers—automating the tedious verification process and highlighting logical flaws instantly.

What it does

ProofMesh is an advanced math proof verification platform. Users can input or upload complex proofs (including scanned documents via automated OCR), and the system breaks them down step-by-step. It uses a multi-stage architecture powered by specialized models to cross-check logical transitions, validate LaTeX expressions, and flag errors with plain-language explanations.

How we built it

Frontend & UI: Built with Streamlit for rapid, interactive user presentation and live feedback.

Core Pipeline & Parsing: Python backend handling PDF text extraction, document parsing, and step segmentation.

LLM Orchestration: Integrated via Featherless's serverless inference endpoints to query open-source math models on demand.

Multi-Stage Validation:

  1. Extraction Stage: Parses raw text or images into structured sequential steps.

  2. Math-Check Stage: Evaluates step-to-step mathematical consistency using specialized math models.

  3. Judge Stage: Summarizes flagged issues and delivers clear, user-friendly verdicts.

    Challenges we ran into

    Handling Strict JSON Schemas: LLMs occasionally stray from strict output formats. We built resilient parsing fallbacks (fence-stripping, bracket extraction, and Python literal evaluation) to reliably convert messy model text into structured data.

Accomplishments that we're proud of

Implementing a seamless provider-agnostic client configuration that lets us switch backends cleanly via environment variables/secrets.

Designing a robust multi-tier pipeline that goes all the way from raw PDF ingestion/OCR to final synthesized judge verdicts.

What we learned

The importance of defensive coding when working with large language models for structured reasoning tasks.

How combining domain-specific models with reasoning judges creates significantly more reliable outputs than a single general-purpose prompt.

What's next for ProofMesh

Expanding support for more formal theorem provers.

Enhancing the interactive UI for real-time collaborative proof editing.

Optimizing inference latency for larger multi-page mathematical documents.

Built With

Share this project:

Updates

Submission history