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 -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/metamath/2b770ce0-e13a-4a4b-b202-f2e6640d6168n%40googlegroups.com.
