炼金术：通过符号变异提升定理证明能力

该研究通过结合学习和定理证明的方法，大幅提升了E自动定理证明器在Isabelle Sledgehammer问题上的性能。利用ENIGMA指导、神经前提选择和E的策略开发，系统在15秒内性能提升25.3%，超越所有之前的ATP和SMT系统。该方法可用于大规模问题的迭代训练。