3
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Jan 9 at 11:29
  • $\begingroup$ This has also been cross posted on leanprover.zulipchat.com/#narrow/stream/113488-general/topic/… $\endgroup$
    – Jason Rute
    Jan 9 at 12:15

1 Answer 1

2
$\begingroup$

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.

For multivariate equations, of course it is undecidable in general, and we don't even have an algorithm for curves as far as I know. The example you give first is an elliptic curve. Generally you need quite a bit of theory to implement any algorithm that would provably find all integral points on an elliptic (or more complicated) curve. Some specific types of curve are simpler, which include the one you mention, which we did actually write Lean code to find all integral solutions to, but it was quite case by case, rather than a tactic that does the whole problem for you we had to write a whole paper about it https://dl.acm.org/doi/10.1145/3573105.3575682! The hard part is of course showing that you have all solutions, in this case we used Mordell-style descent in the class group (though for that example there are likely simpler techniques available). It would be great to extend this work to more examples!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.