Metamath Christmas challenge

[savask]

In the programming community there is a nice tradition to solve programming puzzles on each day of advent, the most famous such challenge being Advent of Code. I have not been patient enough to create enough Metamath puzzles and, needless to say, advent has already started, yet I propose something similar: the Metamath Christmas challenge! The goal is to prove a small but remarkable theorem of Ryley, that every rational number is a sum of three cubes of rational numbers:

  $d a b c A $.
  3cubes $p |- ( A e. QQ <-> E. a e. QQ E. b e. QQ E. c e. QQ A = ( ( ( a ^ 3 ) + ( b ^ 3 ) ) + ( c ^ 3 ) ) ) $= ? $.

To ease the task, I prepared a file with four lemmata, which should help you fill in the gaps and finish the proof:

https://gist.github.com/savask/953a9c38205fb714607faec80ac57b7b

Notice that I have not formalized the proof myself, so if you see a problem with the file, please tell me, and I will hopefully fix it.

I hope someone will find this little challenge interesting - of course, the first person to formalize the proof has the full rights to put their name on the theorem and claim it for themselves :-)

Related questions

1. When preparing the challenge, I was wondering if I missed a bracket somewhere or forgot to put some brackets etc. Is there an easy way to check that a statement passes grammar checks? I think mmj2 could do that, but it is rather cumbersome to use as it is not really supported anymore.

2. In 2017 Norman suggested putting unproved statements of MM100 theorems in set.mm as comments, so that people have an easier time trying to prove these results. Quite often even stating these theorems requires new definitions which are hard to get right. What do you think about having a separate file in the repository with "easier" unproved statements, which do not require new definitions to state or prove? These may serve as a guide on what to do for newcomers (or anyone else), or as a work in progress plan to formalize some big result.

3. If you check the challenge file, you will quickly see that the main part of the proof consists in checking some polynomial identity. Are there any Metamath tools which can prove such statements automatically (by expanding brackets, for example)?

[Glauco]

1. When preparing the challenge, I was wondering if I missed a bracket somewhere or forgot to put some brackets etc. Is there an easy way to check that a statement passes grammar checks? I think mmj2 could do that, but it is rather cumbersome to use as it is not really supported anymore.

Hi Savask,

Yamma checks the grammar of every line of a .mmp file

It gives you a Diagnostic at the first symbol that does violate the grammar (and it suggests you all possible valid characters, at that point of the line)

But I believe that Yamma is at least as cumbersome as mmj2 :-)

[Igor Ieskov]

Hi Savask,

For syntax check you also can use mm-lamp. You have to put each statement one by one into mm-lamp, so this is not very convenient, but it doesn’t require any installation.

1. Navigate to the mm-lamp web site https://expln.github.io/lamp/latest/index.html

2. In the “Source type” select “Web”

3. In the “Alias” select “set.mm:latest”

4. In the opened confirmation dialog click “Confirm”. This will start downloading the latest version of set.mm from us.metamath.org. Wait until the file is loaded (for me it takes about 20 seconds)

5. In “Scope” select “Stop before”

6. In “Label” type “box” and select “mathbox” from the dropdown

7. Click “Apply Changes”

8. Add all the statements you want to check by clicking “+” button. You may see letters G and P appear to the left of each statement. They don’t matter for syntax checking.

9. Click “Unify all” button. This button has shape of a few small connected circles. Make sure all the statements you’ve added are unselected before clicking this button (the checkbox to the left of each statement is empty).

10. If any of the statements have syntax error, you will see an error message in red color under such statement.

I checked all the statements from your challenge - all of them are syntactically correct. Nice challenge by the way, I will be happy to spend some time on it.

–

Igor

[savask]

Glauco,

> But I believe that Yamma is at least as cumbersome as mmj2 :-)

Yamma looks very cool, but it requires VSCode (and I'm on linux...), so I agree that it is perhaps easier to get mmj2 going.

Igor,

> For syntax check you also can use mm-lamp.

Thanks for checking the file! Mm-lamp looks very promising. I tried checking some statement in your proof assistant, and, I'm probably going to express a common remark, but I wish it was possible to type proofs in text there as in mmj2, instead of clicking through GUI. Nice tool, in any case!

[Glauco]

I'm roughly 50% on Windows and 50% on linux, but I develop and use Yamma on linux only.

VSCode on linux works very well... :-)

