Building an Autoformalizer on Analysis

Stream: Machine Learning for Theorem Proving

[Blanca Luo]

Hi! I'm interested in a short-term project that trains a model to autoformalize proofs in the field of analysis (real/complex analysis, measure theory, etc). I plan to get informal->formal paired data from Tao's ongoing Analysis I project and from mathlib, feed them to a base LLM, and then perform some fine-tuning and reinforcement learning. Since I'm still semi new to Lean and ML, I wonder if the method and scale of this project sounds valid, and if this kind of tool will be meaningful/helpful? Any thoughts and advice are welcomed!

[Anthony Wang]

I suspect your main difficulty would be getting enough training data to get useful results out of this. Some other people have been working on Lean autoformalizers as well, so I'd recommend checking out their papers for their methods and datasets that they used. Also, I think RL seems more useful for generating proofs rather than autoformalization so I'm curious as to how you plan to use it for your project.