Comment by marwahaha

I was involved in building https://prove2.me (but I am not affiliated with Anthropic nor involved in anything related to FLT). I think the key insight in prove2me is to prove theorems "top-down", which allows a large number of users to collaboratively work on a single theorem statement. This setup also seems to work well for a "swarm" of agents. I posted more of my thoughts on the Lean Zulip.