Idea: Let people reverse direction

[david-a-wheeler]

Here's a crazy idea.

Perhaps metamath-lamp could allow people to reverse the statement list (e.g., the "basics" first). It's a weird idea perhaps, but I'm pretty confident that it's much easier for LLMs to start with the conclusion and generate the other parts than the reverse. I hope to eventually do some work with the AI, as a way to give hints about what to try next, and it might be nice if it'd be possible for metamath-lamp to show the statements in the same order.

If you think it's crazy, never mind :-). But I thought I'd raise it as an idea.

[expln]

Implementation of this is not too hard, but it will take some time. I will check it after completion of an embedded proof explorer (which I am developing now) and "undo/redo" feature. But I don't imagine how this may help LLMs. Could you provide an example of usage of this feature (reversed statements)? The only scenario I could imagine is that some AI program uses a tool like Selenium to automatically manipulate statements. But even then such a tool could easily reverse statements before feeding them to an LLM.

[expln]

Looks like I understood what you mean. People will take individual statements, send them to an LLM, ask it to prove, and then put results back into the editor. Do you mean this scenario?

[david-a-wheeler]

Yes, exactly.

The problem is how current LLMs work. LLMs repeatedly take the "current state" and repeatedly predict the "next likely word". This quirk means that they're very good at determining the "next immediate state" given the current state, but are terrible at long-term planning to end up with a specific conclusion. In a proof, if you repeatedly start with the goal and work backwards to something true, that can work out okay - we don't care which statement is at each leaf, as long as each one is true. But asking an LLM to end up with a very specific end statement is more challenging for it. Therefore, I expect that LLMs will be more successful if they start with the "statement to be proved" and work backwards. Metamath-exe can easily display proofs in this reversed order, making it easy to train LLMs on this. So if we make it possible to see the proofs "backwards", to make it easier to use LLMs, that might be quite useful.

Note: LLM technology might be replaced at some point with something better without this limitation. But I don't know if that will happen (or if so, when).

In any case, in theory this might not be hard - just show them in reverse order. I think it's okay to temporarily suspend visualization in that case (or just let the lines cross).

I don't think think this is high priority, but I thought I'd mention it now, because it might imply doing other things in a certain way to make this one eventually easy.