Implementing algorithm (say, for solving equations) in Lean

Stream: general

[Bogdan Grechuk]

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 is too difficult to 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 an algorithm 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 as 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?

[Martin Dvořák]

@Tomas Skrivan

[Kevin Buzzard]

Matiyesevich et al show that the best of all possible worlds ("type in an equation, get the solutions") is not possible. You might want to check out the polyrith tactic which is related:

import Mathlib

example (x y : ℚ) (h1 : 2 * x + 3 * y = 5) (h2 : 4 * x + 7 * y = 11) : x = 1 := by
  polyrith -- succeeds

It calls out to a sage-math process which gives an informal argument which lean then proves is correct. Note that this works best over fields though (not $\Z$).

[Johan Commelin]

The group in Amsterdam has also been working on formally verified solutions to Diophantine equations, including some tactic support. I guess @Alex J. Best or @Anne Baanen can tell a bit more about it.

[Jason Rute]

This is also on PASE: https://proofassistants.stackexchange.com/questions/2665/implementing-and-verifying-algorithms-for-solving-equations-in-lean

[Alex J. Best]

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 as it is today.
docs#num_dvd_of_is_root or something similar is the result you are referring to I think.
This coupled with a tactic to compute the divisors of a non-zero number and fin_cases (or just cases?) to break into cases for each divisor and norm_num to evaluate 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 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 availiable).

[Alex J. Best]

I guess I'll post this on SE too?

[Anne Baanen]

At the moment we're focussing in Amsterdam on building more foundations for future equation solving. But I did talk last month with Joey van Langen who designed a computer algebra-based solver for Diophantine equations, how to adapt this to the interactive theorem proving setting.