p.s.

VSCode =!= Visual Studio

[Thierry Arnoux]

Very nice initiative!

Obviously Igor is on the right way with theorem cu3addd.

Concerning your question 3., one of the ideas behind my project "rumm" was to allow one to write tactics for Metamath in general and set.mm in particular. 

Some tactics could be "expand" or "simplify", with a tactics being roughly "if the goal matches this expression, then try applying this theorem, or try (recursively) applying this tactics again".

I developed the tool to the point where some non-trivial theorems could be proved automatically through such tactics, however I felt my tactics language was not quite powerful enough to express what I wanted.

BR,

_
Thierry

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/5e1c4b82-c6df-43b6-bd02-96a808e1a7abn%40googlegroups.com.

[savask]

Thierry, that's a cool project, I had no idea it exists.

I took a brief look at the syntax and the currently implemented tactics. The "equality" tactic looks very useful, others are a bit too technical for me to understand. Correct me if I'm wrong, but it should be possible to write a tactic for expanding polynomial expressions, and maybe to port Mario's tactic for long addition and multiplication.

I agree that one would need a more powerful language to implement some of the more interesting tactics. The "improve" tactic from metamath exe seems as one example.

I'm not sure if it's beneficial to come up with your own scripting language for tactics, but if I were to use a library to write a tactic, I would certainly prefer to have functions from your language like matching patterns etc.

[Thierry Arnoux]

Hi Saveliy,

The current implementation not only performs matches (that it,
unifications), but also allows you to capture the unification results in
new variables, which can later be reused.

One of the reason I thought about a scripting language is that I wanted
the core (the language interpreter) to be database agnostic, while the
script themselves could be tailored to a database. But that might also
be realized with a multilayered library (for example, one specific
library using services from another, agnostic, library). A scripting
language also has the advantage that it can be used as an external,
without the need to e.g. recompile for each use. In the end, the
language in which I specify how the tactics are used, can also be used
for writing the tactics themselves.

Any such tactics language should definitely allow one to implement
operations as developing or simplifying formulas. That's valid for first
and second order logic formulas, but also for algebraic formulas in the
complex numbers, and the abstract level of generic algebraic structures
like groups, rings and fields. Working on numerical expressions,
performing long additions and multiplications, or for example connecting
to an SMT solver, might require the ability to use some custom code.


Maybe I'll have another go at implementing the tactics directly in an
(existing) programming language rather than designing a scripting
language, and see where this leads me. I'd probably use metamath-knife
as a basis for that.

_
Thierry

[Igor Ieskov]

> Obviously Igor is on the right way with theorem cu3addd.

I was able to prove 3cubeslem1, 3cubeslem2 and a bit of 3cubeslem3 in “manual” mode using current capabilities of mm-lamp (I can share proofs if needed). To my surprise mm-lamp works with proofs containing 350 steps (not very fast though, but workable). I feel like I would be able to complete proving 3cubeslem3. But it starts feeling like a not proper use of time doing such proofs manually. So, I am going to start working on adding some automation capabilities to mm-lamp.

> I hope someone will find this little challenge interesting

For sure! Before that challenge I never created new proofs. I was only developing my proof assistant and testing it on proofs based on David’s tutorial for mmj2. But this challenge gave me a good starting point and new ideas of what I can add to my proof assistant.

> What do you think about having a separate file in the repository with "easier" unproved statements, which do not require new definitions to state or prove? These may serve as a guide on what to do for newcomers (or anyone else), or as a work in progress plan to formalize some big result.

I think this is a great idea. At least that’s what I needed to start doing my new proofs.

-

Igor

[savask]

Thierry,

> Maybe I'll have another go at implementing the tactics directly in an (existing) programming language rather than designing a scripting language, and see where this leads me. I'd probably use metamath-knife as a basis for that.

You are definitely exploring new ground here. As far as I understand, most proof systems (like Lean) use one language for proofs and tactics, so they don't have to think about these kinds of problems. I can see how a universal tactic language can be useful though, for one, if it's simple enough, every independent proof assistant could implement some core and immediately get access to all already written tactics for metamath.

Igor,

> I was able to prove 3cubeslem1, 3cubeslem2 and a bit of 3cubeslem3 in “manual” mode using current capabilities of mm-lamp (I can share proofs if needed).

