You should read https://intelligence.org/2013/12/21/josef-urban-on-machine-l... and the citations! After that, you almost wonder why no one had applied NNs before.
http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?deco...
it was the first result at the time from: http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename...
There was a feeling reading the original paper of "why has no one done this yet" but I don't have the chops to ask that, yet.