Automating theorems-from-text: database formatting

[Ender Ting]

Hello!

I've been contemplating how to let LLMs prove theorems, and I'd really like to try a Solitaire-like approach where it can only generate valid syntax. Two challenges become apparent at this moment:

1. Metamath's database is not written in prefix code (forward Polish notation, that is), and validating parentheses isn't easy on a quick glance; hard to check on the fly, thus.

2. LLM's Structured Output (restriction of what it can theoretically generate) only supports JSON output, not very suitable for recursive expressions.

Here, I'm asking about the first point. How to rewrite all the statements so that they use prefix notation? (I've tried this on demo0.mm and it turned out the proof in there remained valid under transformation, which is to be expected but still good to know.)

Next items I'm thinking about are "what script could expand a proof fast on-demand to its steps with full statements written down", "how to support backspacing unfruitful ideas where step could not be proved", "maybe I should simply run an agent against metamath binary". (The latter would be hard since models were not trained on Metamath's rigor.)

Best wishes,

Ender

[Glauco]

Hi Ender,

1.  what script could expand a proof fast on-demand to its steps with full statements written down

as an example, Yamma does it with this method: MmToMmpConverter.buildProof()

2. I've tried this on demo0.mm and it turned out the proof in there remained valid under transformation

Could you please show an example with a small proof, so that I can understand what you mean by under transformation? (do you mean that the original proof is given back if you apply your transformation twice?)

3. about the other questions, if you could publish some code on GitHub (with stub calls for the parts you've not figured out, yet), we could look at it and come up with possible solutions

4. here (OpenAI), you can find an old thread where Stanislas Polu, from OpenAI, built a model with inference capable of proving some small theorem (there's also an OpenAI mathbox). Given that their online proof assistant was a "label suggester" I'm inclined to believe it worked backward (see point 5. below). Unfortunately, I've never found the source code for Stanislas' models.

5. you probably already know, but a non-negligible number of metamath users, tend to write proof backwards. If I had to use a LM for proof automation, I would probably try the backward approach, first (I don't know if this is relevant with respect to your questions about RPN vs FPN).
Of course, it would be fascinating to see an LM that can complete the wff for the current statement (say, copilot style) - probably a simpler goal, but pretty cool anyway.

Looking forward to your thoughts and examples.

Best regards,

Glauco

[Thierry Arnoux]

Hi Ender,

The metamath-knife utility has the -F option to output Metamath's database formulas as s-expressions since version 0.3.9 , which is a prefix format with parentheses.

Here is an example of outputs:

ax-1: (wi wph (wi wps wph))
ax-2: (wi (wi wph (wi wps wch)) (wi (wi wph wps) (wi wph wch)))
ax-3: (wi (wi (wn wph) (wn wps)) (wi wps wph))
mp2.1: wph
mp2.2: wps
mp2.3: (wi wph (wi wps wch))

areacirc: (wi (wa (wcel cR cr) (wbr cc0 cle cR)) (wceq (cfv carea cS) (co cpi cmul (co cR cexp c2))))

This option does not show which statements are hypotheses and which ones are theorem statements, but it would be easy to modify it to print different information.

BR,
_
Thierry

[Thierry Arnoux]

Hi Ender,

what script could expand a proof fast on-demand to its steps with full statements written down

Metamath-knife also has the option -e to output the full proof of a single statement in MMP format (with steps in ASCII, not as S-expressions), as a file.

Here again since the tool is thought as a library, it would be easy to customize.

(Sorry for spamming, I should have answered both points in a single mail)

BR,
_
Thierry

[Ender Ting]

> 2. I've tried this on demo0.mm and it turned out the proof in there remained valid under transformation

>

> Could you please show an example with a small proof, so that I can understand what you mean by under transformation? (do you mean that the original proof is given back if you apply your transformation twice?)

Well, let's look at content of demo0.mm. It is essentially this:

$( demo0.mm $)

  $c 0 + = -> ( ) term wff |- $.
  $v t r s P Q $.    $( metavariables and constant symbols $)

  tt $f term t $.
  tr $f term r $.
  ts $f term s $.
  wp $f wff P $.
  wq $f wff Q $.
  tze $a term 0 $.
  tpl $a term ( t + r ) $.
  weq $a wff t = r $.
  wim $a wff ( P -> Q ) $.

  a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
  a2 $a |- ( t + 0 ) = t $.
  ${
    min $e |- P $.
    maj $e |- ( P -> Q ) $.
    mp $a |- Q $.
  $}

  th1 $p |- t = t $=
    tt tze tpl tt weq tt tt weq tt a2 tt tze tpl tt weq tt tze tpl tt weq tt tt
    weq wim tt a2 tt tze tpl tt tt a1 mp mp $.

Let's rewrite every statement into prefix form. Proof of th1 remains same, exactly.

$( demo1.mm $)
  tpl $a term + t r $.
  weq $a wff = t r $.
  wim $a wff -> P Q $.

  a1 $a |- -> = t r -> = t s = r s $.
  a2 $a |- = + t 0 t $.

  ${
    min $e |- P $.
    maj $e |- -> P Q $.
    mp $a |- Q $.
  $}

  th1 $p |- = t t $=
    tt tze tpl tt weq tt tt weq tt a2 tt tze tpl tt weq tt tze tpl tt weq tt tt
    weq wim tt a2 tt tze tpl tt tt a1 mp mp $.

This demonstrates that there will be no need to update or even decompress proofs unless tuning on them.

---

Ender

пятница, 28 марта 2025 г. в 13:29:01 UTC+3, Glauco:

[Glauco]

Thanks for the clarification, Ender

I thought you were referencing the proof format, but you were clearly addressing the statements.

Appreciate your patience!

Glauco

[Ender Ting]

Hello!

> The metamath-knife utility has the -F option to output Metamath's database formulas as s-expressions since version 0.3.9 , which is a prefix format with parentheses.

Yes that's what I needed, thank you Thierry!

> Metamath-knife also has the option -e to output the full proof of a single statement in MMP format (with steps in ASCII, not as S-expressions), as a file.

Even better! Thanks,

and to you Glauco too!

Now it seems theorem auto-proving is blocked on my efforts only :-)

Best regards,

Ender

пятница, 28 марта 2025 г. в 18:52:07 UTC+3, Glauco: