Lean Oscar Interface

Stream: general

[Cedric Holle]

I am working on interfacing Lean and Oscar. You can find code at my repo. I would love to get some comments and feedback.

Currently working:

proving that a permutation is in the closure of some permutation

def d  : Equiv.Perm (Fin 5) := c[1, 2, 3, 4]
def b0 : Equiv.Perm (Fin 5) := c[2, 1, 3]
def b1 : Equiv.Perm (Fin 5) := c[1, 3, 4]
def b2 : Equiv.Perm (Fin 5) := c[3, 2, 4]
def b3 : Equiv.Perm (Fin 5) := c[3, 1, 4]
def b4 : Equiv.Perm (Fin 5) := c[1, 2]

theorem test2 : d ∈ Group.closure {b0, b1, b2, b3, b4} := by
  perm_group_membership

proving some equalities in presented groups/proving that a presented group is trivial

@[reducible]
def f := FreeGroup (Fin 2)

@[reducible]
def a : f := FreeGroup.mk [(0, true)]
@[reducible]
def b : f := FreeGroup.mk [(1, true)]

@[reducible]
def rels_list := [a⁻¹ * b⁻¹ * a * b * a⁻¹, b⁻¹ * a⁻¹ * b * a * b⁻¹]
@[reducible]
def rels := List.toSet rels_list

@[reducible]
def g := PresentedGroup rels

set_option maxRecDepth 10000000000000000000000
set_option maxHeartbeats 1000000000000000000000

theorem g_triv : ∀ (x : g), x = 1 := by
  kbmag (1 : g)

theorem a_eq_b : (PresentedGroup.of 0 : g) = (PresentedGroup.of 1 : g) := by
  kbmag (1 : g)

and some more small stuff.

The later is not well tested. I am happy that it works.
It's my master's thesis. Text will follow within a month.
@Laurent Bartholdi

[Henrik Böving]

How does this work in proofs? Are you getting a proof certificate from Oscar and converting that into a proper Lean proof? Are there additional axioms involved that assume the correctness of (parts of) Oscar?

[Cedric Holle]

Henrik Böving said:

How does this work in proofs? Are you getting a proof certificate from Oscar and converting that into a proper Lean proof? Are there additional axioms involved that assume the correctness of (parts of) Oscar?

I am getting a proof certificate in Oscar and using it to build a proof in Lean. No additional axioms.

[Henrik Böving]

That's awesome! Is this limited to a certain fragment of what Oscar can do or is your proof recovery procedure complete with respect to everything that Oscar might output?

[Cedric Holle]

It's using Oscar's serialization to send data forth and back. So we are limited to data types for which it is implemented in Oscar and for which I have implemented the same in Lean.

[Miguel Marco]

Very nice!

How does the communication Lean<-> Oscar work?

[Kim Morrison]

