Skip to content

Latest commit

 

History

History
57 lines (42 loc) · 2.71 KB

README.md

File metadata and controls

57 lines (42 loc) · 2.71 KB

Part I : Next-step suggestion

Builds a neural next-step suggestion tool, introducing concepts and past work in neural theorem proving along the way.

Notebooks:

Topic Notebook
0. Intro notebook
1. Data notebook
2. Learning notebook
3. Proof Search notebook
4. Evaluation notebook
5. Context notebook
6. LLMLean tool notebook

All notebooks are in (partI_nextstep/notebooks).

Artifacts:

Name Huggingface
Data: mathlib extractions l3lab/ntp-mathlib
Data: instructions (state-tactic) l3lab/ntp-mathlib-instruct-st
Data: instructions (+context) l3lab/ntp-mathlib-instruct-ctx
Model: state-tactic l3lab/ntp-mathlib-st-deepseek-coder-1.3b
Model: +context l3lab/ntp-mathlib-context-deepseek-coder-1.3b

Setup

Setup Lean in VS Code

To try the interactive tool, you will need VS Code and Lean 4.

Please follow the official instructions for installing Lean 4 in VS Code: Installing and configuring an editor.

Setup Lean on the command line

Additionally, to run the notebooks you will need Lean 4 installed on your laptop/server.

On Linux or in a Colab notebook, run this command:

# from https://leanprover-community.github.io/install/linux.html
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
source $HOME/.elan/env
lake

For MacOS see:

https://leanprover-community.github.io/install/macos.html

Setup language modeling tools

The notebooks use pytorch and Huggingface transformers and datasets. The notebooks ran successfully with transformers==4.39.2 and datasets==2.18.0.