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