Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
On the Editor tab, try to find assertions matching the pattern ( A + ( B + C ) ) = ( ( A + B ) + C ). Assertions are found but it takes a lot of time to finish the search.
On the Editor tab, try to find assertions matching the pattern
( A + ( B + C ) ) = ( ( A + B ) + C ). Assertions are found but it takes a lot of time to finish the search.