Theoremis BETA

BETA Built for

ChatGPT and

Ollama →

Mathematics, reimagined for the age of AI.

Theoremis is the AI-native workspace for mathematics. Bring in your papers and notes, develop proofs, graph them and check them in Lean, with an AI collaborator that proposes, or, in Auto mode, does the work itself.

Download Theoremis View on GitHub↗

Works across all platforms

Free and open source · Public beta · Local-first desktop app

Figurate numbers/Sums of odd integers

Saved RenderedTeX Focus⌘. ···

Élise Moreau · Revision 1 · Edited 2 min ago

Sums of odd integers

We prove and look for an argument that extends to runs of odd integers that do not start at 1.

OPENtested to

Conjecture 1. For every integer , the sum of the first odd positive integers is :

(1)

DRAFTnot formalized

Proof. By induction on . The case reads . Suppose (1) holds for some . Adding the next odd number, , to both sides gives

(2) (3)

Proposed revisionFind gaps · open in review

Hence (1) holds for , and therefore for every .

Runs that do not start at 1

OPEN

Question 3. Which positive integers are sums of two or more consecutive odd integers?

Collaborator/Review of Proof (2)–(3)

GPT-5

ÉMÉlise10:42

SELECTION · PROOF · (2)–(3)FIND GAPS

(2) (3)

Is this fully justified as written?

CollaboratorFind gaps · Medium · 10:42NOT VERIFIED

Thought for 2 seconds

Sound overall. One step is left implicit.

Implicit step in (2)MINOR

(2) splits off the term and applies the hypothesis in one step. Both moves are valid; the use of (1) is not shown.

1Proposed revisionProof · (2)–(3)

ORIGINAL

(2) (3)

PROPOSED

(2) by (1)(3) (4)

AcceptEditRejectCompare

Selection · Proof · (2)–(3) + Context+ File

Medium ManualAutoSeminar

Ask a follow-up, or challenge a step…

ExploreFind gapsChallengeFormalizeIs it known?

Collaborator output is model reasoning, not a checked proof.

Fig. 1. A review in progress. The collaborator flags an implicit step; the author compares, then accepts the revision.

§1What it does

From first conjecture to the final

Theoremis holds the whole arc of mathematical work in one place: the exploration, the argument, and the scrutiny it has to survive.

(i)

Bring in your research

Import a paper, a photo of your notes, LaTeX, Word or a notebook, and continue from there. Figures come straight from the page.

Import⌘O

(ii)

Explore conjectures

State a conjecture, test it numerically, and study the structures behind it before committing to a proof.

Explore

(iii)

Develop proofs

Write in a typeset document with numbered results, aligned equations and cross-references that stay correct as the argument grows.

TeX

(iv)

Graph it

Plot curves, regions and surfaces in 2D and 3D, with sliders, inside the document.

Graph

(v)

Question assumptions

Ask the collaborator to challenge a step, search for counterexamples, or argue the other side.

Challenge

(vi)

Refine reasoning

See where an argument is thin, and compare your original step with a proposed revision before deciding.

Find gaps

(vii)

Collaborate in place

Select a line, ask, review and continue. The conversation stays attached to the mathematics it concerns.

Ask⌘L

(viii)

Hand it off

Switch to Auto and the collaborator does the work itself: edits, Lean, graphs. Every change is listed and undoable.

Auto

(ix)

Check in Lean 4

Formalize a step and check it against Mathlib on your computer. A proof Lean accepts can mark the step verified.

Lean 4 · beta

(x)

Ask what’s known

Is it known? searches arXiv and Crossref, answers from what it finds and cites each paper, which goes into your references in one click.

Is it known?

(xi)

Cite and export

Your macros, your BibTeX and \cite, numbered as the paper will be. Export LaTeX for Overleaf or arXiv, or print to PDF.

.tex · .bib

(xii)

Work with co-authors

Keep the workspace in a shared Dropbox, iCloud Drive or OneDrive folder; if a document changes in two places at once, both versions are kept. Every document keeps its earlier versions.

Shared folder

§2The workspace

The proof in the centre. The AI in the margins.

Your mathematics is set in serif and owned by you. Everything the collaborator contributes is marked, anchored and waits for your decision.

FIG. 2.1

A document that knows its own status

Every statement carries its standing: open, drafted, tested or verified. You can see at a glance what has been established and what is still a hope.

OPENtested to

Conjecture 1. For every integer , the sum of the first odd positive integers is :

(1)

DRAFTnot formalized

Proof. By induction on . The case reads . Suppose (1) holds for some .

FIG. 2.2

A collaborator that reads the argument

Select any step and ask. Findings come back pinned to the exact line they concern, with a severity and a short explanation.

