If anyone has a particularly challenging step in a proof in set.mm where the step derivation could fail, please let me know. I'd be happy to try it.
As I've written, I usually check the largest proof I'm aware of and perform step derivation for a step that has many hypotheses and it's in the final part of the proof. Since it's at the end of the proof, the backtracking has 1500+ candidates for every hypothesis. Furthermore, the correct label is in the last part of set.mm, so tens of thousands of labels have to be tried before a solution is found. But since I wrote the algorithm, I'm the worst person to try to test it, so adversarial tests are welcome. -- 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 [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/e96ad325-e3c6-4689-9ad7-b5a25a2860a9n%40googlegroups.com.
