Multi-agent collaborative theorem proving with Lean 4 and Ensue Memory Network.
Read the blog post
Prerequisites
Lean 4 Installation
Install elan (Lean version manager):
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Restart your terminal or source the environment:
source ~ /.elan/env
Verify installation:
lean --version lake --version
... continue reading