(2)

1Implicit step in (2)MINOR

Splits off the term and applies the hypothesis in one step. Both moves are valid; the use of (1) is not shown.

COLLABORATOR · NOT VERIFIED

FIG. 2.3

Revisions you review before they land

Proposed changes sit beside your original reasoning. Accept, edit or reject. Nothing enters the proof without your decision.

ORIGINAL

PROPOSEDby (1)

Accept⌘↵ Edit Reject Compare

FIG. 2.4

Rigor you can read

AI output is always marked unverified. Numerical evidence is labelled as evidence. Only a proof checked in Lean earns a filled

OPENStated, not yet proved

TESTEDNumerical evidence, not a proof

SUGGESTEDFrom the collaborator, not verified

DRAFTProof in progress

PROVEDChecked by hand

VERIFIEDChecked in Lean

§3Auto mode

Ask for the proof. Get it checked.

Switch the collaborator to Auto and it works on the document itself: it rewrites steps, adds lemmas, writes the Lean and reads Lean’s errors until the proof is accepted, draws the graph, and reads the rest of your project. Switch to Seminar and it convenes a few members instead, a Prover, a Skeptic, a Formalizer, each with an objective of its own, who work on the document at the same time. Every step is listed, every change is marked, and one click takes it all back.

FIG. 3.1

Manual, Auto or Seminar, your call

Manual keeps the collaborator in the margins, proposing. Auto lets it do the work. Seminar shares the work among several members at once. Switch any time, from the composer.

+ Context + File ManualAutoSeminar

Formalize Theorem 1, check it in Lean, and graph the partial sums against .

MANUALProposes rewrites and additions. Nothing changes until you accept. AUTOEdits the document, runs Lean, draws graphs, and reports back. SEMINARConvenes a few members, each with its own objective, who do all of that at once.

FIG. 3.2

Every step on the record

The reply shows what it wrote and what it did, in order, with Lean’s errors under Details. Blocks it wrote are tagged AUTO until you edit them.

CollaboratorAUTOLEAN CHECKED

I'll formalize Theorem 1 and check it in Lean.

Read the document

!Lean found 1 errorDetails

That lemma doesn't exist; the step lemma is Finset.sum_range_succ.

Lean accepted the proof · Theorem 1 (1) is verifiedShow

Checked a graph

Added “The partial sums against ”Show

3 changes to the document.Undo all

01It does the workRewrites a step, adds a lemma or a remark, sets statuses, retitles the document, and reads the rest of the project for context.

02Lean until it passesIt writes the formalization, checks it, reads the errors and tries again. A statement turns verified only when Lean accepts the proof.

03Everything undoableEach change is recorded on the reply. Undo all puts the document back as it was, and your own edits since are kept.

Auto needs a model that can use tools: any ChatGPT model, or an Ollama model such as Qwen 3. Even in Auto, only Lean can verify a statement, and only you can mark one proved.

§4Bring your research

Start from the paper you already have.

Drop in a PDF, a photo of the blackboard, a LaTeX source or a Word file. A vision model transcribes it into statements with their statuses, figures are copied straight from the page, and every paragraph links back to where it came from.

FIG. 4.1

Figures found in the page itself

Theoremis reads what each PDF page draws (plots, diagrams and their labels), so a figure is cropped exactly as printed, never redrawn.

On Sums of Consecutive Odd Integers

A. Example and B. Sample

Theorem 1. For every n ≥ 1, the sum of the first n odd numbers is n².

Figure 1: Partial sums of the odd numbers against n².

F1The figure, as the model sees it: found in what the page draws

FIG. 4.2

A document you can work in

The transcription arrives as ordinary Theoremis blocks: numbered equations, statuses to argue with, and a page chip that opens the original beside it.

OPENp. 3

Theorem 1. For every , the sum of the first odd numbers is :

(1)

Figure 1: Partial sums of the odd numbers against .

PDFPhotos & scansLaTeXMarkdownWordHTMLJupyterCSVCode

Long papers are transcribed a few pages at a time, and an interrupted import continues where it stopped. Without a model, every format still converts directly. Attach the same files to a question and the collaborator reads them too, pages and photos included for models that can see.

§5Graphs

A graphing calculator in every document.

Write y = a\sin(bx) in a graph block and the plot appears, with a slider for every constant. In the plane or in space, typed in LaTeX or plain notation. The collaborator draws them too, and in Auto it checks a graph before it adds one.

FIG. 5.1

In the plane

Pan, zoom, trace a curve, play a slider. Every change is written back to the block, so the graph is part of the text.

▶03

label = max

FIG. 5.2

In space

