This repo contains some of the code I wrote to learn Lean (theorem prover) for my research in the Caltech Anima Lab on LeanAgent. This involved following the Functional Programming in Lean and Theorem Proving in Lean 4 textbooks, the Glimpse of Lean repository, and a bit of the Mathematics in Lean textbook.
Please see Lean's installation instructions, switch to version v4.6.0-rc1, and run the following
git clone /~https://github.com/Adarsh321123/LearningLean.git
cd LearningLean
lake exe cache get
lake build
Note that these commands may take a bit to run as building Lean can be pretty slow.