The proof workspace
Build an argument line by line and have the parts that can be checked, checked. Where the system cannot decide, it says so and stops — it does not guess, and it never marks a proof wrong for being one it could not follow.
The base angles of an isosceles triangle are equal
Assembly modegrade 8directOrders and selects statements and reasons from a pool. Nothing is typed. Validate fully. Every move is from a known set, so every arrangement has a decidable verdict.
Given
g1. Triangle ABC has AB = AC.
g2. M is the midpoint of BC.
To prove
Angle ABC equals angle ACB.
This frame cannot be edited from inside the argument. There is no control here that changes it, which is the point — a target that drifts is a target every proof reaches.
Where this usually goes wrong: Using the converse — 'two equal angles, so two equal sides' — to prove the thing itself. Both statements are true, which is what makes the loop invisible.
The argument
Nothing yet. In assembly mode: orders and selects statements and reasons from a pool. Nothing is typed.
The moves available
Not all of these belong. Three of them are moves a learner actually makes on this proof, and each is wrong in a different, nameable way.
What the system can say
incompleteThe argument does not yet reach "Angle ABC equals angle ACB.". Nothing found so far is wrong.
Checks that ran
structural completeness
reference resolution and level scoping
circularity
A clean report means these came back clean. It does not mean nothing else is wrong, and the gallery below says which classes are checked and which are not.
Hints
Structural before mathematical, and the rung you reach is itself the signal. Nothing below rung four gives away a move.
Scratch
Not marked, and kept anyway. Exploratory work is part of proving, and hiding it is how learners come to believe that proofs arrive in the order they are written down.