Theoremis
An AI-native workspace for mathematics, built around proofs you can actually check.
Explore conjectures, write mathematics, and collaborate with AI inside your document—then use Lean 4 and Mathlib to distinguish a convincing explanation from a machine-checked proof.
Free, open-source desktop application · Public beta · macOS, Windows & Linux
Download Theoremis → · Latest release · Explore the source
[!NOTE]
Public beta: ChatGPT, Ollama and Lean 4 checking are available, but the workflows are still evolving. Keep backups of important work and review AI suggestions before accepting them.
Why Theoremis?
Mathematical work often happens across separate editors, chats, and proof assistants. Theoremis brings these activities into one workspace, without conflating AI-generated reasoning with mathematical verification.
- Write mathematics naturally. Markdown and LaTeX editing, numbered equations (including rows of
align), and a toggle between rendered output and TeX source.
- Keep track of what's established. Statements can be open, tested, draft, adopted, proved, or verified. Status indicators in the gutter and sidebar show where a proof stands.
- Reason alongside AI. Highlight a step or work in one of five modes: Explore, Find gaps, Challenge, Formalize, and Is it known?, which searches arXiv and Crossref and answers from what it finds, citing each paper, so you can add it to your references in one click. Feedback stays attached to its document context.
- Manual, Auto or Seminar. In Manual the collaborator proposes and you decide. In Auto it does the work itself: it edits the document, writes Lean and checks it until Lean accepts, draws graphs, and reads the rest of the project. In Seminar it convenes a few members, each with its own objective (a Prover, a Skeptic, a Formalizer…), who work on the document at the same time while you watch each one's orb. Every change is marked, listed step by step, and undone in one click. Only Lean can make a statement verified, even in Auto.
- Check proofs with Lean 4. Generate Lean code using Mathlib, run Check with Lean, inspect errors or dependencies on
sorry, and mark a step verified only when the checker accepts it under the app's checks.
- Bring in your research. Import PDFs, photos of handwritten notes or a blackboard, LaTeX, Markdown, Word, HTML, Jupyter notebooks, CSV or code. A vision model transcribes them into statements with statuses, figures are copied straight from the PDF, and every paragraph links back to its page in the original.
- Graph in 2D and 3D.
graph and graph3d blocks put a graphing calculator in the document: curves, implicit curves, regions, polar and parametric plots, sliders you can play, surfaces and curves in space. The collaborator can draw them too.
- Show the collaborator anything. Attach images, PDFs and files to a question, and paste screenshots straight into a paragraph.
- Your macros and references. Paste your paper's preamble and the document renders with your
\newcommands. Keep references as BibTeX, add one by arXiv id or DOI, and write \cite{key}: citations are numbered as the exported paper will number them.
- Export as LaTeX, print as PDF. Export an amsart source for pdfLaTeX, with theorems and proofs in amsthm environments, equations numbered as in Theoremis, graphs and figures as files and a
references.bib, as one ZIP ready for Overleaf or arXiv. Or print, and save as PDF.
- Never lose a version. Theoremis keeps versions of every document as you work and before the collaborator changes it, and brings any of them back.
- Work with co-authors. Keep the workspace in a folder Dropbox, iCloud Drive or OneDrive shares; if a document changes in two places at once, both versions are kept. Or send one document as a
.theoremis file.
- Stay in control of edits. Proposed rewrites show the original and replacement; accept, edit, reject, or undo. AI messages are explicitly labeled not verified.
- Work locally. Documents and threads are stored as files on your machine, in a folder you choose. Use a local Ollama model or connect a ChatGPT account.
From an idea to a checked proof
- Write a conjecture or a draft argument using Markdown and LaTeX, or import the paper or notes you already have.
- Select a step and use Find gaps or Challenge to pressure-test the reasoning.
- Choose Formalize to generate a candidate Lean 4 proof.
- Run Check with Lean against Mathlib. If Lean reports errors or
sorry, send the diagnostic back to the collaborator.
- When the checker accepts an eligible proof, mark the statement verified. Until then, the AI's suggestions remain unverified.
This separates exploration, which AI can help accelerate, from verification, which requires more than a plausible-sounding response.
Built as a desktop product
| Area | Implementation |
|---|
| Desktop and UI | Tauri, Rust, React, TypeScript |
| AI collaboration | Sign in with ChatGPT (OAuth + PKCE), or connect to local Ollama models; a reasoning effort per model, from Instant to Max as each model allows; Manual proposals, an Auto agent with document, Lean and graph tools, or a Seminar of agents working at once |
| Formal checking | Lean 4, Mathlib, lake env lean, theorem/axiom inspection |
| Imports and graphs | pdf.js (text layer, rendering, figure detection), vision models, three.js, an expression language compiled without eval |
| Documents | Local JSON files, autosave, versions, per-document conversation threads; LaTeX (amsart, BibTeX) export, print to PDF, shared folders and .theoremis files |
| References | BibTeX with amsplain numbering; lookup by arXiv id or DOI and literature search on arXiv and Crossref, free and keyless |
| Security-minded design | Encrypted sign-in credentials using an OS-keychain-backed key; AI edits require user approval |
| Distribution | macOS (Apple silicon and Intel), Windows and Linux installers; GitHub Actions CI and signed automatic updates |
Engineering choices
Native backend, web interface. The Rust backend handles network calls, model streaming, authentication, storage, and Lean integration. React handles document editing and the collaborator. Tauri channels carry streamed replies into the interface.
Authentication stays outside the webview. The ChatGPT sign-in flow uses OAuth/PKCE and a loopback callback; tokens are encrypted at rest with a key from the system keychain. The application doesn't require an embedded API key.
AI output is not a proof. The Lean integration distinguishes accepted code, code that depends on sorry, and code that fails to compile. It reports unexpected axioms and screens out certain unsafe Lean constructs. These checks are not a complete sandbox for arbitrary code.
A real release pipeline. CI runs interface and backend checks. App changes trigger cross-platform release builds and signed update artifacts; installed copies can offer a restart when an update is ready.
For how the pieces fit together and why, see the architecture guide. For implementation details, source layout, and local data paths, see the developer guide. For release automation and signing, see the release guide.
Download and setup
Download the public beta at theoremis.com or select an installer from GitHub Releases.
On first launch, choose a blank document or the included Figurate numbers example project, then connect a model:
- ChatGPT: Open Settings → ChatGPT → Sign in with ChatGPT. The collaborator uses your connected ChatGPT account, subject to its usage limits. Prompts and relevant context are sent to the remote provider; local file storage does not mean this mode is offline.
- Ollama: Install Ollama, pull a supported model, and choose it in Theoremis. With a locally configured Ollama server, inference can remain on your machine.
- Lean 4 + Mathlib: Go to Settings → Lean 4 & Mathlib → Set up. Setup installs or configures Lean and downloads a Mathlib project with prebuilt libraries. Allow roughly 5 GB of disk space; Git is required.
[!IMPORTANT]
Current beta distributions have platform signing limitations. macOS may require System Settings → Privacy & Security → Open Anyway and Windows may display a SmartScreen prompt. See release and signing details.
Develop locally
Prerequisites: Node.js 20+, stable Rust, and Tauri system dependencies.
git clone https://github.com/adamouks/theoremis.git
cd theoremis/app
npm install
npm run tauri dev
See DEVELOPMENT.md for testing, architecture, Ollama and Lean setup, and website development.
Project structure
app/
src/ React + TypeScript UI
src-tauri/src/ Rust backend (ChatGPT, Ollama, Lean, storage)
site/ theoremis.com static site
docs/ screenshots, developer and release documentation
architecture.md how Theoremis works, and why it is built this way
.github/workflows/ CI and cross-platform releases
Roadmap
- Update Mathlib from inside the app
- Document cross-references that renumber automatically
- Signed releases: the workflows sign and notarize as soon as the certificates are in place (RELEASING.md)
- zbMATH Open in literature search
These are planned capabilities, not promises of release dates.
Open source
Theoremis is free and open source under the MIT License. Contributions, bug reports, and feedback are welcome through GitHub Issues.
The collaborator's visual effects include code from Libraries.dev (MIT) and React Bits (MIT with the Commons Clause), with patterns from Vercel AI Elements (Apache-2.0) and Prompt Kit (MIT). Their notices are in THIRD_PARTY_NOTICES.md.
Try Theoremis · Download installers
