More or less Math in Lean. Dumpster where I throw pieces of proofs I formalized in Lean4.
Yes Mathlib4 exists, but I like having some fun. And I'm using this as exercises to learn Lean4.
Yes the code is terrible. I skimmed "Theorem Proving in Lean 4" between one or two session of Starbound and the reading of Quality Land 2.0. If your expectations are low, reconsider. It's even worse.