What should Sage look like in Lean?

Stream: general

[Gareth Ma]

I have been looking into possibilities to incorporate Sage into Lean (since I do a bit of Sage), something like polyrith, and I have a few questions.

1. To me, polyrith feels more like a proof-of-concept rather than what usage of Sage should look like in Lean/Mathlib - is that correct?
2. Related to (1.), in the long term, will adding the option to use Sage locally (when it's installed) be useful for people here, or is calling sagecell.sagemath.org fine?
3. I'm also wondering what could be done in Sage and what should be done in Mathlib. For example, would a tactic to prove a graph is acyclic via Sage, by returning a cycle for example, then reconstructing the proof in Lean be interesting, or should that be implemented in Lean? Or is there no preference as long as it generates a valid proof?

[Patrick Massot]

Gareth Ma said:

1. To me, polyrith feels more like a proof-of-concept rather than what usage of Sage should look like in Lean/Mathlib - is that correct?

I failed to assign any meaning to this sentence. Could you elaborate? polyrith is a very successful use of Sage in Lean.

[Jireh Loreaux]

I think ideally you want problems for which you can generate certificates. And then a tactic in Lean which can turn the certificates into a proof. This is essentially what polyrith does. It gets the linear combination from Sage and passes it to the linear_combination tactic.

[Gareth Ma]

Patrick Massot said:

Gareth Ma said:

1. To me, polyrith feels more like a proof-of-concept rather than what usage of Sage should look like in Lean/Mathlib - is that correct?

I failed to assign any meaning to this sentence. Could you elaborate? polyrith is a very successful use of Sage in Lean.

Sorry, I guess it should be linked with (2.). It currently calls the online service (from what I know), which is why I thought it seems PoC-like. Or is that an okay approach for future tactics?

[Gareth Ma]

(Sorry if my initial message is unclear, it's a meta-question and I don't know how to phrase it well)

[Gareth Ma]

Jireh Loreaux said:

I think ideally you want problems for which you can generate certificates. And then a tactic in Lean which can turn the certificates into a proof. This is essentially what polyrith does. It gets the linear combination from Sage and passes it to the linear_combination tactic.

Yes, that's exactly what I mean. I'm looking into linear programming certificates too, and there there should be a lot more possibilities.

[Jireh Loreaux]

I think for now it's an okay approach for future tactics, as long as they are self-replacing like polyrith. We certainly wouldn't want a tactic that's trying to call Sage from CI.

[Gareth Ma]

Do you (plural) have any opinions on (3.)

[Patrick Massot]

Calling Sage over network is clearly a deliberate choice here. Being able to use the tactic without installing Sage is a huge benefit. So calling a local Sage would be PoC-like.

[Patrick Massot]

Of course this workflow makes sense only for self-replacing tactics, but we don’t want to call Sage every time Lean checks the proof anyway.

[Gareth Ma]

Hmm I was thinking the opposite. The online Sage doesn't have the optional packages installed, and also doesn't allow for e.g. clustering / parallelisation

[Patrick Massot]

Allowing the option to run a local custom Sage would be nice, but this is not at all the common case.

[Gareth Ma]

That's an interesting perspective, and good that I asked here I guess :D I will rethink about it

[Jireh Loreaux]

Personally, I would prefer to call Sage locally if it were possible, but I realize most people aren't like me.

[Gareth Ma]

Thanks for the input :D I'm in the minority too I guess

[Patrick Massot]

Before using Lean 4 + Mathlib, I used to think Sage was a really gigantic software that one do not install without thinking about it twice.

[Miguel Marco]

About running a local install for polyrith, I think it would make much more sense to use Singular instead of Sage (or rather, to have both options). Singular is a much smaller piece of software than Sage, and the installation is often simpler too.

And in the case of the computations run for polyrith, Sage uses Singular under the hood anyways.

And yes, I think having the possibility of use the Lean tactics without relying on internet connection and external online services (that could disappear at any given moment) is kind of important.

[Gareth Ma]

(deleted)

[Miguel Marco]

To be clear: what I am (kind of) proposing is to give polyrith the option of using a local installation of Singular.

And in fact, any CAS that can do Gröbner basis could work too. It shouldn't be hard to check if any of the usual suspects is installed and try to use it.

[Gareth Ma]

Yes, and I think that should be easy to fix. The polyrith just calls

let out ← IO.Process.output { cmd := "python3", args := #[path.toString] ++ args }

(where path is to a file that make a request to sagecell.sagemath.org), so we can just replace it with a singular call or whatever.

[Kim Morrison]

One might also want to use Sage (or any CAS) + Lean by writing a wrapper for a low level function available in Sage, axiomatizing its behaviour, and then writing a verified higher level algorithm in Lean.

This isn't something you would do in Mathlib, as we don't want new axioms there, but nevertheless is interesting.

[Kim Morrison]

@Rob Lewis and I wrote a short demo of this at https://github.com/aim-cyber-workshop-2023/lean-sage/blob/main/LeanSage/Demo.lean

[Gareth Ma]

Oh my god this is so cool and exactly what I'm looking for. I'll have a closer look when I wake up, thanks!!

[Kim Morrison]

(Here we axiomatize the behaviour of sage's integer factorization algorithm, and then use this to implement a verified "is x a primitive root of unity mod k" algorithm.)

[Gareth Ma]

Is creating a new axiom just a nicer way to write a theorem but sorry'ing it?

[Kim Morrison]

Patrick Massot said:

Sage was a really gigantic software that one do not install without thinking about it twice.

(I just needed to install sage locally to test the above demo still worked: brew install sage, waiting about 3 minutes, and typing a password seems to have been all that was necessary.)

[Kim Morrison]

(Note that this demo is still ridiculously slow because we never merged #8885.)

[Matthew Ballard]

(Note #8885 is delegated at minimum it just needs to brought in line with master. Moving some of the stuff to a separate file would be a nice follow up)

[Patrick Massot]

Scott Morrison said:

Patrick Massot said:

Sage was a really gigantic software that one do not install without thinking about it twice.

(I just needed to install sage locally to test the above demo still worked: brew install sage, waiting about 3 minutes, and typing a password seems to have been all that was necessary.)

In my memory Sage needed more than 1Gb to download and store. Did this change recently?

[Gareth Ma]

The source is 1.2G the source + build artifacts is 1.2G, idk binary

[Gareth Ma]

But installation time is quick yeah, even building from source only takes ~15 minutes on my i5 laptop

[Mario Carneiro]

@Gareth Ma said:

Is creating a new axiom just a nicer way to write a theorem but sorry'ing it?

The two are similar, but have slightly different meanings and effects on lean. A proof by sorry is saying "I think this is provable, but I would rather not prove it now", and lean will remind you that the proof is incomplete with a warning. An axiom is saying "I assert this is true, even though lean cannot prove it" and lean will not give any warning (but you can find use of such axioms later using the #print axioms command, which will also reveal uses of the sorryAx axiom which the sorry term elaborates to after giving the warning). A finished development should not have sorrys but it may have axioms in it.

[Gareth Ma]

That makes sense, thanks. I guess sorry is implemented as (a tactic that just uses) an axiom (the sorryAx) then?

[Mario Carneiro]

In a case like this, you would want to use an axiom rather than sorry, because the theorem is genuinely not provable: calling some FFI function from Sage is an opaque function with no provable properties

[Mario Carneiro]

yes, it's effectively <give warning>; exact sorryAx _ false

[Miguel Marco]

So, the approach of axiomatizing the Sage behaviour means "we will accept as an axiom that whatever the Sage call returns is correct"?

Doesn't that kind of defeat the purpose of formally verifying proofs?

[Gareth Ma]

I guess that's why it's a "demo"

[Miguel Marco]

Along these lines, one of the proposals of Sage for this year's GSOC involves some form of integration with proof assistants:

https://wiki.sagemath.org/GSoC/2024

I think the idea is to give a convenient interface, and also, when possible, modify some functions to return not only the final result, but also a witness of correctness that can be efficiently checked by proof assistants (in the spirit of what polyrith does).

I think it is a nice idea, but out of my head I don't get many examples of computations that allow this kind of witnesses (of course, it deppends on where you set the bar for "easily verified").

[Gareth Ma]

Yes, I’m applying for that :)

[Miguel Marco]

I see.

Here are some thoughts about possible problems that could fit in this idea:

• Factorization problems: Sage can compute the factors, and Lean can easily check that the product of the factors gives indeed the original value. Verifying that the factors are irreducible is another story.
• matrix factorizations (LU, Cholesky, Smith ....): Sage can compute them (the complete factorization), and Lean can verify - that the results are indeed factorizations of the original matrix, and that they satisfy the corresponding property (being triangular/diagonal/orthogonal or whatever).
• Finding solutions of (systems of) equations: Sage can find solutions and Lean verify them. Again, checking that no other solutions exists is another story.
• Same as before, for differential equations.
• Symbolic integrals: Sage can compute them and then Lean can verify that the derivative of the result is indeed the original expression. This one is much more tricky that it looks, because of the multiple expressions that the same function can have
  (and also, I am not sure how good Lean is at computing symbolic derivatives). There is also the problem of the domains where the functions are defined.

Anyways, it sounds like both Sage and Lean could benefit from this: Lean could have more polyrith-like taactics, and Sage could say "here is the result, and Lean checked that it is correct" for some computations (maybe even providing Lean code that can be independently checked).

[Kevin Buzzard]

@William Stein just a heads-up that this discussion is happening

[Eric Wieser]

Scott Morrison said:

One might also want to use Sage (or any CAS) + Lean by writing a wrapper for a low level function available in Sage, axiomatizing its behaviour, and then writing a verified higher level algorithm in Lean.

This isn't something you would do in Mathlib, as we don't want new axioms there, but nevertheless is interesting.

Can't you avoid the axiom here by using opaque, and just proving that a function could exist that performs the low-level function?

[Eric Wieser]

So

@[implemented_by sagePrimeFactorsUnsafe]
opaque sagePrimeFactorsAux (n : ℕ) : {l : List ℕ // p ∈ l ↔ p ∈ Nat.primeFactors n}

[Eric Wieser]

(and use lcProof in the unsafe version to populate the subtype)

[Kim Morrison]

Miguel Marco said:

So, the approach of axiomatizing the Sage behaviour means "we will accept as an axiom that whatever the Sage call returns is correct"?

Doesn't that kind of defeat the purpose of formally verifying proofs?

Not at all. There are always lower levels of a system that you are trusting (i.e. for most Lean users, the Lean kernel. Other Lean users use reduceBool and trust the compiler too, etc.).

I think it's an interesting opportunity, that I hope we pursue, whereby someone who otherwise would have developed a high level algorithm in Sage might instead develop it in Lean.

They can still call a low level function in Sage that is not available in Lean, and axiomatize its behaviour. This is reasonable, because the low-level function has been used for a long time by a large Sage user base. The newly developed work is ensured to be correct by Lean.

[Kim Morrison]

Eric Wieser said:

So

@[implemented_by sagePrimeFactorsUnsafe]
opaque sagePrimeFactorsAux (n : ℕ) : {l : List ℕ // p ∈ l ↔ p ∈ Nat.primeFactors n}

PRs welcome! :-)

[Miguel Marco]

(deleted)

[Ralf Stephan]

Add checking of Wilf-Zeilberger certificates for symbolic summation to the list (regardless of where the certificate comes from).

[Siddhartha Gadgil]

Would it be a good option to have a typeclass TrustSAGE (or many more specific ones) which have the axioms in them? Then there can still be high level algorithms in Lean but the signature makes it clear what is trusted.

[Gareth Ma]

Just to update on this, my GSoC proposal was unfortunately rejected, and I don't see myself working on this if I were to choose between this and, you know, normal mathematics formalisation :D Hope the discussion is useful to any future attempts!

[Luigi Massacci]

I have a foggy notion that the lean infoview can display arbitrary HTML (correct me if I’m wrong), so I was wondering if anyone has given any thought to plotting stuff on it via Sage? By this I mean making some kind of light wrapper for the Sage plotting libraries and then displaying the result in the infoview. Maybe @Tomas Skrivan? Presumably plotting is part of making lean a language for scientific programming

[Mario Carneiro]

yes, I'm sure I've seen examples of this (IIRC ProofWidgets even has an animating plot)

[Anand Rao Tadipatri]

At one point, I had created a light wrapper around the Plotly library to render plots in the infoview. The source code is available here (I can't seem to find the corresponding Zulip post): https://github.com/leanprover-community/ProofWidgets4/pull/15/files.
The ProofWidgets repository also has some examples using the Recharts package.