First, I've got proof no. 3. I can offer a nice 4 argument proof, but you wouldn't let me provide it.
Second, I tried proof no. 2, where I'm offered words like given and algebra I have no use for.
To make a system like this right it needs to be deductive and have a large library of concepts. Getting this right is complex enough to be a PhD project. Properly scoped could be done for MSc.
For proof 2, "Given" is the reason for "ABCD is a kite" and "Algebra" is the reason for "BD = BD". I found that relatively obvious after I understood the purpose of the "statement" and "reason" columns.
If you treat it as a kind of puzzle where you have to arrange the given blocks to form a valid proof, it's not so bad. However, you should at least be able to reorder independent statements, and reasons should include references to the previous statements they depend on, e.g. in proof 4, "<A = <D" follows by "Substitution" only because the previous statement is "<EBC = <A and <ECB = <D". In longer proofs you may have to refer to something proved further up, and requiring the student to give the reference would be a further check of their understanding.
If you haven't done a two-column high school geometry proof in a while, this might seem a little strange. I'm a geometry teacher and created this mostly for my students to practice stringing together math statements in a logical order.
"Given" is a "reason", pretty commonly seen in mathematical solutions. "Given" indicates that the statement was indicated in the specification of the problem.
For now, there is one correct solution. So it's dependent on the teacher to pin any statements/reasons to ensure there's only one possible answer. I have some ideas for making it more flexible in the future, but haven't quite solved the user interface problem for assigning parent and child steps.
First, I've got proof no. 3. I can offer a nice 4 argument proof, but you wouldn't let me provide it. Second, I tried proof no. 2, where I'm offered words like given and algebra I have no use for.
To make a system like this right it needs to be deductive and have a large library of concepts. Getting this right is complex enough to be a PhD project. Properly scoped could be done for MSc.