The Adjoint is an interactive environment for exploring and building mathematical proofs together with state-of-the-art AI models. The goal is to streamline collaboration with LLMs to prove mathematical statements.
It’s built around a simple workflow:
- Explore: to turn a problem or a question into candidate statements together with their assumptions.
- Prove: to transform a first proof into a structured proof, decomposed into smaller lemmas, that you can easily iterate on.
- Write: to write and iterate on mathematical notes, check and review statements.
Write a mathematical document with direct in-context actions (chat, prove, review,...)
Extract LaTeX directly from documents
Interact with your favorite LLMs through a chat
Review notes artifacts (lemmas, propositions, theorems,...). Those are automatically extracted through a regex heuristic if in proper LaTeX environment.
Check artifact consistency and send to the prover mode if needed.
Structure the initial AI-suggested proof into a proof structured in sublemmas.
Switch to a dependency graph view to understand how steps connect.
Ask for edits in chat or directly edit the proposed proof.
Keep a version history so you can revisit earlier attempts.
And last but not least, Export to LaTeX (proof.tex).
- Node.js 18+
cd adjoint
npm installCreate adjoint/.env.local where you should specify either Gemini or OpenAI API keys.
Google (Gemini)
LLM_PROVIDER=googleai
GEMINI_API_KEY=your-keyOpenAI
LLM_PROVIDER=openai
OPENAI_API_KEY=your-keyAnthropic
LLM_PROVIDER=anthropic
ANTHROPIC_API_KEY=your-keynpm run devThen open the Adjoint at http://localhost:9002 (or whatever port you configured).
There is still a lot of work to do. From better prompts for all internal AI models to validation with either symbolic engines (like Sympy) and formal engines (like Lean or Rocq) or literature exploration...
Issues and pull requests are welcome.
If you’re planning a substantial change, please open an issue first so we can discuss direction.
MIT — see LICENSE.