(It took me a moment to find the Oscar homepage: https://www.oscar-system.org/)

[Patrick Massot]

Thanks Kim, I did not have the patience to search for it.

[Patrick Massot]

The presentation of the project goal sounds awfully similar to Sage. Why did they start something else?

[Mario Carneiro]

probably because julia is obviously the right language to be writing a CAS in

[Utensil Song]

It's really nice to see Lean interfacing a Julia CAS!

My understanding is that Julia aims to be a modern Fortran (which still is the language for fast math routines that C calls) that CAS made by it could replace the slow Python based symbolic calculation ecosystem with much better type and abstraction support.

As a maintainer of a SymPy based symbolic package, Julia was my dream language before Rust and Lean, unfortunately Rust has less support for rich operators and symbolic calculation except for egg, and Lean has its emphasis on theorem proving and it's still at a prototype stage interfacing with existing CAS systems.

Julia based Oscar has one more potential advantage, to be interfaced via FFI and have performance gain, over other IO based CAS interfacing. Maybe it could be a better choice over C++ library GiNaC, thanks to its matched performance and previous work on proof generation.

[Cedric Holle]

Miguel Marco said:

Very nice!

How does the communication Lean<-> Oscar work?

Start a julia file as a child with a lean command/tactic. The julia file is then a simple while true loop waiting for a command. I use Std.Tactic.Cache for the definition of the child to make it possible to access the child multiple times in a file.
The Code can be found in Mrdi/Server.lean and Mrdi/server.jl.
Does this answer your question? It is so general that I'm not sure what exactly to elaborate on.

[Andrés Goens]

this is really cool! I'm confused that Oscar gives you proof certificates! I thought especially for group theory like in your examples, Oscar itself would be just calling GAP under the hood? does oscar build the proofs on its own on top of the gap computation, or how does that work?

[Andrés Goens]

CC @Siddharth Bhat

[Utensil Song]

Judging from the code, Lean-Oscar mainly uses Oscar (so far, mostly GAP behind it) to construct complex objects then convert them to Lean for definitions, as for theorems, Oscar seems to be helpful to generate intermediate goals, and the proof recontruction is still done in Lean, with tactics and some heuristics around the intermediate goals.

[Laurent Bartholdi]

Chiming in: e.g. Julia contains Oscar which delegates to GAP which
delegates to KBMAG (Knuth-Bendix) which quickly and cleverly produces new
rules in a rewriting system. Asking it to print a trace of the new rules
that it produced, and how it obtained them ("exploit the overlap of rule #i
with rule #j") makes it possible to replicate the operation in Lean. There
would still be work to do to have, e.g., KBMAG only print the new rules
that were actually used. In principle there could be an arbitrarily large
number of going-nowhere explorations done by KBMAG, but a very small number
of useful ones which are the only one needed in a certificate to be checked
by Lean.

[Cedric Holle]

If I would have managed to let KBMAG also print which rules were used, the reconstruction in Lean would be much more simple and less compute heavy. But this isn't gonna happen in time.

[Cedric Holle]

We were looking for more complex examples beyond just finding a witness. Additionally, I had a lot more fun with the challenging problems. If you want to see a simpler example, take a look at

matrix_inverse

def A : Matrix (Fin 3) (Fin 3) ℚ := !![3, 0, 4; 5, 10, 6; 1, 2, 3]

def A_inv : Matrix (Fin 3) (Fin 3) ℚ := by matrix_inverse A

theorem test3 : A * A_inv = 1 := by
  simp[A, A_inv]
  ext i j
  fin_cases i
  all_goals fin_cases j
  any_goals norm_num [_root_.mkRat, Rat.normalize]
  any_goals rfl

[Miguel Marco]

Cedric Holle said:

Does this answer your question? It is so general that I'm not sure what exactly to elaborate on.

Mostly yes. So it sounds like a trick that could be easily generalized to other CAS systems, right?

I am thinking mostly on having a version of polyrith that relies on a local install of a CAS instead of an online service.

[Cedric Holle]

Miguel Marco said:

Cedric Holle said:

Does this answer your question? It is so general that I'm not sure what exactly to elaborate on.

Mostly yes. So it sounds like a trick that could be easily generalized to other CAS systems, right?

I am thinking mostly on having a version of polyrith that relies on a local install of a CAS instead of an online service.

Should work.
I like the way it is handled in polyrith. It skips all the setup problems for the user.

[Utensil Song]

Miguel Marco said:

I am thinking mostly on having a version of polyrith that relies on a local install of a CAS instead of an online service.

Yes, IMHO, a mature practice of interfacing CAS should probably be able to (modulos the cache invalidation stuff):

1. use a cached result if available
2. use bundled FFI if available
3. use the local CAS if available
4. if steps above fail, and the online option is off or not set, fail the tactic with hint for users to opt-in to rely on an online service, or a guide to set up a local CAS
5. if the online option is on, use the online service, and cache the result.

Relying on a Python installation and a package requests that might not be installed properly and an online service that might not be accessible or stable silently is not really how it should be in the long run.

But this is a little off-topic, and was discussed here, and people clearly have different preferences on this.