proofs | Reservoir

Random proofs in Lean 4.

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.

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).

This project can compile under Lean 4.27.0-rc1.

Formalizing some math from bbchallenge and busycoq.

This project can compile under Lean 4.27.0-rc1.

BBf = Busy Beaver function for Fractran programs. See the wiki for more details.

This project can compile under Lean 4.27.0-rc1.