I am not aware of a specific Lean reference/tutorial (of course they are out there somewhere). But you don’t really need nor even want to be able to read/write Lean. Your AI will read/write Lean, not you. The point of Lean is that it allows you to trust AI output, and trust is normally the achilles heel of AI output.
One key point is that you neither need, nor want, to read/write Lean yourself. The point of Lean is to allow your AI to do math without you needing to check the lines of code. Lean was built so that the lean code only runs if the maths is correct. So you can ask AI to write Lean to prove X, and if it runs (no “sorry” as Lean calls it), then you know the AI really did prove X. This removes the main difficulty of using AI, which is being able to trust anything AI does. If AI says it proved X using Lean, know you for a fact that X has been proved, and you only need to trust the AI when it tells you what X is. Since asking AI what X is just depends on translating the result from one format (Lean) to another format (e.g., pdf) this is an exercise where AI is highly trustworthy.
You can see this in the recent announcement by OpenAI that they solved the Navier-Stokes with a counterexample to the existence and smoothness problem. Nobody wondered if their proof was correct or not because they announced that it was proved in Lean, but equally noone actually read the proof. Because it is in Lean we all know that it is correct, and we only have to trust that the proof is about what they say it is. Contrast this with the proof back in 1989 of the Four Colour Theorem. “At first, The New York Times refused, as a matter of policy, to report on the Appel–Haken proof, fearing that the proof would be shown false like the ones before it. Some alleged proofs, like Kempe’s and Tait’s mentioned above, stood under public scrutiny for over a decade before they were refuted.” [Wikipedia] With Lean there is no waiting months or years while other people read and confirm, if the Lean code runs it is correct.
This is why Lean, which has existed for over a decade, recently moved from an esoteric thing a few mathematicians used to being widespread. Because it is no longer a programming language you use, instead it is a programming language that allows you to trust AI.
So how do I use Lean? I just chat with Claude. My work in the LeanEconomics repo began with me saying [all the following paraphrases my Claude Code session, R=robert, C=claude]:
R: I want to do a project in folder X, we are going to prove existence of equilibrium in Bewley-Imrohoroglu-Huggett-Aiyagari models using Lean. Install Lean and get a copy of Mathlib, read the three papers I uploaded (two of which contain proofs of existence). Give me a proposal starting with a proof that the value and policy fn have a unique solution.
C: I installed Lean. I would like to use git so we can track progress. We need to do X, Y and Z to prove that the value and policy fn have a unique solution. The first thing that we need which is not in mathlib is Berges maximum theorem.
R: Do Berges maximum theorem, we will use the repo https://github.com/LeanEconomics/LeanEconomics
C: done Berges maximum theorem, next is X, Y and Z
R: do X and Y, then report back
C: done, next is Z
R: do Z
C: done Z
R: give me a progress report, what is done and suggest next steps
etc.
This is how things went. I just chat with Claude about Math. Sometimes Claude just does things (especially if you give it a copy of the theorem and proof that already exist). I chose the existence and uniqueness of BIHA stationary eqm because it is a topic I have worked on before, so occasionally there were chats like,
C: next I will use the Feller property to prove uniqueness of the stationary agent distribution
R: should we do both Feller and Mixing conditions?
C: good idea, now doing both
Or another chat
C: I cannot apply Lasry-Lions to Aiyagari as it requires a shared distribution agent across interest rates
R [a few hours later I had an idea and returned to this]: We know that if you start from an arbitrary initial guess, then you converge to the unique stationary agent distribution, can we apply Lasry-Lions using the same arbitrary initial guess for both interest rates
C: yes, we now have Lasry-Lions applied to Aiyagari. But the Lasry–Lions conclusion needs the pairing to be monotone in the distribution, and for a coupling through a price it is not, which is Graber and Matter’s point.
Eventually once I felt we had proved enough,
R: write a pdf explaining our results
C: here it is, in filepath X
I glanced briefly at the contents of a few lean files once we were done, but I certainly cannot read nor write Lean. That is however the point. Lean is not for me, lean is for Claude. So that when Claude tells me we proved X, I know that we actually did prove X. What I did read was the pdf, and I checked this contained the statements what I expected. I just trust that the pdf really is what the Lean is proving.
The whole process is quite fun, although also rather quite disconcerting. You focus on the main math concepts, and Claude+Lean does all the actual lines of proof. Fun as you only think about the math concepts. Disconcerting as you can feel the ground shifting underneath your feet (probably less disconcerting if you are younger).
Long story short. Tell Claude (or whatever AI you use) to install Lean (the programming language) and Mathlib (a collection of mathematical objects/results you will build on). Then just start playing, pick a mathematical result you already understand for your first run, as this way you will understand everything Claude tells you about what it is doing.
PS. As mentioned, while you know for a fact the AI did prove X because the Lean code runs (no “sorry”) you are still dependent on the AI to ‘translate’ X into, e.g., pdf so that you can read what X actually states. Personally, I find that one of the few tasks I can 100% trust AI on is translating documents from one format to another. Actually the resulting freedom from formats is one of my favourite things about AI. Instead of writing equations in latex, I write them by hand, take a photo, and ask Claude to write up the eqns in photo as latex. Or I print a paper, write on it in red pen, scan, ask Claude to turn my red pen into a referee report. This freedom to work in whatever format is easiest/most enjoyable for me, and not have to care about what the final format needs to be because Claude will just convert it, is possibly my favourite thing about AI. So far across hundreds of ‘translations’ between formats I am yet to have Claude fail to nail it, so when I ask for the pdf of the Lean results, I trust that the pdf of the theorem is correct, and we already know the proof of the theorem is correct because Lean is sorry-free.
You can do anything vaguely economics here, happy to accept micro as well as macro contributions.
