vibe proving is an AI platform designed for students and researchers in mathematics. It combines language models with theorem retrieval to provide interactive workflows for learning, problem-solving, proof review, and knowledge discovery.
- Learning Mode — Generate structured explanations with prerequisites, proofs, examples, and extensions
- Solving Mode — Automated proof generation with citation verification and confidence scoring
- Review Mode — Structured analysis of mathematical writing (LaTeX/PDF/images)
- Search Mode — Semantic search across 9M+ theorems from arXiv and mathematical databases
|
Learning Mode |
Problem Solving |
|
Proof Review |
Literature Search |
|
Formalization |
Transform mathematical statements into comprehensive learning resources:
- Background context and motivation
- Prerequisite knowledge with definitions
- Step-by-step proof walkthrough
- Concrete examples and counterexamples
- Extensions and related topics
Target difficulty levels: undergraduate or graduate.
Generator–Verifier–Reviser pipeline:
- Direct retrieval from theorem databases
- Proof generation with reasoning steps
- Independent verification
- Citation checking via TheoremSearch
- Counterexample testing
- Confidence scoring with explicit uncertainty
Automated analysis:
- Logic Consistency: Detect missing steps, circular reasoning
- Citation Accuracy: Verify referenced theorems
- Symbol Consistency: Track variable scope
Supported formats: Text, LaTeX, images (via vision models), PDF (via OCR).
Semantic search:
- 9M+ theorems from arXiv, Stacks Project, and specialized databases
- Natural language queries
- Similarity ranking
- Direct links to papers
Powered by Harmonic Aristotle:
- Submit natural language mathematical statements
- Automatic translation to Lean 4 code
- Integrated with Mathlib theorem database
- Real-time compilation and verification
Requirements: Python 3.11+ or Docker
Install and start Docker first: Docker Desktop for Windows/macOS, or Docker Engine on Linux. Then configure and run:
git clone https://github.com/ml1301215/vibe-proving-math.git
cd vibe-proving-math
cp app/config.example.toml app/config.toml
# Edit app/config.toml:
# - set [auth].superuser_password
# - add your [llm] API endpoint/key/model
docker compose up -d
docker compose ps
docker compose logs -fAccess: http://localhost:8080/ui/
Stop service: docker compose down
git clone https://github.com/ml1301215/vibe-proving-math.git
cd vibe-proving-math
python3 -m venv .venv
source .venv/bin/activate
pip install -r requirements.txt
cp app/config.example.toml app/config.toml
# Edit app/config.toml and add your superuser password and API keys
cd app
python -m uvicorn api.server:app --host 127.0.0.1 --port 8080git clone https://github.com/ml1301215/vibe-proving-math.git
cd vibe-proving-math
python -m venv .venv
.venv\Scripts\Activate.ps1
pip install -r requirements.txt
copy app\config.example.toml app\config.toml
# Edit app\config.toml and add your superuser password and API keys
cd app
python -m uvicorn api.server:app --host 127.0.0.1 --port 8080For Command Prompt, use .venv\Scripts\activate.bat instead of .venv\Scripts\Activate.ps1.
Access: http://127.0.0.1:8080/ui/ or http://localhost:8080/ui/
Configuration is read from app/config.toml. Copy app/config.example.toml first, then edit these required fields:
[auth]
superuser_username = "dev_user"
superuser_password = "change-this-password"
session_days = 30
default_quota = 50
allow_register = true
[llm]
base_url = "https://api.deepseek.com/v1"
api_key = "your-api-key"
model = "deepseek-chat"Authentication uses one unified user system:
- The configured superuser can modify API settings from the right-side settings panel.
- Regular registered users can use the application but cannot see or edit API keys/base URLs.
- Login sessions are stored in an HTTP-only cookie and remain valid for
[auth].session_days.
Optional services:
[nanonets]enables Nanonets OCR for PDF review.[mineru]uses the MinerU Agent Lightweight Extract API and does not require a token.[aristotle]enables Harmonic Aristotle formalization.doclingis not installed by default because it pulls large local OCR/ML dependencies. Install it manually only if you want local Docling fallback:python -m pip install "docling>=2.0.0"
mindmap
root((vibe proving))
Frontend
HTML5
CSS3
Responsive layout
Theme toggle
Motion / transitions
JavaScript ES6+
AppState
SSE client
Event handling
CDN deps
KaTeX
marked.js Markdown
Backend
Python 3.11+
FastAPI
Async I/O
SSE
OpenAPI docs
Uvicorn
ASGI server
Core libs
TOML config
HTTP client
External services
LLM API
DeepSeek v4 Pro
Gemini 3.1 Pro
Custom endpoints
Theorem Search
Nanonets OCR
MinerU Agent
Aristotle Lean 4
DevOps
Deployment
Docker optional
Nginx reverse proxy
Key Components:
- Frontend: Single-page app with real-time streaming and KaTeX rendering
- Backend: FastAPI with SSE support for progressive responses
- LLM Integration: OpenAI-compatible interface (DeepSeek, Gemini, OpenAI)
- Theorem Retrieval: TheoremSearch API for citation verification
- Formalization: Harmonic Aristotle for Lean 4 code generation
- PDF Processing: Nanonets OCR and MinerU Agent for formula-preserving extraction
- User System: SQLite-backed accounts, session cookies, per-user quotas, and a configurable superuser for API administration
We welcome contributions from the mathematical community:
- Bug Reports: GitHub Issues
- Code Contributions: See CONTRIBUTING.md
- TheoremSearch — Semantic theorem retrieval
- Harmonic Aristotle — Automated formalization
- Research Math Assistant — Mathematical research assistant
- Rethlas — Natural language reasoning system
- Aletheia — Generator–Verifier–Reviser architecture
- LATRACE — Long-term memory system
- Nanonets OCR — Formula-aware PDF extraction
QQ Group: 1093249787
GitHub Issues: github.com/ml1301215/vibe-proving-math/issues