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.10.0-rc2.
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.
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.10.0-rc2.
Formalizing some math from bbchallenge and busycoq.
This project can compile under Lean 4.10.0-rc2.