I ran some simple experiments that may be of interest to folks here: porting between Coq and Lean
Cross-posted to Lean Zulip: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/ChatGPT.20can.20help.20translate.20between.20Coq.C2.A0and.20Lean
Here’s a summary:
Making high-quality proof libraries takes a ton of work. It would be a shame to duplicate all that work for each ITP language, or to get locked out of using a specific ITP because it doesn’t have the right libraries. Cheap library reuse across languages would reduce the burden of language silos.
For instance, software verification in Lean could benefit from Coq’s advanced libraries for software, while Coq could benefit from Lean’s math libraries. Having equivalent proofs implemented in different ITPs also provides clear benchmarks for comparing research results across ITPs.
I ran some simple experiments on using ChatGPT-4 as an assistant to iteratively write and translate between Coq and Lean 4 definitions (not proofs).
These experiments found that ChatGPT significantly reduced the work to (a) write a toy ISA model and example assembly programs in Coq (~400 SLOC), (b) translate these to Lean, (c) compare the Coq vs. Lean programs for semantic differences, and (d) port a Coq bugfix to Lean as an incremental patch. The most surprising result was that ChatGPT accurately detected minor semantic differences between two implementations, one in Coq and the other in Lean, and could patch the Lean code to match the Coq code.
—
Is this direction interesting to folks here?