Automatically deriving typeclass instances
A dive into Lean 4's metaprogramming
What are deriving handlers?
[Read More]
My goal for this little corner of the internet is to catalog things I think about, and any progress I make in understanding them.
I have a variety of interests including algebraic geometry, integrable systems, and the formalization of those topics in mathlib. My main tool is Lean. Check out my past, present, and future project goals.
Go here if you want to learn more about me, or feel free to contact me.
If you're still here, maybe some of the posts below might be of interest?