LLM coding agents are increasingly useful for writing Lean proofs, but using them in formalisation raises questions about trust, attribution, and review. I will discuss an approach that keeps the important decisions checkable by the mathematician, using Lean's kernel, Mathlib's reviewed APIs, reproducible builds, and a record of the agent's activities.
lean4-skills is a set of protocols and tools for AI-assisted Lean development. It sits between the coding agent, Lean, Mathlib, and the human formaliser: a contract for how the agent should behave, progressively disclosed reference material, slash-command workflows (such as /prove, /golf, and /review), subagents, and guidance for using the Lean LSP MCP tools, which give the agent access to the proof state and to Mathlib search.
I will draw examples from a large formalisation of de Finetti's theorem, whose development led to the initial version of lean4-skills. I will also discuss how to judge such workflows by more than whether the theorem compiles: whether they preserve the intended statement, reuse Mathlib rather than reinvent it, stay maintainable, and leave the human formaliser able to understand the proof.
=== Online talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1
Meeting ID: 898 5609 1954 Passcode: ITPtalk
