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 thre

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-Machine-Learning-for-Theorem-Proving https://leanprover.zulipchat.com/#narrow/channel/219941-Mach...