Score 162

$$ \begin{align} y^2 (a^2 - 1) + 1 - x^2 = 0 & \text{ } & (14) \\ v^2 (a^2 - 1) + 1 - u^2 = 0 && (14)\\ t^2 (b^2 - 1) + 1 - s^2 = 0 && (14)\\ r y^2 - v = 0 && (7)\\ py \cdot 4 - b + 1 = 0 && (7) \\ a + q u - b = 0 && (6)\\ x + cu - s = 0 && (6)\\ k + 4 y (d - 1) - t = 0 && (11) \\ k + e - 1 - y = 0 && (7) \\ (y (a - 2) + m - x)^2 + ((f - 1)(a \cdot 4 - 5))^2 (-1) = 0 && (36) \\ 4 a - m - g - 5 = 0 && (8) \\ 2 + h - w = 0 && (5)\\ k + l - w = 0 && (5) \\ z^2 (w - 1)^2 (w^2 - 1) + 1 - a^2 = 0 && (22) \end{align} $$

This solution is taken from Martin Davis's article Hilbert's Tenth Problem Is Unsolvable, using the sets of equations in theorems 3.1 and 3.5. The proof for why this works is approximately fifteen pages, so I won't be replicating it here - Matiyasevič’s theorem, which draws an equivalence between solutions to Diophantine equations and the values of sets that can be enumerated by a program, and is the reason this challenge is solvable, relies on the exponential function being Diophantine, which took multiple decades to prove.

I've replaced the base \$n\$ in the given equations with \$2\$, and reformatted the equations to be polynomials that fit the challenge's spec. The scoring system is a bit weird - in particular, there's no way to subtract two formulas directly, and the scoring around them is weird - e.g. a - b previously had to be scored as (a) - b^1, or a + b(-1), although this has now been changed. I think I've done a reasonably good job, but it's possible there's more to be saved.