Are LLMs being trained with knowledge of tactic state?

Stream: general

[Dan Abramov]

This isn't in reference to any specific LLM — just curious what the state of the art is.

I've tried using LLMs a little bit (only online ones like Claude Sonnet and o3-mini-high) and they haven't been great. I'm assuming their knowledge of Lean is kind of general, based on whatever's available on the internet.

There are a couple things I'm curious about:

• Do we know of any LLMs being specifically trained or fine-tuned on Lean code
• Do such LLMs get the "tactic state" as one of the inputs into consideration

The second question is particularly interesting to me. When I'm working on a proof in Lean, seeing "what's in the right panel" at every line is essential for my reasoning:

Screenshot 2025-02-22 at 20.56.22.png

I might be wrong here but intuitively it seems that LLM output would be better if the input it was trained on included the tactic state of every line for the proofs it's being trained on.

Does my assumption make sense? Has anyone tried training LLMs on Lean code? Does including the tactic state like I described seem like a good idea, and has anyone tried that?

[Kyle Miller]

off topic math tip

In that strong induction proof, you only need to do cases on primality inside the induction itself.

example {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p ∣ n := by
  induction' n using Nat.strong_induction_on with n ih
  by_cases np : n.Prime
  · use n
  · rw [Nat.prime_def_lt] at np
    push_neg at np
    have ⟨m, mlen, mdvdn, mne1⟩ := np h
    have : 2 ≤ m := by
      have : m ≠ 0 := ne_zero_of_dvd_ne_zero (by omega) mdvdn
      omega
    obtain ⟨p, pp, pdvdm⟩ := ih m mlen this
    use p, pp
    exact pdvdm.trans mdvdn

[Kyle Miller]

There's a #Machine Learning for Theorem Proving channel you might be interested in.

[Kyle Miller]

I'm working with people that have been training LLMs that guess tactics to use based on the current tactic state. I don't have anything to point you toward though yet.

[Eric Taucher]

This presentation by @Jason Rute for Lean Together 2025 is worth watching.

The Q&A topic is here.