I seriously doubt mochi's going to be any help for the lean formalization effort.
But a lean-assistive llm trained on mochi's work? Ahhh! What an intriguing possibility!
But a lean-assistive llm trained on mochi's work? Ahhh! What an intriguing possibility!
https://leandojo.org/ https://github.com/lean-dojo/LeanCopilot https://arxiv.org/abs/2404.07382
As far as making LLMs understand mochi math... I'm going to go out on a limb and say it will probably take less time for us to build an AI that understands mochi than it would take to understand mochi ourselves.
The progress isn't insane or miraculous. But it's moving the needle in an otherwise somewhat stagnant area. And that means we need to pay attention and update our beliefs and working theories.