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).
I am working on a proof. I used the bottom-up prover a lot of times during this proof, but I always had to unselect "Allow new variables". This suggests that a more convenient default value for this parameter should be "false" (unselected).
I am working on a proof. I used the bottom-up prover a lot of times during this proof, but I always had to unselect "Allow new variables". This suggests that a more convenient default value for this parameter should be "false" (unselected).