Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?

Question

I'm creating a "CAS for category theory / homological algebra" in C++ that "supports proofs". Although it is feature creep, I was wondering if there exists a format that my app can easily export to (assuming I have all the makings of a propositional logic system, etc.) and such that the current popular proof assistants (Lean, Coq, Isabelle, etc.) can import that possibly even converting it to a code file that can be formally checked? The system I'm making is not going to be formally checked, on the other hand it's going to be insanely fast and will be able to search (visually too as an option in version 2) for a diagram chase-like proof.

Answer 1

Your XY problem

Let me step back and think about the XY of your problem. You have a category theory solver which already generates "proofs" and you want to export those proofs to be checked by an external solver.

One big question, as Couchy mentioned, is "what do you mean by 'proofs'?" In particular, what logical system are you using in your solver? Presumably your proofs are being already stored in some internal format, or at least you should have the ability to add tracing to your application to record proof traces.

The second big question is what sort of interaction your want with an external checker? Here are some options:

1. You want two-way instant communication in the middle of your already fast application where you send the proof to an external checker and have it checked and then the external checker sends back VALID/INVALID?
2. You want Lean/Coq/Isabelle to be able to use your tool as a tactic. This would require a two-way communication with your tool where the tactic sends your tool a problem (in some format), your tool sends back a proof (in another format), and the tactic converts your proof to a valid proof in Lean/Coq/Isabelle.
3. You want to export your proof to a file as a witness that an external checker can check. It is ok if the external checker takes a long time and it is ok if the export format is unreadable.
4. You want to export your proof to a readable text Lean/Coq/Isabelle file so you can inspect the proof and use the proof with or inside Lean/Coq/Isabelle category theory libraries.

Ok, so now that we understand more about the XY problem, let's talk about possible solutions and existing work.

Checking your tool's custom logic

I would first focus less on a standard logical interchange format, and more on the logic that your tool already uses. I would take the time to:

• (if easy) export your proofs to a serialized text format
• write down a specification for your proof data structures and what it would take to check that they are correct

It is difficult without more detail to know anything about your proofs, but let me propose some options on what it would mean to "check your proofs".

Option 1: Ad-hoc external checker

