Theoremis

Works with ChatGPT

Poe and OpenRouter coming soon →

Mathematics, reimagined for the age of AI.

Theoremis is the AI-native workspace for mathematics. Explore conjectures, develop proofs and test every step with an AI collaborator that works inside your document.

Download Theoremis View on GitHub↗

Free and open source · Local-first desktop app

PROJECTS

Figurate numbers

Sums of odd integers

Nicomachus’s theorem

Faulhaber’s formula

Centered squares

Additive bases

Partition congruences

Figurate numbers/Sums of odd integers

Saved locally RenderedTeX

Élise Moreau · Revision 7 · Edited 2 min ago

Sums of odd integers

OPEN tested to

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

(1)

DRAFT not formalized

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

(2) (3)

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

SUGGESTEDnot verified

Remark 2 (a direct proof). Since , the sum in (1) telescopes:

Lemma verified in Mathlib · this use is not RejectEditAccept

Collaborator/Review

ChatGPTGPT-6.1 Sol

ÉMÉlise10:42

SELECTION · PROOF (2)–(3)USES (1)

Is (2) fully justified as written?

CollaboratorFind gaps

NOT VERIFIED

Sound overall. One step is left implicit.

1Implicit 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.

ORIGINAL

PROPOSEDby (1)

Accept Edit Reject Compare

2A shorter route: telescopingRemark 2 · pending

Selection · (2)–(3)

+ Context

Ask a follow-up, or challenge a step…

ExploreFind gapsChallengeFormalize

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)

Explore conjectures

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

Explore

(ii)

Develop proofs

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

TeX

(iii)

Question assumptions

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

Challenge

(iv)

Refine reasoning

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

Find gaps

(v)

Collaborate in place

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

Ask⌘L

§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

§3Integration

Works with ChatGPT.

Connect your ChatGPT account and the collaborator runs on it, inside your workspace. Theoremis is a dedicated mathematical environment, not ChatGPT itself: ChatGPT provides the model, and Theoremis provides the document, the structure and the review around it.

Connect

Link your ChatGPT account once, in Settings.

Choose the context

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

Review what returns

Findings arrive as marked suggestions in your document, never as silent edits.

ON YOUR MACHINE Your document Sums of odd integers

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

CONNECTED

ChatGPT Your account · GPT-6.1 Sol

SENT

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

RETURNED

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

1NOT VERIFIED

§4Providers

One workspace. Your choice of model.

ChatGPT is available today. Poe and OpenRouter are in development, so you will be able to choose the model behind your collaborator.

AVAILABLE NOW

ChatGPT Connect your account and start reviewing proofs today. MODELGPT-6.1 Sol How it connects →

COMING SOON

Poe Use the models available through your Poe account. Notify me →

COMING SOON

OpenRouter Route the collaborator through the provider and model you choose. Notify me →

Dashed, as in Theoremis itself: proposed, not yet established.

§5Principles

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. Connect the account you already use, starting with ChatGPT.

Axiom 5 (Agency). The collaborator proposes; the mathematician decides. Nothing enters a proof without consent.

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↗

A better environment for mathematical thought.

Free and open source. Works with ChatGPT today.

Download Theoremis View on GitHub↗

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