AI tutorial for LEAN beginner

Stream: Machine Learning for Theorem Proving

[Miheer Dewaskar]

Hi everyone:

I started learning LEAN a few weeks ago motivated by the potential of AI to help mathematicians. My aim is to formalize math in my field (of Probability & Statistics) with the ultimate hope that LEAN + AI might become an effective research assistant. So from a perspective of a beginner user to LEAN (e.g. the user story of Alice in @Jason Rute's talk at Lean Together 2025), I want to ask if there are any tutorials/documentation on AI tools that I can use to help me with learning LEAN and the formalization process.

Currently, I am able to read and understand around 50% of LEAN code that I see online, however proof formalization still seems like a daunting task. I just came across LEAN Explore, which seems useful to find relevant Mathlib libraries. For help just dealing with LEAN 4 syntax and debugging the formalized code, would Cursor or Github Copilot be useful? @Terence Tao's youtube channel gives nice examples of this.

To summarize, is there a webpage where AI tools useful for beginners to learn LEAN are listed?

[Jason Rute]

To revive this discussion, no, there isn't a website or other landing place (other than maybe this Zulip channel) to find this sort of information. I think people have had the most luck with the following three categories of tools:

• Online search websites like https://www.leanexplore.com/, https://leansearch.net/, and https://www.moogle.ai/
• Off-the-shelf AI coding assistants, including Cursor, Continue.dev, Tabnine, and GitHub Copilot, as well as chatbots from the major AI companies. It matters a lot which specific model you use, including the exact model name and version number and whether or not it has a thinking mode. Often, the older, default models are not the best ones. See elsewhere on this channel for specific recommendations and user feedback about which models work best both for code assistants and chat bots. (This information will of course change as newer models are released.)
• Powerful tactics (most of which don't use neural AI at all), like Canonical, Lean Hammer, Lean Auto, Duper, Lean SMT, Grind, etc. Many of these are so new (and others are still in development) that I don't think there is consensus on what problems they are good at solving. (Honestly, I wouldn't mind a website just sorting out these various tactics. I've become quite lost.)

There are also a lot of research projects and papers, but most of those are not usable by average Lean users. Kimina-Prover has a fairly user-friendly demo, although it may not be user-friendly enough to be widely used. DeepSeek-Prover v2 is open sourced and there are some demos, but I think to use it in practice, you have to find and put in their system prompt. (Not a lot has changed since I gave my Last Mile talk. :frown:)

[(deleted)]

Kimina Prover is extremely weak. I recommend using DeepSeek Prover V2.

[(deleted)]

But anyway, for learning, I don't think AI is of much help.

[Justin Asher]

Just to add my two cents, I found AI to be very helpful understanding already written Lean code. It is just not great right now at writing Lean code. I would also imagine if you used the LeanExplore MCP integration with something like Claude, then you could discuss with it different declarations and ideas in Lean with the model being properly grounded and factual.

[Jason Rute]

Huỳnh Trần Khanh said:

Kimina Prover is extremely weak. I recommend using DeepSeek Prover V2.

To be clear, what does this even mean? How do you use DeepSeek Prover V2? Do you self-host? Do you use one of the online demos? Do you use a service like OpenRouter? Do you add in a system prompt? Do you use the 7B model or the 617B model? Is it useful in practice? Or are you just going by the published metrics?

[(deleted)]

This is my firsthand experience actually. I have to use these AIs extensively at work.

[(deleted)]

For the Kimina model I use the online demo (https://demo.projectnumina.ai)

[(deleted)]

For the DeepSeek Prover model I use an inference provider for the 617B model. I pasted the recommended system prompt.

[(deleted)]

I know saying this will not make the anti-AI people happy, but using these AIs makes me a lot faster and more productive at work.

[Jason Rute]

Yeah, I guess it makes sense that you would prefer the 617B DeepSeek model over the 7B Kimina model. If I may ask, do you use the DeepSeek model for general Lean development, or for special purposes? If for general Lean development, do you use it for writing proofs or for more general Lean coding? Do you have a recommended workflow?

[(deleted)]

I don't use Lean as a programming language. I use these AIs for generating proofs. I have a workflow. Generally, strong mathematical intuition is required—currently, no amount of AI can replace it. The first step is to actually have the proof in my mind! After that, I try to decompose the proof into smaller steps. For each step, I try to guess if the AI can solve it automatically or not.

If the step is dependent on algebraic manipulation, AI can solve it. If the step is dependent on choosing some special witness values (epsilon delta proofs :eyes:), AI can do it just fine. Or if I guess that the step can be solved by simple induction, AI can do it just fine. I then run DeepSeek Prover on the step 2 times in parallel, and choose the proof that works.

If DeepSeek Prover starts writing in Chinese, or Russian, or being incoherent, I check whether the theorem statement I feed into DeepSeek is incorrect. Usually this involves using a more general purpose LLM like Gemini 2.0 Pro to do a sanity check. I know I have a brain but I currently don't use it. If it is, I refine the theorem statement, or conclude that the way I decompose the problem into multiple steps is wrong, and go back to the drawing board.

[Jason Rute]

Is there a good example of the sort of problem you have found DeepSeek-Prover v2 really helpful for that other tools don't come close?

[(deleted)]

There aren't that many contenders. But the problems that I have to solve generally look like this: https://artofproblemsolving.com/wiki/index.php/2005_IMO_Shortlist_Problems/N2

[(deleted)]

Given that DeepSeek Prover is specifically trained on olympiad problems, its performance on these types of problems is quite good.

[(deleted)]

I know that SMT solvers can be quite powerful when working with inequality problems as I've used them standalone before. But I haven't figured out how to use them with Lean.

[(deleted)]

If I do figure out a way, that means my productivity could be even higher. My job is like an automation arms race. I have to be better at automating than my employer.

[(deleted)]

I think there's a few people here who do the same kind of work as I do. I invite these people to chime in.

[Jason Rute]

Is “the kind of work” you do secret?

[(deleted)]

No. It's about training AI models to write Lean code for olympiad problems. And my employer tries to solve the math problems with their existing AI models in advance and only when they fail, they make the problems available for me to solve so they can improve their AI further. My work contributed to the development of the Kimina model.

[(deleted)]

Initially I was skeptical that a good LLM for Lean could exist. But then a few months ago, everything changed, and the employer suddenly announced that there are good LLMs available, and I'm expected to use them in my work.

[Mario Carneiro]

lol, those two things are not in contradiction

[(deleted)]

whatever it's midnight my brain isn't operating properly I hope someone can gain something from what I said but if it's too incoherent I beg your forgiveness

[Mario Carneiro]

I mean, you might think that good LLMs for lean don't exist while at the same time your manager is pushing you to use them. In fact that sounds like a very common situation