I am a Research Software Engineer/Tech Lead at the Lean FRO and a mathlib maintainer.
How to reach me: send me a message on Zulip
Pronouns: he/him
I am a Research Software Engineer/Tech Lead at the Lean FRO and a mathlib maintainer.
How to reach me: send me a message on Zulip
Pronouns: he/him
The math library of Lean 4
Lean 4 programming language and theorem prover
A lecture on a proof of the Freyd-Mitchell Embedding Theorem
TeX
A browser-based IDE for the untyped lambda calculus. Try it:
Technical report on the architecture of the GUI of the Windows operating system
TeX