Every Lean listing in Lean Programming for AI Agents lives in a free, public companion repository, so you can run the code instead of retyping it from the page.
It builds with lake build on Lean 4.35.0 and is released under the MIT licence, so you are welcome to copy it into your own projects.
Quick start
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
git clone https://github.com/abduljaleel/lean-programming-for-ai-agents.git && cd lean-programming-for-ai-agents
lake buildThe first line installs elan, the Lean toolchain manager. The repository pins its toolchain, so lake build fetches the right version of Lean on its own.