🖇️ Articulation and Syntax Processing #213

New Issue

aniva · 2025-06-19T13:23:40-07:00

aniva commented

2025-06-19 13:23:40 -07:00

A couple of features are missing which could be useful.

Articulation

A search which can be concluded in Pantograph does not immediately yield usable Lean code. This is because of the divergence between the search and presentation views.

The main challenge of an articulator is the divergence between the syntax and expression. For example, repeat sorry would solve all goals with sorry. If we use this to perform drafting, at the conclusion of the goal, an articulator would need to unroll the repeat tactic combinator. The existence of such tactic combinators is difficult to handle. For example, one could also do repeat (simp <;> sorry) as a drafting tactic.

Proof Portability and Efficiency

The most efficient form of storing a proof for further checking is the proof term as an .olean file. This format is fragile and not portable between Lean versions. On the other hand, a proof stored entirely in tactic form is not universally portable either since the behaviour of many tactics is volatile.

I suspect the best way to write such portable proofs is to use very simple tactics such as apply or rewrite. This is something the articulator could handle.

Decomposition

Also called "Lemma Condensation" in Trillium, this involves collecting hot spots in a proof and extracting them as lemmas. It is also one of the goals of the ExpMath project.

Syntax-Level Processing

Language model researchers want to be able to execute tactics in a line. For example,

match x with
| .zero => sorry

should return "case ... not handled". An agent seeing this feedback could supply the case:

| .succ => sorry

To implement this, we could have a syntax prefix stored in every goal object as a "partial solution". When new syntaxes come in, they could be elaborated in conjunction.

A couple of features are missing which could be useful. ## Articulation A search which can be concluded in Pantograph does not immediately yield usable Lean code. This is because of the divergence between the search and presentation views. The main challenge of an articulator is the divergence between the syntax and expression. For example, `repeat sorry` would solve all goals with `sorry`. If we use this to perform drafting, at the conclusion of the goal, an articulator would need to unroll the `repeat` tactic combinator. The existence of such tactic combinators is difficult to handle. For example, one could also do `repeat (simp <;> sorry)` as a drafting tactic. ### Proof Portability and Efficiency The most efficient form of storing a proof for further checking is the proof term as an `.olean` file. This format is fragile and not portable between Lean versions. On the other hand, a proof stored entirely in tactic form is not universally portable either since the behaviour of many tactics is volatile. I suspect the best way to write such portable proofs is to use very simple tactics such as `apply` or `rewrite`. This is something the articulator could handle. ### Decomposition Also called "Lemma Condensation" in Trillium, this involves collecting hot spots in a proof and extracting them as lemmas. It is also one of the goals of the ExpMath project. ## Syntax-Level Processing Language model researchers want to be able to execute tactics in a line. For example, ```lean match x with | .zero => sorry ``` should return "case ... not handled". An agent seeing this feedback could supply the case: ```lean | .succ => sorry ``` To implement this, we could have a syntax prefix stored in every goal object as a "partial solution". When new syntaxes come in, they could be elaborated in conjunction.

aniva added this to the 0.4.0 milestone 2025-06-19 13:23:40 -07:00

aniva added the

part/Frontend

category

feature

labels 2025-06-19 13:23:40 -07:00

aniva self-assigned this 2025-06-19 13:23:40 -07:00

aniva added the

priority

medium

label 2025-06-19 13:27:24 -07:00

aniva added a new dependency 2025-06-24 15:17:04 -07:00

#220 feat(frontend): Tomogram

aniva commented

2025-06-24 15:17:48 -07:00

#220 gives a tool for analyzing the order of MetaM (and below) execution across a Lean file. It is still WIP.

#220 gives a tool for analyzing the order of `MetaM` (and below) execution across a Lean file. It is still WIP.

aniva changed title from ~~Tracker: Articulation and Syntax Processing~~ to 🖇️ Articulation and Syntax Processing

2025-06-25 10:44:06 -07:00

aniva commented

2025-06-25 21:33:17 -07:00

I suspect articulation will have to work like Project No. 3 in Trillium, where we need to have a combination of syntax and expression based processing.

Sign in to join this conversation.