# Algebra Teaching Tool
An interactive tool for manipulating algebraic expressions, which only allows you to create correct derivations.
Intended for teaching algebra.
## MVP
I want this tool to be as simple as it can possibly be, given what it needs to do.
In particular:
- It will *not* be a full proof system.
- It will only have one type: real numbers.
- Logical forms may be restricted. No arbitrary nested quantifiers! ∀∃∀∃∀∃∀∃∀∃∀∃∀∃
That said, what *does* it need to support?
- A theorem's inputs are a list of variables, along with a list of equalities and inequalities between expressions.
- A theorem's output is a disjunction of cases.
    - Each case is a conjunction of equalities and inequalities between expressions.
- Some sort of dependency: the validity of values can depend on theorems.
    - In sandbox mode, the user will choose the assumptions. How do we enforce "denominator nonzero" there?
Motivating Examples:
- Theorem: Given any numbers \\(a\\) and \\(b\\) such that \\(ab = 0\\), either \\(a = 0\\) or \\(b = 0\\).
- I want it to only be possible to write \\(\\frac{a}{b}\\) if it is already known that \\(b \\neq 0\\).
    - Similarly for \\(\\sqrt{a}\\) and \\(a \\geq 0\\).
    - This is hard, especially in hypotheses.
## Levels
I imagine a tree of levels, as if in a puzzle game.
Sorted into "Chapters"
Tree or DAG of levels in each.
Chapters may themselves be sorted into trees.
- Chapter 1: Addition and Subtraction
    - a - a = 0
    - --a = a
- ...
- Chapter ?: Quadratic Formula
    - Final level proves the formula itself.
- Bonus Chapter: Cubic Formula
- Bonus Chapter: Quartic Formula
- Sandbox Mode
# Notes
Tutorial levels: proving subtraction rules.
Then subtraction rules are available for future levels.
If allow use sandbox in tutorial, how avoid circularity?
Option: Allow long variable names. (checkbox)
Fun animation of a case going "poof" upon contradiction?
If cases disappear both upon contradiction and upon proving the conclusion,
you're done when they're all gone.

- [Algebra Teaching Tool](./algebra_teacher.md)