I came across this essay by Rodrigo Ochigame exploring possible future impact of math formalization and automation. Automated Mathematics and the Reconfiguration of Proof and Labor Abstract: This essay examines how . . . Read more

I have always wanted to learn tactics writing in Lean. But for whatever reason, none of the tutorials that exist online have been helpful. I suspect that the best way to learn to write tactics to play around and modify the existing ones. I came across this short, 4-page tactics tutorial that look . . . Read more