Random proofs in Lean 4. Here is a script to build all of the maintained files:
lake build BBfLean.Size20Summary
lake build BBfLean.Size21Summary
lake build BBfLean.Size22Summary
lake build BBfLean.Size22HaltedSummary
lake build BBfLean.Size23Summary
lake build BusyLean.BusyLean
lake build SquarePyramid.SquarePyramid
This is my attempt at formalizing Terence Tao's Analysis I. I gave up in the middle of chapter 4 because setoids were not fun to work with.
This project can compile under Lean 4.27.0-rc1, but is not maintained anymore.
This is my attempt at formalizing Wikipedia's proof of Rayleigh's theorem. My attempt was successful.
I submitted a pull request to mathlib4 and it was merged after some fairly heavy modifications. The mathlib4 docs are available here.
This project can compile under Lean 4.10.0-rc2, but is not maintained anymore. See mathlib4 for the maintained version.
This is my attempt at formalizing Anglin's proof of the cannonball problem. My attempt was successful and I created a summary PDF (link).
Formalizing some math from bbchallenge and busycoq.
BBf = Busy Beaver function for Fractran programs. See the wiki for more details.