Looks like you're close to proving 3cubes indeed!

> ... But it starts feeling like a not proper use of time doing such proofs manually. So, I am going to start working on adding some automation capabilities to mm-lamp.

Funny enough, I had a similar experience with metamath. My contribution was very small, but I was surprised how tiring it was to do the most mundane of things, so I thought I would try to make a proof assistant with automation myself. Long story short, turns out making a proof assistant is way harder than making a verifier, so I gave up :-) It would be amazing if some tool, like metamath-lamp, would have basic automation allowing one to prove statements like 3cubeslem3 with ease.

[Igor Ieskov]

A proof for 3cubes is ready - https://github.com/expln/metamath-theorems/blob/master/metamath-christmas-challenge-2023/metamath-christmas-challenge-2023.mm 

-

Igor

[savask]

> A proof for 3cubes is ready

Igor, congratulations! I hope you'll prepare a pull request to set.mm, in my opinion the result is interesting enough to have it, at least, in a mathbox.

I looked over your proof file. I think some smaller lemmata (especially leading to the proofs of 3cubeslem1 and 3cubeslem2) can be joined into bigger chunks, that way proofs will be able to reuse same statements (for example, in syntax breakdown steps). Also I have a feeling that the metamath.exe minimization algo will be able to do more with bigger proofs. Similarly, many proofs share the same hypotheses (for instance, |- ( ph -> A e. RR ) ), and it can be reused if you put several statements into one block.

Also you seem to be jumping back and forth from the deduction style (like in _3cubeslem1_gtz_d) and "usual style" (like in _3cubeslem1_gtz_i). I don't know if that's necessary, but the idea is usually to carry the proof in deduction style where it's possible and maybe switch to the usual style near the end to state the main result.

If you prepare the set.mm pull request, more experienced metamath users will surely give more comments on how to simplify the proof, what labels to choose etc. I think it can be shortened quite a bit.

By the way, did you end up using some automation to finish the proof, or you did it all by hand after all?

[Igor Ieskov]

> Igor, congratulations! I hope you'll prepare a pull request to set.mm, in my opinion the result is interesting enough to have it, at least, in a mathbox.

> I looked over your proof file. I think some smaller lemmata (especially leading to the proofs of 3cubeslem1 and 3cubeslem2) can be joined into bigger chunks, that way proofs will be able to reuse same statements (for example, in syntax breakdown steps). Also I have a feeling that the metamath.exe minimization algo will be able to do more with bigger proofs. Similarly, many proofs share the same hypotheses (for instance, |- ( ph -> A e. RR ) ), and it can be reused if you put several statements into one block.

Thank you! Sure, I will add it into my mathbox after some enhancement.

> Also you seem to be jumping back and forth from the deduction style (like in _3cubeslem1_gtz_d) and "usual style" (like in _3cubeslem1_gtz_i). I don't know if that's necessary, but the idea is usually to carry the proof in deduction style where it's possible and maybe switch to the usual style near the end to state the main result.

At the beginning I didn’t know what approach to use. That’s why there are theorems in different forms in the beginning. Initially I created all three forms (inference, deduction and closed) for each theorem because I didn’t know what form I would need further in the proof. But somewhere in the middle of the proof I realized that I need only deduction. Before creating a pull request I will remove all redundant theorems.

> By the way, did you end up using some automation to finish the proof, or you did it all by hand after all?

The parts where I needed to compare or transform polynomials have been proved in semi-automatic mode. Everything else has been done manually. I heavily used the bottom-up prover of mm-lamp, but I count it as “manual mode” because it is able to find only very simple proofs. By the semi-automatic mode I mean a new automation functionality which I added to mm-lamp while working on this proof. It is currently not available on the mm-lamp web site, but I will release it in one of the next versions (hopefully in the next one).

-

Igor

[David A. Wheeler]

Savask:

> > Igor, congratulations!

I agree, Igor, congrats!!

> On Jan 2, 2024, at 12:07 PM, Igor Ieskov <igori...@gmail.com> wrote:
>
> Thank you! Sure, I will add it into my mathbox after some enhancement.

That's great! I'm hoping that you'll format it so that it (or at least some of the supporting parts)
can eventually be moved into the "main" body as well.

