Qiyuan Xu (Nov 12 2024 at 12:14): Qiyuan Xu (Nov 12 2024 at 12:14):Hi, dear Isabelle users,
Machine-learning integrated theorem proving has become hot recently. However, I hear many complaints from machine-learning colleagues about the difficulties in connecting Isabelle to machine-learning systems. This interface problem seems to become the major issue why people turn to other proof assistants like Lean.
To address this, I'm proposing Isa Proof Shell: a Unix-pipeline-based interface to Isabelle/HOL specially designed for machine learning integration. It provides a minimal yet powerful abstraction layer that eliminates human-oriented complexities while preserving Isabelle's existing automation power like Sledgehammer. Concurrency and state rollback are also supported.
The proposal can be found from its GitHub repository. Any comments, suggestions, and concerns are highly appreciated.
Additionally, I have also made a REPL server for Isabelle, also see its zulip thread. I hope machine learning users may find it useful :)
Last updated: Nov 21 2024 at 12:39 UTC