alt Hacker News> Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics.
So why don;t they use AI to write Lean programs? That should make the AI-proofs more readily human undersrndable.
Replies
bckgrndrdtn • today at 1:35 PM
It's a mixed bag. Some people don't use AI, for the usual reasons that people don't use AI. Others have used AI to write Lean programs. For example the 200K loc example mentioned in OP. But generally speaking, the quality isn't good enough yet. And when you've looked at 13 AI-generated examples and found them lacking on various axes compared to Mathlib, then you'll take a break before being motivated to look at example 14.
Terence Tao talks about this [1]
> In particular, the process of converting a medium-sized Lean document (containing a few thousand lines of code, with some proofs AI-generated) into a nicely golfed and structured Mathlib submission has been an interesting experience. AI agents can be used to perform local golfs that can shave the size of the code somewhat, but global refactoring decisions, such as noticing that a certain argument appears multiple times across the document and can be abstracted into a standalone lemma that can may have additional utility beyond the file, is still largely beyond the reach of current AI tools. (I find that I can explain such a refactor to an AI agent, who can then execute it, but they struggle to spontaneously discover such refactors on their own.)
[1] https://mathstodon.xyz/@tao/116789373239346609