Building up Lean.Expr's

Stream: Machine Learning for Theorem Proving

[Arthur Paulino]

I had this idea yesterday and I wonder if anyone has tried it before. Instead of trying to write Lean code, an AI agent would try to create terms of Lean.Expr directly. This approach would be more easily plugged to Lean 4, as a meta program. I wonder if this path would be promising.

[Adam Topaz]

I had a similar idea a little while ago, but realized that the most convenient interface for an agent to interact with is still the tactic system, but with a restricted set of tactics (intro, apply and refine, primarily)

[Arthur Paulino]

It depends on what you mean by "convenient". Operating with Lean.Expr directly is very convenient too as it doesn't need to leave MetaM and avoids overheads related to parsing. In RL algorithms, the cycle cost is very important. That is, the cost of checking whether a new proof term attempt works or not.

[Arthur Paulino]

The main problem, however, is in the feedback the human would receive. Instead of a series of tactics, it would be some seriously ugly proof term. My thinking is that it's a tradeoff that favors the machine over the human in the loop

[Eric Wieser]

I think trying to build an Expr for a rw tactic is rather an ordeal

[Eric Wieser]

For instance, look at how large the proof term for the following is:

import Mathlib

open scoped TensorProduct

-- to show the full proof term
set_option pp.all true

set_option pp.all true
#check add_comm (1 : ℤ ⊗[ℤ] ℤ ⊗[ℤ] ℤ) 0

[Aaron Liu]

oh god

[Eric Wieser]

Giving up typeclass search and the elaborator is giving up some very carefully tuned algorithms written by humans, and asking your agent to learn those at the same time as learning formalizing mathematics

[Eric Wieser]

(and also to memorize all the instance names which are explicitly not part of any backwards compatibility guarantee)

[Arthur Paulino]

If not Lean.Expr, then maybe Syntax.
It's more constrained than pure text and still more easily pluggable via metaprogramming

[Leni Aniva]

Technically speaking Lean.Expr is also Lean code.

I've a system that can do this. I don't think we should give up the elaboration system.

Also it would be a huge pain to use this mechanism to build up any non-trivial proof. Just #print some random theorem in mathlib to see this.

[Leni Aniva]

If you have a system that incrementally builds an expression, then its basically just tactics, and we're back in square one.

[Frederick Pu]

cant you just stop the elaboration depth after a certain point

[Leni Aniva]

Frederick Pu said:

cant you just stop the elaboration depth after a certain point

What do you mean by this?

[Eric Wieser]

Arthur Paulino said:

If not Lean.Expr, then maybe Syntax.

This is a very reasonable thing to do in principle, though compared to generating raw text it is much harder to benefit from existing LLM training.

[Frederick Pu]

Leni Aniva said:

Frederick Pu said:

I meant don't unfold function and typeclass definitions.

[Aaron Liu]

They're not being unfolded, they're just normally implicit, but they're still in the Lean.Expr.