The Lean Zulip chat includes a "Is there code for X" section; you can go there and ask if a specific theorem or research problem has been formalized/verified in

The Lean Zulip chat includes a "Is there code for X" section; you can go there and ask if a specific theorem or research problem has been formalized/verified in Lean, and if not, whether someone is working or intends to work on it. This way you can form impromptu working groups if you find others interested in your problem.