Turn it by dragging. Surfaces, implicit surfaces like , parametric surfaces and curves.

The surface z = sin x cos y in a box, drawn by a 3D graph block

[0, 2π]²

2Dcurvesimplicit curvesregionspolarparametricpointssliders3Dsurfacesimplicit surfacesparametric surfacesspace curves

§6Models

Made for ChatGPT and Ollama.

Sign in with ChatGPT and the collaborator runs on your own plan, such as Plus or Pro. Or run open models with Ollama, entirely on your computer. Theoremis is a dedicated mathematical environment, not a chatbot: the model provides the reasoning, and Theoremis provides the document, the structure and the review around it. Both are in beta.

Connect

Choose the context

Select a step, a lemma or a section. You see exactly what is shared before you ask.

Review what returns

In Manual, findings arrive as marked suggestions, never as silent edits. In Auto, changes are made for you, listed and undoable.

ON YOUR MACHINE Your document Sums of odd integers

THEOREMIS Context and review Proof (2)–(3), uses (1)

YOUR MODEL

ChatGPT

Ollama Your plan, or this computer

SENT

Your selection, the results it cites, and your question.

RETURNED

One finding and one proposed revision, marked as model reasoning.

1NOT VERIFIED

§7Providers

One workspace. Your choice of model.

ChatGPT and Ollama, both in beta. The collaborator runs on the ChatGPT plan you already have, or on open models on your own computer. No API keys, and nothing billed per request.

AVAILABLE · BETA

ChatGPT Sign in with your ChatGPT account and the collaborator uses your plan. Every model reads images and works in Auto. MODELSThose your plan includes How it connects →

AVAILABLE · BETA

Ollama Run open models such as Qwen 3 or Llama on your own computer. Nothing leaves it. Vision models read pages and photos; models with tools work in Auto. MODELSAny model you pull Get Ollama ↗

§8Formal checking

Check it in Lean 4. BETA

Formalize a step and Theoremis checks it with Lean 4 against Mathlib, on your computer. If Lean accepts the proof and nothing in it rests on sorry, you can mark the step verified. If not, Lean's errors go back to the collaborator in one click, and in Auto mode it reads them and tries again on its own.

01FormalizeThe collaborator writes the step as a Lean 4 theorem that imports Mathlib.

02Check with LeanLean runs on your computer and reports errors, any sorry, and the axioms each proof uses.

03Mark it verifiedA proof Lean accepts can move the step to VERIFIED, checked in Lean. Nothing else can, in Manual or Auto.

Dashed, because it is new: setup installs Lean and downloads Mathlib (about 5 GB), and a first formalization often needs a few rounds of fixes.

§9Principles

Mathematicians should not be replaced by AI. They should be empowered by better tools.

Axiom 1 (Open). Theoremis is free to use, and its source is public. Read it, audit it, extend it.

Axiom 2 (Local). Your documents live on your machine, in files you own.

Axiom 3 (For mathematicians). Typeset documents, numbered results and a review process designed around proofs.

Axiom 4 (Your model). Bring your own AI: your ChatGPT plan, or open models running on your machine with Ollama.

Axiom 5 (Agency). The mathematician decides how much the collaborator may do: propose, or act. Whatever it does is marked, and can be undone.

Axiom 6 (Rigor). Model reasoning stays marked unverified until something stronger checks it.

Built in the openRead the source, file an issue, or propose a change.

View on GitHub↗

§10Status

Theoremis is in beta.

Everything here works and is ready to try on real mathematics, but it is early. So that you know where the edges are:

(i)

It will change

Features, screens and the way documents are saved may change between versions. Updates install themselves.

Updates

(ii)

Expect rough edges

Some things will break. Keep your own copies of work that matters; your documents are plain files on your computer.

Back up

(iii)

The collaborator is not a proof checker

Replies from ChatGPT or Ollama are model reasoning, marked unverified. Only Lean checks anything.

NOT VERIFIED

(iv)

Lean 4 is the newest part

Setup downloads several gigabytes and needs Git, and the first check after a restart can take a minute.

Lean 4 · beta

(v)

The installers are not signed yet

macOS and Windows ask for confirmation the first time you open Theoremis.

First launch

(vi)

Auto and Seminar are new

They edit your document on their own. Read what it did, and use Undo all when it gets something wrong.

Auto · beta

(vii)

Transcription is only as good as the model

Check an imported paper against its original; every paragraph links to its page.

p. 3

Found a problem or missing something? Open an issue on GitHub ↗

A better environment for mathematical thought.

Free and open source. In beta, for ChatGPT and Ollama.

Download Theoremis View on GitHub↗

Works across all platforms: macOS, Windows and Linux

Release notes and integration news, a few times a year.