Math Question Solver (work in progress)
#std -- import std
-- theorem
!unfold := x^2 + ..0 x -> (x + ..0 / 2)^2 - (..0 / 2)^2
-- variables
$old := x^1 + 4 x + y^2 + 6 y = 0
$new := (x + 2)^2 + (y + 3)^2 = 13
-- question to solve (?0)
?:= old <=> new(output from mqs with --markdown option)
question to solve: ?0
theory:
meaning:
approach:
1: substitute $old
$\text{old} \longrightarrow x^2 + 4 x + y^2 + 6 y = 0$
2: substitute $new
$\text{new} \longrightarrow (x + 2)^2 + (y + 3)^2 = 10$
3: rewrite using !unfold
$x^2 + 4 x \longrightarrow (x + \frac{4}{2})^2 - (\frac{4}{2})^2$
4: rewrite using !unfold
$y^2 + 6 y \longrightarrow (y + \frac{6}{2})^2 - (\frac{6}{2})^2$
5: simplify (2x)
$\frac{4}{2} \longrightarrow 2$
6: simplify
$2^2 \longrightarrow 4$
7: simplify (2x)
$\frac{6}{2} \longrightarrow 3$
8: simplify
$3^2 \longrightarrow 9$
9: rewrite using std::!move_sub
$\space..\space - 9 = \space..\space \longrightarrow \space..\space = \space..\space + 9$
10: simplify
$0 + 9 \longrightarrow 9$
11: rewrite using std::!swap_add
$(\space..\space - 4) + \space..\space \longrightarrow \space..\space + (\space..\space - 4)$
12: rewrite using std::!move_sub
$\space..\space - 4 = \space..\space \longrightarrow \space..\space = \space..\space + 4$
13: simplify
$9 + 4 \longrightarrow 13$
both sides are equal! (using std::!sides_equal)
answer: correct (true)
steps tried: 10023
(output from mqs with --markdown and --at 0:9 options)
question to solve: ?0
theory:
meaning:
step 9:
state before step:
$(x + 2)^2 - 4 + (y + 3)^2 - 9 = 0 \implies (x + 2)^2 + (y + 3)^2 = 13$
step: rewrite using std::!move_sub
$\space..\space - 9 = \space..\space \longrightarrow \space..\space = \space..\space + 9$
state after step:
$(x + 2)^2 - 4 + (y + 3)^2 = 0 + 9 \implies (x + 2)^2 + (y + 3)^2 = 13$