This theorem of Ryley ("every rational number is a sum of three cubes of rational numbers") is
general, so I think it's worthy to eventually be the main body. We often put
things in mathboxes first, then *later* move them into the body, so it'd be a pretty typical progression.

> At the beginning I didn’t know what approach to use. That’s why there are theorems in different forms in the beginning. Initially I created all three forms (inference, deduction and closed) for each theorem because I didn’t know what form I would need further in the proof. But somewhere in the middle of the proof I realized that I need only deduction. Before creating a pull request I will remove all redundant theorems.

I agree. Putting most things in deduction form makes it easier to combine results, and you can always create the other forms from deduction form.

> > By the way, did you end up using some automation to finish the proof, or you did it all by hand after all?
>
> The parts where I needed to compare or transform polynomials have been proved in semi-automatic mode. Everything else has been done manually. I heavily used the bottom-up prover of mm-lamp, but I count it as “manual mode” because it is able to find only very simple proofs. By the semi-automatic mode I mean a new automation functionality which I added to mm-lamp while working on this proof. It is currently not available on the mm-lamp web site, but I will release it in one of the next versions (hopefully in the next one).

I'm looking forward to this new automation functionality in metamath-lamp!

I think metamath-lamp is a nice proof assistant for Metamath.
If you're interested in learning more about metamath-lamp, I wrote this guide:
https://lamp-guide.metamath.org/
and the first chapters of that guide are also available as videos:
https://www.youtube.com/playlist?list=PL1jSu6GGefBk3RhHW5Srpc2qxWMqhga9J

