Theoremis
A math-native IDE that turns handwritten proofs into verifiable formal mathematics.
Why is a proof
hard to check?
An informal argument can get an idea across while leaving its assumptions unstated. A formal proof has to spell those out.
Theoremis is an editor for going from a handwritten proof to one a computer can check. Writing and checking happen in the same place, so you are not switching tools mid-thought.
A sketch of the workflow, not a production architecture diagram.
A sum, by induction.
01 — Base case
For n = 1, both sides equal 1.
02 — Inductive hypothesis
Assume the statement holds for some integer k ≥ 1: 1 + ⋯ + k = k(k + 1)/2.
03 — The step that matters
Add k + 1 to both sides. The right side becomes k(k + 1)/2 + (k + 1) = (k + 1)(k + 2)/2. This is precisely the statement for k + 1.
A mathematical explanation; this page does not execute a formal proof checker.
Getting the feedback right is the hard part.
How should the editor point out a missing assumption? How much formality belongs on screen at once? I don’t have good answers to these yet.
Open Theoremis ↗