This is an active area of research and experimentation! Much of Lean community a...

		danabramov 3 months ago \| parent \| context \| favorite \| on: The Math Is Haunted This is an active area of research and experimentation! Much of Lean community are on Zulip (which is kind of like a forum?) and you can see many relevant threads here: https://leanprover.zulipchat.com/#narrow/channel/219941-Mach...