Seems LLM works well on modular structure

Stream: Machine Learning for Theorem Proving

[张守信(Shouxin Zhang)]

This is just some food for thought, but I've found that LLMs struggle to tackle a complex problem all at once. However, if you allow them to build out a framework incrementally, the complexity ceiling of the APIs they can successfully complete increases dramatically.

Another thing I've found: an LLM is far less likely to succeed when trying to fill in a small sorry for an API within a single, several-hundred-line file than it is when that same small proof is isolated in its own file.

Does anyone have more extensive, practical experience with this? I feel that exploring simple, pragmatic methods to enhance the performance of LLMs for writing Lean code is a fascinating and valuable topic for the long run.

[张守信(Shouxin Zhang)]

Also, another thing I've noticed recently is that concepts like MCP have become very popular. In my limited experience, giving an LLM agent access to information from the Lean compiler and the type signatures of Mathlib APIs can significantly reduce many low-level errors.

I was wondering, are there any official plans for a "Lean MCP" or any development initiatives aimed at making it easier for LLMs to interface with Mathlib?

[Eric Taucher]

(deleted)

[Eric Taucher]

(deleted)

[Notification Bot]

This topic was moved here from #general > Seems LLM works well on modular structure by Michael Rothgang.

[Eric Taucher]

(deleted)