# Implementing and verifying algorithms for solving equations in Lean

In computer algebra systems, one can enter an equation and ask for integer solutions. Sometimes it is solved. But the output is not guaranteed to be correct.

In Lean, one can formalize the solutions to specific equations, for example, prove that the only integer solutions to $$y^2=x^3-1$$ is $$(x,y)=(1,0)$$.

I would like to have the best of two words, and be able to enter the equation, and get either message that it cannot be solved, or the description of all its integer solutions VERIFIED BY LEAN.

The first step is to consider easy equations, say, in one variable. Then all possible solutions are divisors of the free term (if it is not zero). We need to find all divisors and substitute.

A naive way of doing this is to try to write a computer program (say in Python) where the input is the equation and the output is the Lean code for its solution, which should compile in Lean.

The question is whether this is a correct way to proceed or is there a better way for doing such things in Lean?

After all, we are implementing algorithms for solving one-variable equations in integers. Are there other algorithms implemented in Lean? How this is usually organised? Is there any specific support in Lean for algorithms implementation?

We may also consider this task and the task of writing new tactic in Lean for solving equations. Can users write new tactics in Lean. Is this the correct way to proceed?

• In Lean, you can verify the code itself. You can prove that the function will always return the right answer. You don’t necessarily need tactics or metaprogramming for this. However, for your particular use case, there are a number of practical complexities including Hilbert’s 10th problem and the fact that there can be infinitely many solutions. This would make any practical solution complicated. Jan 9 at 11:29
• This has also been cross posted on leanprover.zulipchat.com/#narrow/stream/113488-general/topic/… Jan 9 at 12:15

For single variable equations its very doable indeed, but you should decide what sort of interaction you want, verified code or a tactic. Both should be possible with Lean + mathlib as it is today. I would probably be inclined to write a Lean tactic to solve such equations if I were you, this is likely the shortest path to what you want. https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Polynomial/RationalRoot.html#num_dvd_of_is_root or something similar is the result you are referring to about dividing the constant term. This coupled with a tactic to compute the divisors of a non-zero number and the fin_cases tactic (or just cases repeatedly) to break into cases for each divisor and norm_num to evaluate the resulting polynomials at integers would already be quite close to a tactic for solving all single variable equations in integers, you might not need much metaprogramming at all to write it really.