Dave Ishii - Problem Solving Blog

🧠 Lean Copilot–Specific & Very Close

Lean-AI / LLM-for-Lean community

• Lean Zulip → #ai and #llm streams

• Regular discussions on:

  • tactic prediction

  • proof step synthesis

  • context window compression

  • Copilot-style autocomplete for Lean 4

• Many contributors to:

  • lean-copilot

  • LeanDojo

  • Pantograph

  • ProofNet

➡️ This is currently the closest thing to a living Copilot-Lean working group.

LeanDojo Community

• Open research ecosystem for learning-based theorem proving

• Weekly or bi-weekly open research meetings (depending on semester)

• Focus:

  • interactive proof search

  • dataset construction

  • RL + transformers for Lean

• Strong overlap with Copilot-style workflows (step-by-step guidance)

🤖 AI for Theorem Proving (Lean-heavy)

AITP (AI for Theorem Proving)

• Workshop + year-round research network

• Lean is now a primary target system (alongside Isabelle, Coq)

• Includes:

  • tool demos

  • reading groups

  • shared benchmarks

• Strong theoretical CS / ML crossover

ITP + AI Satellite Groups

• Communities around:

  • ITP (Interactive Theorem Proving)

  • CICM

  • CADE + IJCAR AI tracks

• Often host online seminar series during the year

🧩 Proof Assistants + ML (Broader)

ML4PL (Machine Learning for Programming Languages)

• Not Lean-only, but many Lean Copilot papers appear here

• Autocomplete, code synthesis, proof synthesis all overlap

Big Proof / Formal Math initiatives

• Formal Mathematics / Formalization of Mathematics

• Mathlib community meetings

  • Occasionally host AI-assisted proof talks

• Proof assistants + NLP workshops

🧪 Industry-adjacent but Research-driven

• DeepMind – Mathematical Reasoning & Lean

  • Open talks & seminars (not a WG, but recurring)

• Meta / FAIR theorem proving research

• OpenAI formal reasoning research (Lean-focused)

🧷 Where to actually participate (practical advice)

If your goal is active participation, do this:

1. Join Lean Zulip

   • Follow: #ai, #tactics, #mathlib, #llm

2. Track AITP & ITP workshops

   • They often spin up temporary working groups after workshops

3. Follow LeanDojo announcements

   • Open calls are usually shared publicly

4. Mathlib community calls

   • Occasionally spin off AI-focused subcalls

🧭 TL;DR