Kurt is a small language for mathematical proofs: one claim per line, and Kurt checks
each one and says why it follows. Everything runs here in your browser; nothing is uploaded.
Getting started
Open the tutorial menu and start with 00-check-a-proof-file.kurt: each lesson
answers one question, from "How do I prove an implication?" to "Why did this step fail?", with a proof you
can change and check again. The keywords menu has a short lesson on each keyword and idea of
Kurt, starting with 00-true.kurt. The mafi1 menu has the proofs of the
lecture "Mathematik für Informatik 1" (linear algebra), chapter by chapter. The last lessons of the tutorial are complete
proofs, and theories shows the theories that load brings in
(load prop, load logic, …).
Checking a proof
Run (or Cmd/Ctrl+Enter) checks the proof. The output repeats each line with its reason
(hover over a line of the output, or tap it, to see the lines its step uses, in the output and in the editor):
B ; 5 by 3(4) says that line 5 follows by the rule of line 3 from the fact of line 4, and
Proof checked means every line holds. If a line doesn't follow, Kurt stops there and says why;
click the error to jump to that line. Cancel stops a check that takes too long.
Shell, above the output: after a check, a line under the output continues where the
check stopped -- at a breakpoint line (which opens it by itself), at the failing line, or after
the last line -- with the open blocks and the facts there. A line typed there (Enter) is checked at once;
Shift+Enter starts a new line, Tab completes (the next step, the value after = with
calc on, \forall, names). Copy to editor inserts the accepted
lines into the proof, where the shell started.
Writing
- Declare what you use first, e.g.
bool A, B; use states an axiom, a plain line is
a claim that must follow.
- Blocks are indented by four spaces:
assume A, then the indented lines; dedenting closes the
block and gives A implies ….
- Comments start with
;.
- Symbols: tap them in the bar above the editor, or type a LaTeX-style name followed by a space, e.g.
\forall → ∀, \exists → ∃, \implies → ⇒, \and → ∧,
\or → ∨, \not → ¬, \in → ∈.
The buttons
- File: upload a
.kurt file, download the proof as one (for the
kurt command line), or copy a link to this proof: the link contains the proof itself.
- View: the text size, and the column where the reasons start in the output (changing
it checks the proof again, so you see it right away).
- Light / Dark, at the top right: the light or the dark theme.
- The symbols below the editor insert themselves at the cursor. The bar between the editor and the
output moves (double-click: half and half).
- File, above the output: copy the output, download it, or download the proof's
certificate (
.kurtc, after a successful check): for each line, the rule, the facts and the
values that Kurt's kernel checked. Put it next to the same proof.kurt, and the command-line
kurt checks it again without searching. Clear closes the output.
With a keyboard, Cmd/Ctrl+Enter checks and Cmd/Ctrl + / − / 0 changes the text size. Your draft stays in
this browser, and the playground also works offline after the first visit.
More
Kurt is developed by Stefan Harmeling (TU Dortmund, 2016-2026).
github.com/harmeling/kurt-lang: Kurt's
repository, with the language reference, the tutorial, and the theories. There you can also
install Kurt, or download the single file kurt.py.