Comment by iamgopal

True, but could humans cross pollinating lean x prolog x A* ( or any search algorithm) could have solved such math problems with super computer ?