Metadata-Version: 2.4
Name: kurt-lang
Version: 0.7.6
Summary: Kurt: a small language for mathematical proofs close to how humans write them, checked automatically.
Author-email: Stefan Harmeling <stefan.harmeling@cs.tu-dortmund.de>
License: MIT License
        
        Copyright (c) 2016-2026 Stefan Harmeling
        
        Permission is hereby granted, free of charge, to any person obtaining a copy
        of this software and associated documentation files (the "Software"), to deal
        in the Software without restriction, including without limitation the rights
        to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
        copies of the Software, and to permit persons to whom the Software is
        furnished to do so, subject to the following conditions:
        
        The above copyright notice and this permission notice shall be included in all
        copies or substantial portions of the Software.
        
        THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
        IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
        FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
        AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
        LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
        OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
        SOFTWARE.
        
Project-URL: Homepage, https://www.kurt-lang.org
Project-URL: Repository, https://github.com/harmeling/kurt-lang
Project-URL: Documentation, https://github.com/harmeling/kurt-lang/blob/main/doc/kurt-doc.md
Project-URL: Issues, https://github.com/harmeling/kurt-lang/issues
Keywords: proof,proof checker,logic,mathematics,education,natural deduction
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Education
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Education
Classifier: Topic :: Scientific/Engineering :: Mathematics
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Provides-Extra: dev
Requires-Dist: coverage; extra == "dev"
Dynamic: license-file

# Kurt

Kurt is a small language for writing mathematical proofs in a form close to how people write
them — one claim per line, blocks for assumptions and cases — and a checker that tells you
immediately, line by line, whether each step follows. It is meant for students learning to prove
things, much like running tests while learning to program. Kurt has been developed by Stefan
Harmeling (TU Dortmund) since 2016.

**Status: 0.7, a public beta.** Kurt is used for teaching, but the language isn't frozen yet: a
proof written for 0.7 may need small changes for 1.0.

