Vampire -> Lean

Stream: Equational

[Michael Bucko]

Since Vampire proof generation is going so well, I learnt a bit how we are converting those proofs (I guess similar learnings would apply to a next-generation Vampire, or a next-generation Lean).

Here's the pdf (might be incorrect - I used O1 to generate it). Still, it helped me understand the basics.

Vampire - Lean.pdf

[Daniel Weber]

Nice! Some comments:

• In doSubsumptionSingle, t1 is a single literal, and t2 is a clause.
• In doSubsumptionWith both t1 and t2 are clauses, and it cases on t1 and applies doSubsumptionSingle to every literal with t2.
• doResolutionSingle and doResolution actually do subsumption resolution, not just resolution, as does the resolve term elaborator.
• Most of the code has backtracking, as metavariables can be assigned in multiple ways.
• The subsumption tactic is misleadingly named, it just tries to show the goal by applying arg1 _ (..) _ (arg2 ..) (and closing leftover metavariables by assumption)

You might also want to take a look at https://github.com/teorth/equational_theories/blob/main/equational_theories/Generated/Greedy/OrLemmas.lean, which contains Or.assocn lemmas which are used to apply superposition where the equation is a clause. For example, given eq213 : c = sk2 ∨ c = sk1 ∨ b = sk1, eq116 : (old a sk1 sk2) ∨ c = sk1 ∨ b = sk1, we use Or.assoc3 (eq213.imp_left (fun h : c = sk2 ↦ superpose h eq116)) : (old a sk1 c) ∨ c = sk1 ∨ b = sk1 ∨ c = sk1 ∨ b = sk1.

It also has trans_resol : a ≠ b ∨ b ≠ c ∨ a = c, which using resolution gives equality factoring.

Another kind of logical step Vampire takes is demodulation, which is converted to Lean as Eq.mp (by simp only [eq1, or_comm, or_left_comm, or_assoc, eq_comm, ne_comm]) eq2

[Daniel Weber]

(deleted)

[Michael Bucko]

Wow, that's very insightful. Thank you!

[Shreyas Srinivas]

Btw, is there a plan to spin off the ATP tactics into a separate lean package?

[Michael Bucko]

Shreyas Srinivas schrieb:

Btw, is there a plan to spin off the ATP tactics into a separate lean package?

I don't know about Lean's strategy when it comes to this (others can answer this better than me) -- from my perspective, it'd make a lot of sense.

My approach to this: let's build an agent with tools, incl. diffusion stuff that could come up with new tactics. And then make it open source.

The easiness of use, its flexibility and the variety of tools would turn that agent into a helpful assistant (and eventually a tool that creates new math on its own).

Check this out: https://buildermath.substack.com/p/on-implication-flow

[Shreyas Srinivas]

I don't fully understand this agent thing. What I mean is can we create a GitHub repository which consists of ATP specific directories that contain tactics to use them, along with scripts to install whichever ATP gets used.

[Michael Bucko]

Shreyas Srinivas schrieb:

I don't fully understand this agent thing. What I mean is can we create a GitHub repository which consists of ATP specific directories that contain tactics to use them, along with scripts to install whichever ATP gets used.

Sure, I understand. I think this would make sense for Lean, but others can answer this better than me.

As for the agentic approach, maybe I'll just build something small and share here. An agent would be this kind of autonomous system that leverages deep learning architectures / LLMs to understand, reason, and generate human-like responses or actions based on input data. It'd use tools like Vampire and so on.

Started building something here back in the day: https://github.com/riccitensor/mathplatform I think I could make it work in a couple of hours / days. That's also why I was looking into Vampire -> Lean and Lean -> Vampire, as well as minizinc.

[Daniel Weber]

Shreyas Srinivas said:

Btw, is there a plan to spin off the ATP tactics into a separate lean package?

I think the clausificatuon should be a lot more robust before this can be done, I had to do really specific stuff for this project

[Shreyas Srinivas]

One question, I see a lot of subproblems in this report that are already solved by lean tactics in Mathlib. Have you chosen to avoid these for specific reasons?

[Shreyas Srinivas]

(deleted)

[Daniel Weber]

I don't understand what you mean, could you give an example?

[Shreyas Srinivas]

For example, lean provides a congr tactic

[Shreyas Srinivas]

Eq.symm already exists in lean and is also provided with the symm tactic

[Shreyas Srinivas]

Is superpose not a repeated application of the trans followed by closing all goals withassumption or exact??

[Daniel Weber]

I didn't know the symm tactic, I guess it can be used in place of mod_symm. congrWith is mostly copied from Lean's congr, but it needs to be able to use the given equality with backtracking

[Shreyas Srinivas]

Btw, is there a link to the source code?

[Shreyas Srinivas]

I am currently relying on the doc posted above

[Daniel Weber]

Shreyas Srinivas said:

Is superpose not a repeated application of the trans?

I don't think so. It's approximately (congrArg motive (eq1 arg11 arg12 ..)).mpr (eq2 arg21 arg22 ..), with correctly chosen motive, args, and sometimes applying symm to eq1, eq2

[Daniel Weber]

Shreyas Srinivas said:

Btw, is there a link to the source code?

https://github.com/teorth/equational_theories/blob/main/equational_theories/Superposition.lean

[Alex Meiburg]

Could you give some explanation as to why it's called "superpose"? Is that a term used elsewhere in literature, or in some of the paper?

[Michael Bucko]

Alex Meiburg schrieb:

Could you give some explanation as to why it's called "superpose"? Is that a term used elsewhere in literature, or in some of the paper?

Isn't that a superposition of two equations?

[Cody Roux]

https://en.wikipedia.org/wiki/Superposition_calculus

[Alex Meiburg]

Thanks! I was thinking of a different use in math, https://en.wikipedia.org/wiki/Clone_(algebra) , wondering if it was somehow related