מידע כללי General Information Общая Информация معلومات عامة

Research with LLMs and Lean

All information is tentative for now!

To participate, please make sure to do these three steps: a) enroll on GR++/Webcourse, and b) enroll on the SAP Portal, and c) fill out this sign up form: https://forms.gle/j9pDiYX1psmMUaKi8.

If you encounter any difficulties in the above three steps (for instance, no seats left, enrollment cap, waitlist, etc.), please reach out: Joachim Neu - jneu@technion.ac.il.

Please also join the discussion on Piazza: https://piazza.com/technion.ac.il/fall2026/2360802

Please pick the paper you would like to present: https://docs.google.com/spreadsheets/d/1Ry2EHe4YOMsxHD8frxlwSV59zaSPYx4iSNyyq9TTr5w/edit?usp=sharing

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 (corresponding to the usual weekly workload of ~2h in class and ~4h out of class)
• Instructor: Joachim Neu
• Course language: English
• Discussion and announcements: Piazza
• 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.

Prerequisites

There are no strict/formal prerequisites. That said, given the theme of the course, you will most benefit if you are towards the end of your BSc, or in your MSc or PhD. You should know what a mathematical proof looks like, and, ideally, you have some experience with research already (but it is also fine if not). Given the methods/topics of the course, prior experience with machine learning, LLMs, programming languages, formal methods, and/or formal verification will be an advantage.

Outline

See the tentative schedule below for dates and papers.

• 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-8: seminar phase; in-class students present papers (two per week, after introductory overviews by the instructor in weeks 2 and 5); 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 9-12: 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 will be able to find a solution.

Tentative Schedule

Week 1 (1 Nov) - Hello World!

• Instructor: Administrivia, introductions, overview; live demo of a simple LLM + Lean pipeline for autoformalization
• At home: Read Tao, Machine-Assisted Proof; set up your LLM + Lean workspace; start a Lean learning game (due before week 5)

Week 2 (8 Nov) - LLMs 1: how LLMs are made

• Instructor: Overview of how LLMs are made (tokens, pretraining, post-training, reasoning models)
• Student presentation: Vaswani et al., Attention Is All You Need
• At home: Lean game; prepare next week's papers in your role

Week 3 (15 Nov) - LLMs 2: from pretraining to assistant

• Student presentations: Brown et al., Language Models are Few-Shot Learners (GPT-3); Ouyang et al., Training language models to follow instructions with human feedback (InstructGPT)
• At home: Lean game; prepare next week's papers

Week 4 (22 Nov) - LLMs 3: reasoning models

• Student presentations: DeepSeek-AI, DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning; Lightman et al., Let's Verify Step by Step
• At home: Finish the Lean game; prepare next week's papers

Week 5 (29 Nov) - Lean 1: the system and the idea

• Instructor: Overview of Lean as a system, following de Moura and Ullrich, The Lean 4 Theorem Prover and Programming Language (to be read by everyone)
• Student presentation: Wadler, Propositions as Types
• At home: Prepare next week's papers

Week 6 (6 Dec) - Lean 2: inside the trust boundary

• Student presentations: Carneiro, The Type Theory of Lean; de Moura, Avigad, Kong and Roux, Elaboration in Dependent Type Theory
• At home: Prepare next week's papers; start thinking about your project

Week 7 (13 Dec) - LLMs with Lean

• Student presentations: Wu et al., Autoformalization with Large Language Models; Hubert et al., Olympiad-level formal mathematical reasoning with reinforcement learning (AlphaProof)
• At home: Prepare next week's papers; define/pick your project

Week 8 (20 Dec) - Agents for research

• Student presentations: Romera-Paredes et al., Mathematical discoveries from program search with large language models (FunSearch); Swanson et al., The Virtual Lab: AI Agents Design New SARS-CoV-2 Nanobodies with Experimental Validation
• At home: Start work on your project

Weeks 9-12 (27 Dec, 3 Jan, 10 Jan, 17 Jan) - Project

• Instructor: A current development, then exchange of observations, ideas and lessons learned, then project clinic
• At home: Work on your project

Week 13 (24 Jan) - Project presentations

• Students: Final presentations, about 10 minutes per project: what was achieved, what comes next

Paper Assignment

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.
• Tooling for the research workflow around LLMs and Lean
  • Rendering readable English from Lean
  • A workflow for capturing research meetings and drafting research summaries
  • Knowledge-base curation for a researcher, and the interplay with long-running agents
  • Writing cleanup tools
  • Investigate why AI writing comes out as slop, e.g., undefined, proprietary, or drifting terminology, and how to improve it
  • etc.
• Propose your own project

Grading

• truncate (x,y) ≜ x ⋅ 𝟙_{{x ≥ y}}
• Project:
  • a ∈ [0,45]
  • A ≜ truncate (a,45/2)
• Seminar presentation:
  • b ∈ [0,25]
  • B ≜ truncate (b,25/2)
• Participation:
  • c ∈ [0,25]
  • C ≜ truncate (c,25/2)
• Lean game completion:
  • d ∈ [0,15]
  • D ≜ truncate (d,15/2)
• Final grade: min (A+B+C+D,100)