[tezthenerd]

If you want to see this kind of thing done “really in real time” check out Terry Tao’s recent mathstodon posts where he learns Lean while formalizing a paper of his own. Fascinating stuff.

[SkyMarshal]

https://mathstodon.xyz/@tao