Metamath-lamp isn't perfect of course. Its "unification" algorithm currently has a known weakness
(it's really just a "match" algorithm, so sometimes you have to hand-execute replacements
that would be automatic in tools like mmj2 that use full unification).
That's not fundamental to the tool, it's just a weakness of its current implementation.
In addition, mmj2 has some nice situation-specific automation that metamath-lamp currently lacks.
That said, you can start using metamath-lamp without installing anything ("just use your
web browser"), and it even works well on a mobile phone without installing anything.
That "ease of getting started" makes metamath-lamp a nice addition to our collection of tools.
So congrats to Igor for both the proof *and* for developing the metamath-lamp tool!

--- David A. Wheeler

[Igor Ieskov]

>  I agree, Igor, congrats!!

Thanks, David!

>  I'm hoping that you'll format it so that it (or at least some of the supporting parts)
> can eventually be moved into the "main" body as well.

Sure, I will format as required for set.mm. 

Anyway, I think my PR will not be merged without appropriate formatting.

-

Igor

[Igor Ieskov]

Here are a few videos which show the automation I used to prove some parts of 3cubes (all videos are speechless):

Part 0 - initial setup to make this demo easier to reproduce

https://drive.google.com/file/d/1x-cV6dL3wqEeKalbXlaRP7AtZmxnFlWQ/view?usp=drive_link

Part 1 - converting a polynomial to the “base form”

https://drive.google.com/file/d/1IOk3QMteDB-IyV8OCWS56miyfcXksOFy/view?usp=drive_link

Part 2 - proving equality of two polynomials. This part also shows how to automatically create inference and closed forms from an existing deduction form (at the end of the video). Also, in this part, I cut a lot of time where the screen was blinking. So, macros work faster on the video than in reality.

https://drive.google.com/file/d/1hipxElyqrkuKYzEjH_AR4c0uap_3MYvu/view?usp=drive_link

Part 3 - creating a simple macro

https://drive.google.com/file/d/1qpFCZTXXVZ6TwJuuA_OPnAgfXzFiPrAZ/view?usp=drive_link

This automation is based on macros. A macro is a JavaScript function which automates one or few manual steps by calling special predefined API functions. Those API functions allow to interact with metamath-lamp functionality (everything works locally, there are no calls via the Internet). Those API functions do something which could be done manually. Only the proveBottomUp API has some additional capabilities not available via the UI. I am not providing more details because this is still a work in progress. This has not been released yet and it is available on dev version of metamath-lamp at the moment.

-

Igor

[Igor Ieskov]

Here is a new link for the part 3:

https://drive.google.com/file/d/1c5t-Nhuy6KX6UmTtEGjXJa-54HFZhp3x/view?usp=drive_link

(the previous link became invalid)

-

Igor

[savask]

> Here are a few videos which show the automation I used to prove some parts of 3cubes (all videos are speechless)

That's impressive!

In all fairness, it's pretty hard to understand what's going on in the videos, but it looks like your tactics use a lot of intermediate variables in the process (which get eliminated in the end, I guess). I think any intermediate variables can be avoided whatsoever. Also I was expecting a lot less manual interaction for comparing two polynomials, but I probably don't understand some details.

You might know about this already, but mmj2 also has some macros, see https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js Maybe this can serve as inspiration for future work.

[Igor Ieskov]

>In all fairness, it's pretty hard to understand what's going on in the videos, but it looks like your tactics use a lot of intermediate variables in the process (which get eliminated in the end, I guess). I think any intermediate variables can be avoided whatsoever.

You are right. Intermediate variables are used to make the statements more readable. Also a special naming convention for the variables is used, so that tactics can understand what to do with each variable. I also think that intermediate variables can be avoided. But this depends on personal preferences and tools used. For example, I cannot work with very long statements containing a lot of parenthesis. That’s why I prefer to use intermediate variables. Also, the special naming convention helps to improve performance a bit. Tactics can easily parse a variable name to get required information about that variable’s value instead of analyzing the value itself.

> Also I was expecting a lot less manual interaction for comparing two polynomials, but I probably don't understand some details.

I think it is possible to make a full automation for such types of proofs. Maybe I will do it in some time.

Thanks for the transformations.js script. I will review it.

-

Igor

[savask]

> Intermediate variables are used to make the statements more readable. Also a special naming convention for the variables is used, so that tactics can understand what to do with each variable.

I hope the usage of variables doesn't have a negative impact on the proof's length.

> I think it is possible to make a full automation for such types of proofs. Maybe I will do it in some time.

That would be great. Say, if you have two polynomials f(A, B) and g(A, B) and you want to prove |- f(A, B) = g(A, B), a tactic should be able to do that, and leave some unproved goals of the form |- A e. CC and |- B e. CC.

I tried making a rudimentary polynomial-expansion tactic in Haskell, for example to expand ( A + B ) x. ( A + B ) x. A it would output:

ghci> let (exp, pf) = expand ((va .+. vb) .*. (va .+. vb) .*. va)
ghci> mapM_ print $ clean pf
( ( ( A + B ) x. ( A + B ) ) x. A ) = ( ( ( ( A x. A ) + ( B x. A ) ) + ( ( A x. B ) + ( B x. B ) ) ) x. A )
A e. CC
( A x. A ) e. CC
B e. CC
( B x. A ) e. CC
( ( A x. A ) + ( B x. A ) ) e. CC
( A x. B ) e. CC
( B x. B ) e. CC
( ( A x. B ) + ( B x. B ) ) e. CC
( ( ( ( A x. A ) + ( B x. A ) ) + ( ( A x. B ) + ( B x. B ) ) ) x. A ) = ( ( ( ( A x. A ) + ( B x. A ) ) x. A ) + ( ( ( A x. B ) + ( B x. B ) ) x. A ) )
( ( ( A x. A ) + ( B x. A ) ) x. A ) = ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) )
( ( ( A x. B ) + ( B x. B ) ) x. A ) = ( ( ( A x. B ) x. A ) + ( ( B x. B ) x. A ) )
( ( ( ( A x. A ) + ( B x. A ) ) x. A ) + ( ( ( A x. B ) + ( B x. B ) ) x. A ) ) = ( ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A x. B ) + ( B x. B ) ) x. A ) )
( ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A x. B ) + ( B x. B ) ) x. A ) ) = ( ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A x. B ) x. A ) + ( ( B x. B ) x. A ) ) )
( ( ( ( A x. A ) + ( B x. A ) ) + ( ( A x. B ) + ( B x. B ) ) ) x. A ) = ( ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A x. B ) x. A ) + ( ( B x. B ) x. A ) ) )

The first line is the proved statement, and the lines after it are the proof. If you insert it in metamath-lamp line by line (marking A e. CC and B e. CC as hypotheses), it would successfully unify. Of course your tactics are superior, but at least mine didn't require any intermediate variables or manual input :-)

> Thanks for the transformations.js script. I will review it.

It would be nice to hear what Mario has to say about it, but you will quickly notice that quite often the tactic simply tries to apply some theorem from a carefully chosen list when it is possible or when the expression matches some pattern. That seems to be enough to perform basic arithmetic (prove stuff like ; 1 2 + ; 3 9 = ; 5 1).