**Try it in your browser**, without installing anything:
[www.kurt-lang.org](https://www.kurt-lang.org), the playground. It runs the same Kurt in the
browser, with the tutorial, the keyword lessons, and the proofs of a lecture (mafi1).

## A first proof

A file `modus-ponens.kurt`:

    ; simple modus ponens proof
    bool A, B
    use A implies B
    use A
    B

Check it on the command line:

    $ kurt modus-ponens.kurt
    This is Kurt, v0.7.6 (made by Stefan Harmeling, 2016-2026), file c57cc53c5c5d
    use A implies B                           ; 3 without proof
    use A                                     ; 4 without proof
    B                                         ; 5 by 3(4)
    Proof checked

Each line gets the reason it holds: `B` follows by the rule of line 3 from the fact of line 4.
A proof with blocks, from the theory `prop` that comes with Kurt:

    ; if A implies B, then not B implies not A
    load prop
    bool A, B

    show (A implies B) implies (not B implies not A)
    proof
        assume A implies B
            assume not B
                assume A
                    B
                    false
                not A
    qed

`kurt` without a file starts an interactive shell, which reads the same language, with the
same indentation rules as a file.

## What Kurt offers

- **Proofs as text**, line by line. Kurt finds each single step by itself, from the facts and
  rules around. You don't need tactics or rule names.
- **Theories written in Kurt itself**: propositional and first-order logic, equality, sets,
  arithmetic, natural numbers with induction, analysis (sums, limits), and groups; and, as an
  experimental example, a fragment of modal logic.
  Even the grammar is declared there (`infix`, `bindop`, `chain`), so students can read why a
  step goes through.
- **A kernel checks every step again**: the search hands each accepted step to a small checker
  as a certificate. `cert N` shows the certificate of line `N`. The certificates of a checked
  file are kept in a `.kurtc` file, and next time the kernel checks them again, without any
  search.
- **Exact arithmetic** with `calc on`: `0.1 + 0.2 = 0.3` holds, and `1 / 3` stays a fraction.
- **For grading**: `kurt --strict` rejects axioms (`use`), `todo` and new rules outside the
  theories that come with Kurt.
- **No dependencies**: one Python file. It's also available as a single self-contained script
  with all theories embedded, to hand out in a course.

## Installing

With Python 3.10 or newer, from [PyPI](https://pypi.org/project/kurt-lang/):

    pip install kurt-lang

Then run `kurt` or `python -m kurt`. The newest state of the repository, between releases:
`pip install git+https://github.com/harmeling/kurt-lang.git`.

**Without installing**, for a course: download the single self-contained `kurt.py` of the
latest release,

    https://github.com/harmeling/kurt-lang/releases/latest/download/kurt.py

It has all the theories embedded (`load prop` and so on work right away) and needs nothing but
Python: `python3 kurt.py proof.kurt`. You can also build it from this repository yourself, with
`python3 scripts/build_standalone.py` (writes `dist/kurt.py`). To keep the theories as separate, editable files instead,
copy `src/kurt/kurt.py` together with the directory `src/kurt/theories/`.

**From Python**, e.g. for a grader or an editor:

    import kurt
    result = kurt.check_text('load prop\nbool A, B\nuse A implies B\nuse A\nB\n')
    result.ok, result.complete, result.error, result.output     # complete: also no `todo` left
    result.events      # each line: its id, kind, rule, the lines it uses (also `kurt --json FILE`)

    session = kurt.new_session(kurt.RunConfig(strict=True, paths=('teacher/',)))
    session.check_file('proof.kurt')

Each session has its own options and state (fresh names, certificates, the cache of checked
theories), so checks in one process don't influence each other -- one check at a time; for checks
in parallel, use processes.

## Documentation

- [`tutorial/`](tutorial/): the tutorial, 27 lessons (00 to 26), task by task: prove an implication, argue by
  contradiction, split into cases, rewrite with equality, use induction, diagnose "can not
  derive". Each one is a Kurt file you can run and change.
- [`keywords/`](keywords/): 47 short lessons (00 to 46), one keyword or idea each
  ([plan](keywords/plan.md)).
- [`doc/kurt-doc.md`](doc/kurt-doc.md): the language reference.
- [`doc/kurt-soundness.md`](doc/kurt-soundness.md): what the checker's correctness rests on,
  rule by rule, and the bugs found so far, each with its regression test.
- [`proofs/`](proofs/): many more example proofs. Each one is also a test.

## Why trust it?

A checker is only useful if what it accepts is correct. In Kurt, every step the search finds is
checked again by the kernel. Loaded theories are checked on their own, independent of what was
loaded before. A `def` must be conservative. Adversarial test files (`proofs/soundness/`) keep
every bug found so far from coming back. Kurt is not a small-kernel system like Metamath or HOL
Light yet: the kernel still shares the parser and the normal forms with the search.
`doc/kurt-soundness.md` says exactly what is trusted.

## AI assistance

Stefan Harmeling has designed and developed Kurt since 2016, and AI tools have helped with
parts of the work:

- **ChatGPT**, used in interactive chat to figure out bugs and details of the search procedure,
  in particular how to generate all possible matches.
- **AI coding assistants** since September 2026: Anthropic's Claude via Claude Code, and OpenAI's
  Codex. They implemented features and wrote tests, tutorial lessons and documentation. They
  also reviewed the code for soundness bugs.

The author has not checked every line of the code they produced. He has reviewed the changes,
to see that they do what they should. Every change must also pass the test suite, which checks
every proof in `proofs/` and every tutorial lesson, including the adversarial cases in
`proofs/soundness/`. Commits made with an AI coding assistant say so in a `Co-Authored-By:`
line. The design of the language, and the responsibility for it, remain the author's.

## Editor support

`kurt --lsp` is a language server for editors: the errors and `todo`s at their lines, the reason
of each checked line at its end and on hover, and completion with the state at the cursor.

The [kurt-syntax](https://github.com/harmeling/kurt-syntax) repository has editor support for
`.kurt` files: highlighting, comments and indentation, and, in VS Code and Emacs, LaTeX-style
shortcuts such as `\forall` → `∀`.

- **VS Code**: an extension with snippets, built with `npm install` and `npm run package`, then
  installed with `code --install-extension kurt-syntax-<version>.vsix`.
- **Emacs**: put `kurt-mode.el` and `replacements.json` together in a directory on your load
  path, and add `(require 'kurt-mode)` to your configuration.
- **Vim and Neovim**: use the repository as a plugin, e.g. clone it into
  `~/.vim/pack/plugins/start/kurt-syntax`, or into Neovim's plugin directory.

## Developing Kurt

    python -m venv .venv
    source .venv/bin/activate
    pip install -e .[dev]
    python -m unittest              # the test suite, including every file in proofs/
    coverage run -m unittest && coverage report

The implementation is the single file `src/kurt/kurt.py`. The theories are in
`src/kurt/theories/`.

The banner's `file <hash>` is a fingerprint of the exact `kurt.py` you're running. When you
compare unexpected behavior with someone else, it tells you whether you really run the same
code.

## License

[MIT](./LICENSE) © 2016-2026 Stefan Harmeling. When you use or cite Kurt, please link back to
this repository. A star on GitHub is also appreciated!
