Research with LLMs and Lean
All information is tentative for now!
Sign up: https://forms.gle/j9pDiYX1psmMUaKi8
Description
LLMs have arrived at the core of research: generating ideas, and producing genuinely novel mathematical arguments. But generation at this scale creates a verification bottleneck: researchers risk drowning in plausible-looking output whose correctness no one is willing to invest time to check carefully. Formal methods like Lean are the complementary force: they let a computer check logical reasoning with absolute rigor, and their historical weakness—the tedium of spelling out every step by hand—is precisely what AI now automates.
This hands-on course explores the synergy between the two: LLMs as an engine of generation, Lean as a filter for truth. We will study a) how modern AI models work and what their architectures imply for how to use them effectively in research; b) the foundations of Lean and its dependent type theory needed to verify AI-generated reasoning; and, c) through a series of practical assignments, how to wield both in tandem. The course culminates in a real research or development project—advancing your thesis, mechanizing a recent paper of yours, or improving the still-primitive tooling at the intersection of AI and Lean. We are all new to this! A central goal of the course is to learn together and exchange techniques, experience, best-practices.
Administrivia
- When? Sundays, at 10:00am for 2h, starting 1 Nov 2026
- Where? Taub 6
- Format: seminar, 2 credits
- Instructor: Joachim Neu
- Course language: English
- Grading: see below
- Dropping the course late: Since we count on everyone presenting the paper they are assigned at the beginning of the course, the course cannot be dropped later than two weeks into the semester.
Outline
- Week 1: in-class introductory lecture by the instructor; out-of-class students complete one of the Lean games at https://adam.math.hhu.de/
- Week 2-7 (approx.): seminar phase; in-class students present 2 papers per week; out-of-class students prepare the papers according to role-playing seminar style; paper topics:
- architecture of modern LLMs, and what we can learn from it regarding how/when/why they (don't) work for research
- type theory and software system of Lean, and what we can learn from it regarding how to faithfully express/check mathematical research results
- systems for using LLMs and/or Lean in research
- Week 8-12 (approx.): project phase; in-class discussion of case studies and recent developments (led by the instructor), discussion of project progress and exchange of experiences/best-practices/lessons-learned; out-of-class students work on their individual projects (see list of project ideas below, or propose your own project!)
- Week 13: in-class project final presentations
AI Usage
This is a research seminar about AI usage in research. Obviously, please use as much AI as you want/can. However, you are responsible for whatever AI output you introduce into your assignments/contributions for this class.
Two recommendations:
- Examine critically what the AI produces. Take moments to reflect intentionally on when the AI does/doesn't work, and why that may be. Bring your observations/experiences to the class discussion, they will be valuable.
- When you see an opportunity, produce repeatable prompts ("skills") to automate certain research tasks (e.g., identifying key related work). Again, this will be valuable to discuss/share in class. And you can submit these as part of your project.
AI access: The class will require an AI subscription, likely roughly at the level of $100/month (e.g., Claude Max 5x, OpenAI Pro). If this would prohibit you from taking the class, please reach out, and we may be able to find some accommodation.
Some Project Ideas
- New research result ("LLM first, Lean second")
- Use AI to identify and solve a research problem. Use Lean to show that the solution is correct. Write Lean to help the LLM understand the research problem better.
- Mechanize existing research ("Lean first, LLM second")
- Use Lean to mechanize/check the research results in someone else's research paper
- Build/contribute to a Mathlib-style library of basic definitions for some other subject area
- Game theory
- Distributed computing
- Cryptography
- Algorithms
- etc.
- Improve our understanding of the LLM/Lean interplay
- Analyze tricks to reduce token consumption and improve mechanization performance
- Build a system
- Prototype a Lean-mandatory PDF-optional "preprint" repository
- Build/improve a Lean-oriented harness for LLMs
- Develop repeatable workflows ("skills") for AI/Lean-assisted research
- etc.
- Propose your own project
Grading
- $\operatorname{truncate}(x, y) \triangleq x \cdot \mathbb{1}_{{x \geq y}}$
- Project:
- $a \in [0,45]$
- $A \triangleq \operatorname{truncate}(a, 45/2)$
- Seminar presentation:
- $b \in [0,25]$
- $B \triangleq \operatorname{truncate}(b, 25/2)$
- Participation:
- $c \in [0,25]$
- $C \triangleq \operatorname{truncate}(c, 25/2)$
- Lean game completion:
- $d \in [0,15]$
- $D \triangleq \operatorname{truncate}(d, 15/2)$
- Final grade: $\min(A + B + C + D, 100)$