[Igor Ieskov]

> The first line is the proved statement, and the lines after it are the proof. If you insert it in metamath-lamp line by line (marking A e. CC and B e. CC as hypotheses), it would successfully unify.

The first line doesn’t look like a full expansion, because A gets multiplied by a sum of other variables. The right part of the last line seems to be the full expansion. But when I inserted all the lines to metamath-lamp (this link leads to my attempt to unify your proof), there was one not unified step, basically the first line in your proof was not unified. It could be a bug in metamath-lamp (I need more time to understand what’s going on). But also it looks like some steps are missing in your proof. For example, I would expect a line which proves “( A + B ) e. CC”, but it is missing in your proof. Anyway, I understand the idea of your approach, and it looks very reasonable. 

> Of course your tactics are superior, but at least mine didn't require any intermediate variables or manual input

For this example, my tactics require only one intermediate variable and almost no manual input either. Here is a demo - https://drive.google.com/file/d/1ihCwiCyW0Ha_1qK6AY8xpa_BqsKlb51r/view?usp=drive_link

Intermediate variables become necessary for my tactics when there are also constants, for example, ( A x. ( ( 2 + 1 ) x. B ) ). If you try to apply the same tactic as shown on the demo above, you’ll end up with something like … ( 2 x. B ) … + … ( 1 x. B ) … , which is obviously not the desired result. Anyway, I am not insisting on any of the approaches. This is just what I came to during work on proof for 3cubes. However, I found usage of intermediate variables very convenient. Here is why I like this approach. The demos I showed run very smooth because I prepared by repeating those proofs several times before recording. But even there I made a few mistakes. When I was working on proofs for 3cubes, I made a lot more mistakes and encountered a lot of errors (due to both my inexperience and bugs in tactics). But thanks to usage of intermediate variables, which made all the statements short and readable, I was able to resolve errors sufficiently fast. So, intermediate variables may look awkward and negatively impact the quality of the resulting proof, but they may save a bit of mental health for such beginners as me :)

> I hope the usage of variables doesn't have a negative impact on the proof's length.

I don’t think the variables negatively impact the proof’s length. The tactics itself may produce long proofs.

> you will quickly notice that quite often the tactic simply tries to apply some theorem from a carefully chosen list when it is possible or when the expression matches some pattern. That seems to be enough to perform basic arithmetic (prove stuff like ; 1 2 + ; 3 9 = ; 5 1).

I noticed that. The bottom-up prover in metamath-lamp (this is the core of all my tactics) also uses a similar approach. However, from what I see, transformations.js uses trickier algorithms. Comparing to it my prover is more straightforward. I am not sure if my prover will be able to prove statements like ; 1 2 + ; 3 9 = ; 5 1, but I think it should be able (probably after some revision).

-

Igor

[savask]

> The first line doesn’t look like a full expansion, because A gets multiplied by a sum of other variables. ...

Yes, you are right, that's a bug in my program. What actually has happened is that in the routine which is supposed to expand X and Y before expanding X x. Y by distributivity, I forgot to record the proofs for X = (expanded X) and Y = (expanded Y). So that's why some steps are missing and the proof starts with a strange line. It's funny that it unified at all!

The correct proved statement is this:

|- ( ( ( A + B ) x. ( A + B ) ) x. A ) = ( ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A x. B ) x. A ) + ( ( B x. B ) x. A ) ) )

I think I fixed the program, here's the correct proof (I hope).

> Intermediate variables become necessary for my tactics when there are also constants, for example, ( A x. ( ( 2 + 1 ) x. B ) ).

I guess it's not entirely clear how to do that automatically, indeed. Say, if you have ( ( ( 3 x. 2 ) x. A ) x. B ), in some cases you would want to transform it into ( ( 6 x. A ) x. B ) and in other cases it's better to leave it as is. Ideally, you would want to be able to type |- X = Y and let the tactic figure out the rest :-)

> However, from what I see, transformations.js uses trickier algorithms.

As I understand it, there's an arithEval function which can parse metamath expressions like ( ( ; 3 1 + ; 9 0 ) x. 3 ) and evaluate them to a concrete integer (363 in this case). I don't think it's very tricky, but I haven't tried implementing something like that myself, so I might be underestimating it.