One option (which I don't recommend as a final solution, but maybe as an intermediate one) is that you take your custom proof system and write a custom external checker for it. This doesn't give you that much, since how do you even know if your logical system is consistent? But if your system is simple enough, sometimes it is just enough to (1) clearly write down the syntax and rules of your logical system, (2) export your proofs to a minimal proof format representing steps in this logical system, and (3) write an external proof checker for your system which can check your exported proofs. This is what Lean does. The proofs are converted by Lean's kernel into a simple export format which encodes all the logical steps in a Lean proof using Lean's type theory. This format ignores all of Lean's fancy features (like type classes, notations, elaboration, etc.) and just checks the pure type-theoretic proof. Many users have written their own external type checkers for Lean's exported proofs. This adds a lot of support that there are no silly bugs in Lean's kernel, or at least none that effect the current proofs in Lean's mathlib library. (But to be clear, I wouldn't use Lean's export format directly. I would at best, take inspiration from the idea to make your own.) Also, if you go this route you could look at MetaMath Zero which is an experimental meta-logical system for implementing your own logical systems and checker for them. MetaMath Zero handles a lot of the boiler plate. You just have to write down your logical rules and encode your proofs in MetaMath Zero's format. But, to repeat, the danger of implementing your own logical system is that all the pressure is on you to verify that it is sound (i.e. it accurately represents the category theory semantics of what you are trying to prove), which I feel is what you are trying to address with this question.

Option 2: Pure logic checker

Another option is to export your proofs to some pure logic. For example, you seem to claim that your proofs can be represented in propositional logic. I could maybe believe this if your diagram chasing is more like satisfiability testing (or model checking) where you are just checking that some finite property of your finite communicative diagram holds. If you are confident that this is true, you could look at the formats used by various SAT and SMT solvers for both encoding SAT problem statements and their proofs. If you could convert your proof into the proof of a SAT problem, then this would allow you to check your proofs with a SAT/SMT solver.

Similarly, if you could likely write your proofs in FOL. You would have a bunch of axioms for category theory as well as axioms (assumptions) for all the categorical theorems your system is taking for granted. Then your constructed proof would combine all those assumptions into a proof of some final first order logic statement. You could export and check your proof using the format for some FOL solver like E or Beagle.

(Edit: Some category problems could also be represented via the internal logic of a category in pure type theory which could be checked by a type theory checker, but I think this "synthetic category theory" approach would have limited value since you would have to assume a lot about the kinds of categories you are working in.)

Note, however, for both the SAT and FOL approaches, your are just checking your logical reasoning, not the category theoretic axioms and theorems that you are starting from. Or in the SAT case, you are checking your SAT proof, but not that you are even translating the problem correctly into the right SAT problem. This could be fine if you especially trust your axioms or your SAT translation, but don't trust the proofs themselves. By exporting the proof, you would be checking the logical steps of the proof.

Option 3: Integrate into existing ITP and it's library

The last, and in my opinion the most comprehensive, option is to embed your logic into both the logic and category theory library of some ITP like Lean, Coq, or Isabelle. You could make, say, a Lean file writing down every starting axiom and category theory fact you use in your system. You could for starters assume them as axioms in Lean, but eventual prove them (likely leveraging Lean's existing category theory library). The same would be true of all the deduction rules in your system. There are many options here. You could just directly translate your proof into a Lean term (or tactic) proof. You could also, to make the translation easier, make custom Lean tactics to cover some of your rules. I would start simple with just a smaller subset of your logical system. But with enough work, eventually you would have a full embedding of your logic into Lean's (or Isabelle's or Coq's) and it would be fully integrated with the mathematical theory of categories already in Lean (or Isabelle or Coq). So you could translate both the statement you are proving in your system to an easy to read Lean statement along with a Lean-checkable proof of that statement.

Prior work on similar interchange systems.

As I mentioned there are many ways to communicate back and forth with an ITP or external checker.

Lots of theorem provers have export formats which can be checked with an external checker. Also, it is possible to use these external formats to embed a simple logic into a more powerful one. For example, Mario Carneiro imported the whole MetaMath library into Lean's logic. And someone else imported all of Lean's library into Coq (I can't find the reference off hand). But note, these translations don't have a lot of value. Sure, they work as (over-engineered) external checkers, but the translated proofs don't align at all with the existing libraries in the stronger system unless a lot of alignment work is done manually. For example, in the translation of MetaMath into Lean, Mario did do just enough alignment to prove Dirichlet's theorem in Lean's natural numbers using the MetaMath translation. On the other hand, the translation of the prime number theorem into Lean uses a different MetaMath definition of logarithm, limit, and real number which would require a lot of work to align with the existing Lean definitions.

There do exist Logical Frameworks like Dedukti which in theory let one store proofs from many ITP systems into a common format, but I'm really not sure they work well as an interchange format for proofs, again because of alignment issues.

Robert Y. Lewis and Minchao Wu made a bidirectional interface from Mathematica to Lean. I think in their system it is possible to both call Lean from inside Mathematica and Mathematica from inside Lean. Besides the communication protocol, again the question is about alignment of concepts from one system to another.

Hammer systems like Isabelle's Sledgehammer and Coq's CoqHammer work as follows. They are tactics in Isabelle or Coq which take the current proof state goal and convert it into a FOL problem. Then that problem is sent (via some interchange format) to a FOL solver like E. If E finds a solution, then that solution is decoded into a tactic proof in Isabelle or Coq. I'm less sure on this, but I think the hammer tactic doesn't directly translate every step of the proof into Isabelle, but instead it uses the E proof as a hint for reconstructing the proof with powerful Isabelle tactics like MESON (a FOL solver tactic built in Isabelle).