Thanks for your interest in contributing to Bourbaki.
- Python 3.11+
- Bun (for the TUI)
- At least one LLM API key (see below)
- Optional: Lean 4 + Mathlib for formal verification
Copy the example environment file and fill in your keys:
cp .env.example .envAPI keys (at least one LLM key required):
| Key | Service | Required |
|---|---|---|
OPENROUTER_API_KEY |
OpenRouter — access many models with one key | Recommended |
OPENAI_API_KEY |
OpenAI — GPT-4, GPT-5, etc. | Or any other LLM key |
ANTHROPIC_API_KEY |
Anthropic — Claude models | Or any other LLM key |
GOOGLE_API_KEY |
Google AI — Gemini models | Optional |
XAI_API_KEY |
xAI — Grok models | Optional |
OLLAMA_CLOUD_API_KEY |
Ollama Cloud | Optional |
EXASEARCH_API_KEY |
Exa — web/paper search | Optional |
TAVILY_API_KEY |
Tavily — alternative search | Optional |
For local Ollama, no key needed — just have ollama serve running.
For Lean 4 verification, set LEAN_PATH to a Lean project with Mathlib.
# Backend
cd backend
pip install -e ".[dev]"
uvicorn bourbaki.main:app --reload --port 8000
# TUI (separate terminal)
bun install
bun start# Python backend tests
cd backend && pytest
# TypeScript type checking
bun run typecheck- Fork the repo and create a branch from
master - Make your changes
- Run
pytestandbun run typecheckto verify nothing is broken - Open a PR against
master
- Python: formatted with Ruff (
ruff check/ruff format) - TypeScript: standard TypeScript with strict mode
backend/bourbaki/— Python backend (FastAPI + Pydantic AI)src/— TypeScript TUI (React + Ink)src/skills/— SKILL.md proof technique files
See ARCHITECTURE.md for detailed system design.
Skills are Markdown files in src/skills/. To add one:
- Create
src/skills/your-technique/SKILL.md - Add YAML frontmatter with
name,description,tags - Write the proof strategy instructions in the body
- The backend discovers it automatically — no code changes needed
By contributing, you agree that your contributions will be licensed under the MIT License.