IsabeLLM

IsabeLLM is a tool that integrates a Large Language Model with the theorem prover Isabelle via an API.

Installation

Scala configuration

Install SDKMAN:

curl -s "https://get.sdkman.io" | bash
source .bashrc

Install JAVA 11 and scala build tool (sbt):

sdk install java 11.0.11-open
sdk install sbt

Python configuration

Install python:

sudo apt install python3 python3-pip -y

Install virtual environment:

sudo apt install python3-venv -y

Create and activate a virtual environment:

python3 -m venv myenv
source venv/bin/activate

API configuration

Intall the openai library for python:
```
pip install openai
```
Setup a free OpenRouter account a create a new api key. Export your api key:
```
export aikey="<YOUR API KEY>"
```

Clone project and make sure it compiles

git clone https://github.com/EllbellCode/IsabeLLM.git
cd IsabeLLM

Then compile the project:

sbt compile

Configure Isabelle

Download and install isabelle2022 in the parent directory

cd ~
wget https://isabelle.in.tum.de/dist/Isabelle2022_linux.tar.gz
tar -xzf Isabelle2022_linux.tar.gz
alias isabelle=~/Isabelle2022/bin/isabelle

Add the name of your theory files to the ROOT file